---

Step * 1 1 of Lemma mul-monomials-ringeq

.....assertion..... 
1. r : CRng
2. m5 : ℤ-o
3. m6 : {vs:ℤ List| sorted(vs)} 
4. m3 : ℤ-o
5. m4 : {vs:ℤ List| sorted(vs)} 
6. f : ℤ ⟶ |r|
⊢ ring_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (ring_term_value(f;imonomial-term(<1, m6>)) * ring_term_val\000Cue(f;imonomial-term(<1, m4>))) ∈ |r|
BY
{ (DSetVars THEN All Thin THEN RenameVar `bs' 3 THEN RenameVar `as' 2 THEN MoveToConcl 2 THEN ListInd 2) }

1
1. r : CRng
2. f : ℤ ⟶ |r|
⊢ ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;[])>)) = (ring_term_value(f;imonomial-term(<1, as>)) * \000Cring_term_value(f;imonomial-term(<1, []>))) ∈ |r|)

2
1. r : CRng
2. f : ℤ ⟶ |r|
3. u : ℤ
4. v : ℤ List
5. ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * \000Cring_term_value(f;imonomial-term(<1, v>))) ∈ |r|)
⊢ ∀as:ℤ List. (ring_term_value(f;imonomial-term(<1, merge-int(as;[u / v])>)) = (ring_term_value(f;imonomial-term(<1, as>\000C)) * ring_term_value(f;imonomial-term(<1, [u / v]>))) ∈ |r|)

---

Latex:

---

Latex:
.....assertion..... 
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|
\mvdash{}  ring\_term\_value(f;imonomial-term(ə,  merge-int(m6;m4)>))  =  (ring\_term\_value(f;imonomial-term(ə,  m\000C6>))  *  ring\_term\_value(f;imonomial-term(ə,  m4>)))


By

---

Latex:
(DSetVars
  THEN  All  Thin
  THEN  RenameVar  `bs'  3
  THEN  RenameVar  `as'  2
  THEN  MoveToConcl  2
  THEN  ListInd  2)

---

Home Index