---

Step * of Lemma fps-mul-assoc

No Annotations
∀[X:Type]. ∀[eq:EqDecider(X)].
  ∀[r:CRng]. ∀[f,g,h:PowerSeries(X;r)].  (((f*g)*h) = (f*(g*h)) ∈ PowerSeries(X;r)) supposing valueall-type(X)
BY
{ (Auto
   THEN (Assert Assoc(|r|;+r) ∧ Comm(|r|;+r) ∧ BiLinear(|r|;+r;*) ∧ Assoc(|r|;*) BY
               ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
                THEN Fold `comm` (-1)
                THEN Auto
                THEN RepeatFor 2 (DVar `r')
                THEN Auto))
   THEN (Auto
         THEN RepUR ``power-series fps-mul fps-coeff`` 0
         THEN Fold `infix_ap` 0
         THEN Fold `fps-coeff` 0
         THEN (EqCD THEN Auto)
         THEN (Assert ∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus) BY
                     (With ⌜-r⌝ (D 0)⋅ THEN Auto THEN RepeatFor 2 (DVar `r') THEN Auto))
         THEN ((RWO "bag-summation-linear1<" 0 THEN Auto)⋅ THEN (RWO "bag-summation-linear1-right<" 0 THEN Auto)⋅)⋅)⋅) }

1
1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. f : PowerSeries(X;r)
6. g : PowerSeries(X;r)
7. h : PowerSeries(X;r)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
10. BiLinear(|r|;+r;*)
11. Assoc(|r|;*)
12. b : bag(X)@i
13. ∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus)
⊢ Σ(p∈bag-partitions(eq;b)). Σ(p1∈bag-partitions(eq;fst(p))). (f[fst(p1)] * g[snd(p1)]) * h[snd(p)]
= Σ(p∈bag-partitions(eq;b)). Σ(p1∈bag-partitions(eq;snd(p))). f[fst(p)] * (g[fst(p1)] * h[snd(p1)])
∈ |r|

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].
    \mforall{}[r:CRng].  \mforall{}[f,g,h:PowerSeries(X;r)].    (((f*g)*h)  =  (f*(g*h)))  supposing  valueall-type(X)


By

---

Latex:
(Auto
  THEN  (Assert  Assoc(|r|;+r)  \mwedge{}  Comm(|r|;+r)  \mwedge{}  BiLinear(|r|;+r;*)  \mwedge{}  Assoc(|r|;*)  BY
                          ((InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
                            THEN  Fold  `comm`  (-1)
                            THEN  Auto
                            THEN  RepeatFor  2  (DVar  `r')
                            THEN  Auto))
  THEN  (Auto
              THEN  RepUR  ``power-series  fps-mul  fps-coeff``  0
              THEN  Fold  `infix\_ap`  0
              THEN  Fold  `fps-coeff`  0
              THEN  (EqCD  THEN  Auto)
              THEN  (Assert  \mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;0;minus)  BY
                                      (With  \mkleeneopen{}-r\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  RepeatFor  2  (DVar  `r')  THEN  Auto))
              THEN  ((RWO  "bag-summation-linear1<"  0  THEN  Auto)\mcdot{}
                          THEN  (RWO  "bag-summation-linear1-right<"  0  THEN  Auto)\mcdot{}
                          )\mcdot{})\mcdot{})

---

Home Index