---

Step * 1 1 1 of Lemma fps-elim-hom


1. X : Type
2. valueall-type(X)
3. eq : EqDecider(X)
4. r : CRng
5. x : X
6. FunThru2op(PowerSeries(X;r);PowerSeries(X;r);λf,g. (f+g);λf,g. (f+g);fps-elim(x))
7. a1 : PowerSeries(X;r)
8. a2 : PowerSeries(X;r)
9. b : bag(X)
10. x ↓∈ b
11. ∀[b:bag(bag(X) × bag(X))]. ∀[f:(bag(X) × bag(X)) ⟶ |r|].
      Σ(x∈b). f[x] = 0 ∈ |r| 
      supposing (∀x:bag(X) × bag(X). (x ↓∈ b ⇒ (f[x] = 0 ∈ |r|))) ∧ IsMonoid(|r|;+r;0) ∧ Comm(|r|;+r)
12. p1 : bag(X)
13. ¬x ↓∈ p1
14. p2 : bag(X)
15. ¬x ↓∈ p2
16. (p1 + p2) = b ∈ bag(X)
⊢ (* (a1 p1) (a2 p2)) = 0 ∈ |r|
BY
{ xxx(xxx(Assert x ↓∈ p1 + p2 BY Auto)xxx THEN BagMemberD (-1) THEN SquashExRepD THEN D -1 THEN Auto)xxx }

---

Latex:

---

Latex:

1.  X  :  Type
2.  valueall-type(X)
3.  eq  :  EqDecider(X)
4.  r  :  CRng
5.  x  :  X
6.  FunThru2op(PowerSeries(X;r);PowerSeries(X;r);\mlambda{}f,g.  (f+g);\mlambda{}f,g.  (f+g);fps-elim(x))
7.  a1  :  PowerSeries(X;r)
8.  a2  :  PowerSeries(X;r)
9.  b  :  bag(X)
10.  x  \mdownarrow{}\mmember{}  b
11.  \mforall{}[b:bag(bag(X)  \mtimes{}  bag(X))].  \mforall{}[f:(bag(X)  \mtimes{}  bag(X))  {}\mrightarrow{}  |r|].
            \mSigma{}(x\mmember{}b).  f[x]  =  0 
            supposing  (\mforall{}x:bag(X)  \mtimes{}  bag(X).  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (f[x]  =  0)))  \mwedge{}  IsMonoid(|r|;+r;0)  \mwedge{}  Comm(|r|;+r)
12.  p1  :  bag(X)
13.  \mneg{}x  \mdownarrow{}\mmember{}  p1
14.  p2  :  bag(X)
15.  \mneg{}x  \mdownarrow{}\mmember{}  p2
16.  (p1  +  p2)  =  b
\mvdash{}  (*  (a1  p1)  (a2  p2))  =  0


By

---

Latex:
xxx(xxx(Assert  x  \mdownarrow{}\mmember{}  p1  +  p2  BY
                            Auto)xxx
        THEN  BagMemberD  (-1)
        THEN  SquashExRepD
        THEN  D  -1
        THEN  Auto)xxx

---

Home Index