---

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


1. m : iMonomial()
2. u : iMonomial()
3. v : iMonomial() List
4. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
5. mul-mono-poly(m;v) ∈ iMonomial() List
⊢ ipolynomial-term([mul-monomials(m;u) / mul-mono-poly(m;v)]) ≡ imonomial-term(m) (*) ipolynomial-term([u / v])
BY
{ (Thin (-1) THEN RWW "ipolynomial-term-cons -1 mul-monomials-equiv" 0 THEN Auto) }

1
1. m : iMonomial()
2. u : iMonomial()
3. v : iMonomial() List
4. ipolynomial-term(mul-mono-poly(m;v)) ≡ imonomial-term(m) (*) ipolynomial-term(v)
⊢ (imonomial-term(m) (*) imonomial-term(u)) (+) (imonomial-term(m) (*) ipolynomial-term(v)) ≡ imonomial-term(m)
  (*) (imonomial-term(u) (+) ipolynomial-term(v))

---

Latex:

---

Latex:

1.  m  :  iMonomial()
2.  u  :  iMonomial()
3.  v  :  iMonomial()  List
4.  ipolynomial-term(mul-mono-poly(m;v))  \mequiv{}  imonomial-term(m)  (*)  ipolynomial-term(v)
5.  mul-mono-poly(m;v)  \mmember{}  iMonomial()  List
\mvdash{}  ipolynomial-term([mul-monomials(m;u)  /  mul-mono-poly(m;v)])  \mequiv{}  imonomial-term(m)
    (*)  ipolynomial-term([u  /  v])


By

---

Latex:
(Thin  (-1)  THEN  RWW  "ipolynomial-term-cons  -1  mul-monomials-equiv"  0  THEN  Auto)

---

Home Index