---

Step * 1 of Lemma fps-compose-scalar-mul


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. c : |r|
6. x : X
7. g : PowerSeries(X;r)
8. f : PowerSeries(X;r)
9. bs : bag(X)
10. v : bag(bag(X) List+)
11. bag-parts'(eq;bs;x) = v ∈ bag(bag(X) List+)
12. Comm(|r|;+r)
13. Assoc(|r|;+r)
14. ∀L:bag(X) List+. (||L|| ≥ 1 )
15. Assoc(|r|;*) ∧ Comm(|r|;*)
16. ∀L:bag(X) List+. (Πa ∈ tl(L). f a ∈ |r|)
17. ∀[mul:|r| ⟶ |r| ⟶ |r|]. ∀[zero:|r|]. ∀[b:bag(bag(X) List+)]. ∀[f:bag(X) List+ ⟶ |r|].
      ∀a:|r|. (Σ(x∈b). a mul f[x] = (a mul Σ(x∈b). f[x]) ∈ |r|) 
      supposing (∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;zero;minus)) ∧ Comm(|r|;+r) ∧ BiLinear(|r|;+r;mul)
⊢ Σ(L∈v). (c * (g (hd(L) + bag-rep(||tl(L)||;x)))) * Πa ∈ tl(L). f a
= Σ(L∈v). c * ((g (hd(L) + bag-rep(||tl(L)||;x))) * Πa ∈ tl(L). f a)
∈ |r|
BY
{ xxx(Using [`T',⌜bag(X) List+⌝] EqCD⋅ THEN Auto THEN (RW RngNormC 0 THEN Auto)⋅)⋅xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  c  :  |r|
6.  x  :  X
7.  g  :  PowerSeries(X;r)
8.  f  :  PowerSeries(X;r)
9.  bs  :  bag(X)
10.  v  :  bag(bag(X)  List\msupplus{})
11.  bag-parts'(eq;bs;x)  =  v
12.  Comm(|r|;+r)
13.  Assoc(|r|;+r)
14.  \mforall{}L:bag(X)  List\msupplus{}.  (||L||  \mgeq{}  1  )
15.  Assoc(|r|;*)  \mwedge{}  Comm(|r|;*)
16.  \mforall{}L:bag(X)  List\msupplus{}.  (\mPi{}a  \mmember{}  tl(L).  f  a  \mmember{}  |r|)
17.  \mforall{}[mul:|r|  {}\mrightarrow{}  |r|  {}\mrightarrow{}  |r|].  \mforall{}[zero:|r|].  \mforall{}[b:bag(bag(X)  List\msupplus{})].  \mforall{}[f:bag(X)  List\msupplus{}  {}\mrightarrow{}  |r|].
            \mforall{}a:|r|.  (\mSigma{}(x\mmember{}b).  a  mul  f[x]  =  (a  mul  \mSigma{}(x\mmember{}b).  f[x])) 
            supposing  (\mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;zero;minus))
            \mwedge{}  Comm(|r|;+r)
            \mwedge{}  BiLinear(|r|;+r;mul)
\mvdash{}  \mSigma{}(L\mmember{}v).  (c  *  (g  (hd(L)  +  bag-rep(||tl(L)||;x))))  *  \mPi{}a  \mmember{}  tl(L).  f  a
=  \mSigma{}(L\mmember{}v).  c  *  ((g  (hd(L)  +  bag-rep(||tl(L)||;x)))  *  \mPi{}a  \mmember{}  tl(L).  f  a)


By

---

Latex:
xxx(Using  [`T',\mkleeneopen{}bag(X)  List\msupplus{}\mkleeneclose{}]  EqCD\mcdot{}  THEN  Auto  THEN  (RW  RngNormC  0  THEN  Auto)\mcdot{})\mcdot{}xxx

---

Home Index