---

Step * 1 2 of Lemma mul-monomials-ringeq


1. r : CRng
2. m5 : ℤ-o
3. m6 : {vs:ℤ List| sorted(vs)} 
4. m3 : ℤ-o
5. m4 : {vs:ℤ List| sorted(vs)} 
6. f : ℤ ⟶ |r|
7. ring_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (ring_term_value(f;imonomial-term(<1, m6>)) * ring_term_va\000Clue(f;imonomial-term(<1, m4>))) ∈ |r|
⊢ (int-to-ring(r;m5 * m3) * (ring_term_value(f;imonomial-term(<1, m6>)) * ring_term_value(f;imonomial-term(<1, 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|
BY
{ ((RWO "int-to-ring-mul" 0 THENA Auto)
   THEN GenConclTerms Auto [⌜ring_term_value(f;imonomial-term(<1, m6>))⌝
                      ;⌜ring_term_value(f;imonomial-term(<1, m4>))⌝
                      ; int-to-ring(r;m5)
                      ; int-to-ring(r;m3)]⋅
   THEN All Thin) }

1
1. r : CRng
2. v : |r|
3. v1 : |r|
4. v2 : |r|
5. v3 : |r|
⊢ ((v2 * v3) * (v * v1)) = ((v2 * v) * (v3 * v1)) ∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  m5  :  \mBbbZ{}\msupminus{}\msupzero{}
3.  m6  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
4.  m3  :  \mBbbZ{}\msupminus{}\msupzero{}
5.  m4  :  \{vs:\mBbbZ{}  List|  sorted(vs)\} 
6.  f  :  \mBbbZ{}  {}\mrightarrow{}  |r|
7.  ring\_term\_value(f;imonomial-term(ə,  merge-int(m6;m4)>))  =  (ring\_term\_value(f;imonomial-term(ə,  \000Cm6>))  *  ring\_term\_value(f;imonomial-term(ə,  m4>)))
\mvdash{}  (int-to-ring(r;m5  *  m3)  *  (ring\_term\_value(f;imonomial-term(ə,  m6>))  *  ring\_term\_value(f;imonomia\000Cl-term(ə,  m4>))))
=  ((int-to-ring(r;m5)  *  ring\_term\_value(f;imonomial-term(ə,  m6>)))  *  (int-to-ring(r;m3)  *  ring\_term\000C\_value(f;imonomial-term(ə,  m4>))))


By

---

Latex:
((RWO  "int-to-ring-mul"  0  THENA  Auto)
  THEN  GenConclTerms  Auto  [\mkleeneopen{}ring\_term\_value(f;imonomial-term(ə,  m6>))\mkleeneclose{}
                                        ;\mkleeneopen{}ring\_term\_value(f;imonomial-term(ə,  m4>))\mkleeneclose{}
                                        ;  int-to-ring(r;m5)
                                        ;  int-to-ring(r;m3)]\mcdot{}
  THEN  All  Thin)

---

Home Index