---

Step * of Lemma fps-scalar-mul-property

∀[X:Type]
  ∀[eq:EqDecider(X)]. ∀[r:CRng].
    ((IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
    ∧ IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f))
    ∧ (∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g)))) 
  supposing valueall-type(X)
BY
{ xxx(RepeatFor 4 ((D 0 THENA Auto))
      THEN (InstLemma `rng_plus_comm` [⌜r⌝]⋅ THENA Auto)
      THEN Fold `comm` (-1)
      THEN (Assert Assoc(|r|;+r) BY
                  (RepeatFor 2 (DVar `r') THEN Auto))
      THEN (Assert BiLinear(|r|;+r;*) ∧ IsMonoid(|r|;+r;0) ∧ (∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus)) BY
                  (RepeatFor 2 (DVar `r') THEN Auto THEN With ⌜-r⌝ (D 0)⋅ THEN Auto)))xxx }

1
1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. Comm(|r|;+r)
6. Assoc(|r|;+r)
7. BiLinear(|r|;+r;*) ∧ IsMonoid(|r|;+r;0) ∧ (∃minus:|r| ⟶ |r|. IsGroup(|r|;+r;0;minus))
⊢ (IsAction(|r|;*;1;PowerSeries(X;r);λc,f. (c)*f)
∧ IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;λf,g. (f+g);λf,g. (f+g);λc,f. (c)*f))
∧ (∀c:|r|. Dist1op2opLR(PowerSeries(X;r);λf.(c)*f;λf,g. (f*g)))

---

Latex:

---

Latex:
\mforall{}[X:Type]
    \mforall{}[eq:EqDecider(X)].  \mforall{}[r:CRng].
        ((IsAction(|r|;*;1;PowerSeries(X;r);\mlambda{}c,f.  (c)*f)
        \mwedge{}  IsBilinear(|r|;PowerSeries(X;r);PowerSeries(X;r);+r;\mlambda{}f,g.  (f+g);\mlambda{}f,g.  (f+g);\mlambda{}c,f.  (c)*f))
        \mwedge{}  (\mforall{}c:|r|.  Dist1op2opLR(PowerSeries(X;r);\mlambda{}f.(c)*f;\mlambda{}f,g.  (f*g)))) 
    supposing  valueall-type(X)


By

---

Latex:
xxx(RepeatFor  4  ((D  0  THENA  Auto))
        THEN  (InstLemma  `rng\_plus\_comm`  [\mkleeneopen{}r\mkleeneclose{}]\mcdot{}  THENA  Auto)
        THEN  Fold  `comm`  (-1)
        THEN  (Assert  Assoc(|r|;+r)  BY
                                (RepeatFor  2  (DVar  `r')  THEN  Auto))
        THEN  (Assert  BiLinear(|r|;+r;*)
                                \mwedge{}  IsMonoid(|r|;+r;0)
                                \mwedge{}  (\mexists{}minus:|r|  {}\mrightarrow{}  |r|.  IsGroup(|r|;+r;0;minus))  BY
                                (RepeatFor  2  (DVar  `r')  THEN  Auto  THEN  With  \mkleeneopen{}-r\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))xxx

---

Home Index