---

Step * of Lemma fps-mul-comm

∀[X:Type]. ∀[eq:EqDecider(X)].
  ∀[r:CRng]. ∀[f,g:PowerSeries(X;r)].  ((f*g) = (g*f) ∈ PowerSeries(X;r)) supposing valueall-type(X)
BY
{ (Auto
   THEN Unfold `power-series` 0
   THEN RepUR ``fps-mul fps-coeff`` 0
   THEN (EqCD⋅ THEN Auto)
   THEN (Fold `infix_ap` 0 THEN Fold `fps-coeff` 0)⋅
   THEN (Assert Assoc(|r|;+r) ∧ Comm(|r|;+r) BY
               ((InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
                THEN Fold `comm` (-1)
                THEN Auto
                THEN RepeatFor 2 (DVar `r')
                THEN Auto))
   THEN RW (AddrC [3;3] (RevLemmaC `bag-partitions-symmetry`)) 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. b : bag(X)
8. Assoc(|r|;+r)
9. Comm(|r|;+r)
⊢ Σ(p∈bag-partitions(eq;b)). f[fst(p)] * g[snd(p)]
= Σ(p∈bag-map(λp.<snd(p), fst(p)>;bag-partitions(eq;b))). g[fst(p)] * f[snd(p)]
∈ |r|

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  Unfold  `power-series`  0
  THEN  RepUR  ``fps-mul  fps-coeff``  0
  THEN  (EqCD\mcdot{}  THEN  Auto)
  THEN  (Fold  `infix\_ap`  0  THEN  Fold  `fps-coeff`  0)\mcdot{}
  THEN  (Assert  Assoc(|r|;+r)  \mwedge{}  Comm(|r|;+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  RW  (AddrC  [3;3]  (RevLemmaC  `bag-partitions-symmetry`))  0
  THEN  Auto)

---

Home Index