---

Step * 2 of Lemma mul-mono-poly-ringeq

.....aux..... 
1. r : CRng
2. m : iMonomial()
3. u : iMonomial()
4. v : iMonomial() List
5. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
⊢ (mul-mono-poly(m;v))↓
BY
{ xxx(GenConcl ⌜mul-mono-poly(m;v) = L ∈ (iMonomial() List)⌝⋅ THEN Auto)xxx }

---

Latex:

---

Latex:
.....aux..... 
1.  r  :  CRng
2.  m  :  iMonomial()
3.  u  :  iMonomial()
4.  v  :  iMonomial()  List
5.  ipolynomial-term(mul-mono-poly(m;v))  \mequiv{}  imonomial-term(m)  (*)  ipolynomial-term(v)
\mvdash{}  (mul-mono-poly(m;v))\mdownarrow{}


By

---

Latex:
xxx(GenConcl  \mkleeneopen{}mul-mono-poly(m;v)  =  L\mkleeneclose{}\mcdot{}  THEN  Auto)xxx

---

Home Index