---

Step * 3 1 of Lemma mul-mono-poly-req


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))
BY
{ (GenConclTerms Auto [⌜imonomial-term(m)⌝;⌜imonomial-term(u)⌝;⌜ipolynomial-term(v)⌝]⋅ THEN All Thin) }

1
1. v1 : int_term()
2. v2 : int_term()
3. v3 : int_term()
⊢ (v1 (*) v2) (+) (v1 (*) v3) ≡ v1 (*) (v2 (+) v3)

---

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)
\mvdash{}  (imonomial-term(m)  (*)  imonomial-term(u))  (+)  (imonomial-term(m)  (*)  ipolynomial-term(v)) 
\mequiv{}  imonomial-term(m)  (*)  (imonomial-term(u)  (+)  ipolynomial-term(v))


By

---

Latex:
(GenConclTerms  Auto  [\mkleeneopen{}imonomial-term(m)\mkleeneclose{};\mkleeneopen{}imonomial-term(u)\mkleeneclose{};\mkleeneopen{}ipolynomial-term(v)\mkleeneclose{}]\mcdot{}  THEN  All  Thin)

---

Home Index