---

Step * of Lemma fps-alg_wf

∀[X:Type]. ∀[eq:EqDecider(X)].  ∀[r:CRng]. (fps-alg(X;eq;r) ∈ CAlg(r)) supposing valueall-type(X)
BY
{ ((Auto THEN InstLemma `fps-scalar-mul-property` [⌜X⌝;⌜eq⌝;⌜r⌝]⋅ THEN Auto)
   THEN (InstLemma `fps-rng_wf` [⌜X⌝;⌜eq⌝;⌜r⌝]⋅ THEN Auto)
   THEN MemTypeD (-1)
   THEN Auto
   THEN Fold `member` (-2)
   THEN MemTypeD (-2)
   THEN Auto
   THEN Fold `member` (-3)
   THEN RepeatFor 3 ((MemTypeCD THEN Auto THEN Try ((Reduce 0 THEN BackThruSomeHyp))))) }

1
1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
6. IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f)
7. ∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g))
8. fps-rng(r) ∈ RngSig
9. IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1)
10. Comm(|fps-rng(r)|;*)
⊢ fps-alg(X;eq;r) ∈ algebra_sig{i:l}(|r|)

2
1. X : Type
2. eq : EqDecider(X)
3. valueall-type(X)
4. r : CRng
5. IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
6. IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f)
7. ∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g))
8. fps-rng(r) ∈ RngSig
9. IsRing(|fps-rng(r)|;+fps-rng(r);0;-fps-rng(r);*;1)
10. Comm(|fps-rng(r)|;*)
11. IsGroup(fps-alg(X;eq;r).car;fps-alg(X;eq;r).plus;fps-alg(X;eq;r).zero;fps-alg(X;eq;r).minus)
⊢ Comm(fps-alg(X;eq;r).car;fps-alg(X;eq;r).plus)

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[eq:EqDecider(X)].    \mforall{}[r:CRng].  (fps-alg(X;eq;r)  \mmember{}  CAlg(r))  supposing  valueall-type(X)


By

---

Latex:
((Auto  THEN  InstLemma  `fps-scalar-mul-property`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (InstLemma  `fps-rng\_wf`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{};\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  MemTypeD  (-1)
  THEN  Auto
  THEN  Fold  `member`  (-2)
  THEN  MemTypeD  (-2)
  THEN  Auto
  THEN  Fold  `member`  (-3)
  THEN  RepeatFor  3  ((MemTypeCD  THEN  Auto  THEN  Try  ((Reduce  0  THEN  BackThruSomeHyp)))))

---

Home Index