---

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


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)
6. ∀[m:iMonomial()]. ∀[p:iMonomial() List].  ipolynomial-term([m / p]) ≡ imonomial-term(m) (+) ipolynomial-term(p)
7. ∀[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)
⊢ ipolynomial-term([mul-monomials(m;u) / mul-mono-poly(m;v)]) ≡ imonomial-term(m) (*) ipolynomial-term([u / v])
BY
{ (RWW "-2 -1 -3" 0
   THEN Auto
   THEN GenConclTerms Auto [⌜imonomial-term(m)⌝;⌜imonomial-term(u)⌝;⌜ipolynomial-term(v)⌝]⋅
   THEN All Thin) }

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

---

Latex:

---

Latex:

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)
6.  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
          ipolynomial-term([m  /  p])  \mequiv{}  imonomial-term(m)  (+)  ipolynomial-term(p)
7.  \mforall{}[m1,m2:iMonomial()].
          imonomial-term(mul-monomials(m1;m2))  \mequiv{}  imonomial-term(m1)  (*)  imonomial-term(m2)
\mvdash{}  ipolynomial-term([mul-monomials(m;u)  /  mul-mono-poly(m;v)])  \mequiv{}  imonomial-term(m)
(*)  ipolynomial-term([u  /  v])


By

---

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

---

Home Index