---

Step * of Lemma mul-monomials-ringeq

∀[r:CRng]. ∀[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)
BY
{ xxx((UnivCD THENA Auto)
      THEN D 3
      THEN D 2
      THEN RepUR ``mul-monomials`` 0
      THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))
      THEN xxx(D 0 THEN Reduce 0 THEN Auto THEN (RWO "imonomial-term-linear-ringeq" 0 THENA Auto))xxx)xxx }

1
1. r : CRng
2. m5 : ℤ-o
3. m6 : {vs:ℤ List| sorted(vs)} 
4. m3 : ℤ-o
5. m4 : {vs:ℤ List| sorted(vs)} 
6. f : ℤ ⟶ |r|
⊢ (int-to-ring(r;m5 * m3) * ring_term_value(f;imonomial-term(<1, merge-int-accum(m6;m4)>)))
= ((int-to-ring(r;m5) * ring_term_value(f;imonomial-term(<1, m6>))) * (int-to-ring(r;m3) * ring_term_value(f;imonomial-t\000Cerm(<1, m4>))))
∈ |r|

---

Latex:

---

Latex:
\mforall{}[r:CRng].  \mforall{}[m1,m2:iMonomial()].
    imonomial-term(mul-monomials(m1;m2))  \mequiv{}  imonomial-term(m1)  (*)  imonomial-term(m2)


By

---

Latex:
xxx((UnivCD  THENA  Auto)
        THEN  D  3
        THEN  D  2
        THEN  RepUR  ``mul-monomials``  0
        THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto))
        THEN  xxx(D  0
                          THEN  Reduce  0
                          THEN  Auto
                          THEN  (RWO  "imonomial-term-linear-ringeq"  0  THENA  Auto))xxx)xxx

---

Home Index