---

Step * 1 1 of Lemma mvp-add_wf


1. r : CRng
2. s : bag(Atom)
3. p1 : {f:PowerSeries(r)| ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)} 
4. s1 : bag(Atom)
5. q1 : {f:PowerSeries(r)| ∀[b:bag(Atom)]. f[b] = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s1)} 
6. b : bag(Atom)
7. ¬sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
⊢ (+r (p1 b) (q1 b)) = 0 ∈ |r|
BY
{ xxx(All DSet
      THEN All (Unfold `fps-coeff`)
      THEN RWO "4 7" 0
      THEN Auto
      THEN Try ((ParallelLast THEN BLemma `sub-bag-lub` THEN Auto)))xxx }

1
1. r : CRng
2. s : bag(Atom)
3. p1 : PowerSeries(r)
4. ∀[b:bag(Atom)]. (p1 b) = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s)
5. s1 : bag(Atom)
6. q1 : PowerSeries(r)
7. ∀[b:bag(Atom)]. (q1 b) = 0 ∈ |r| supposing ¬sub-bag(Atom;b;s1)
8. b : bag(Atom)
9. ¬sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
⊢ (+r 0 0) = 0 ∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  s  :  bag(Atom)
3.  p1  :  \{f:PowerSeries(r)|  \mforall{}[b:bag(Atom)].  f[b]  =  0  supposing  \mneg{}sub-bag(Atom;b;s)\} 
4.  s1  :  bag(Atom)
5.  q1  :  \{f:PowerSeries(r)|  \mforall{}[b:bag(Atom)].  f[b]  =  0  supposing  \mneg{}sub-bag(Atom;b;s1)\} 
6.  b  :  bag(Atom)
7.  \mneg{}sub-bag(Atom;b;bag-lub(AtomDeq;s;s1))
\mvdash{}  (+r  (p1  b)  (q1  b))  =  0


By

---

Latex:
xxx(All  DSet
        THEN  All  (Unfold  `fps-coeff`)
        THEN  RWO  "4  7"  0
        THEN  Auto
        THEN  Try  ((ParallelLast  THEN  BLemma  `sub-bag-lub`  THEN  Auto)))xxx

---

Home Index