---

Step * 1 1 2 1 of Lemma mul-monomials-ringeq


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|)
6. as : ℤ List
7. ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * ring_term_val\000Cue(f;imonomial-term(<1, v>))) ∈ |r|
⊢ (int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>)))
= ((int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, as>))) * (int-to-ring(r;1) * ring_term_value(f;imonomial-ter\000Cm(<1, [u / v]>))))
∈ |r|
BY
{ (Assert ⌜ring_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>)) = ((f u) * ring_term_value(f;imonomial-\000Cterm(<1, merge-int(as;v)>))) ∈ |r|⌝⋅
   THENA ((GenConclTerm ⌜merge-int(as;v)⌝⋅ THENA Auto) THEN All Thin)
   ) }

1
1. r : CRng
2. f : ℤ ⟶ |r|
3. u : ℤ
4. v1 : ℤ List
⊢ ring_term_value(f;imonomial-term(<1, insert-int(u;v1)>)) = ((f u) * ring_term_value(f;imonomial-term(<1, v1>))) ∈ |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|)
6. as : ℤ List
7. ring_term_value(f;imonomial-term(<1, merge-int(as;v)>)) = (ring_term_value(f;imonomial-term(<1, as>)) * ring_term_val\000Cue(f;imonomial-term(<1, v>))) ∈ |r|
8. ring_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>)) = ((f u) * ring_term_value(f;imonomial-term(<1,\000C merge-int(as;v)>))) ∈ |r|
⊢ (int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, insert-int(u;merge-int(as;v))>)))
= ((int-to-ring(r;1) * ring_term_value(f;imonomial-term(<1, as>))) * (int-to-ring(r;1) * ring_term_value(f;imonomial-ter\000Cm(<1, [u / v]>))))
∈ |r|

---

Latex:

---

Latex:

1.  r  :  CRng
2.  f  :  \mBbbZ{}  {}\mrightarrow{}  |r|
3.  u  :  \mBbbZ{}
4.  v  :  \mBbbZ{}  List
5.  \mforall{}as:\mBbbZ{}  List.  (ring\_term\_value(f;imonomial-term(ə,  merge-int(as;v)>))  =  (ring\_term\_value(f;imonomi\000Cal-term(ə,  as>))  *  ring\_term\_value(f;imonomial-term(ə,  v>))))
6.  as  :  \mBbbZ{}  List
7.  ring\_term\_value(f;imonomial-term(ə,  merge-int(as;v)>))  =  (ring\_term\_value(f;imonomial-term(ə,  a\000Cs>))  *  ring\_term\_value(f;imonomial-term(ə,  v>)))
\mvdash{}  (int-to-ring(r;1)  *  ring\_term\_value(f;imonomial-term(ə,  insert-int(u;merge-int(as;v))>)))
=  ((int-to-ring(r;1)  *  ring\_term\_value(f;imonomial-term(ə,  as>))) 
      * 
      (int-to-ring(r;1)  *  ring\_term\_value(f;imonomial-term(ə,  [u  /  v]>))))


By

---

Latex:
(Assert  \mkleeneopen{}ring\_term\_value(f;imonomial-term(ə,  insert-int(u;merge-int(as;v))>))
                  =  ((f  u)  *  ring\_term\_value(f;imonomial-term(ə,  merge-int(as;v)>)))\mkleeneclose{}\mcdot{}
  THENA  ((GenConclTerm  \mkleeneopen{}merge-int(as;v)\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Thin)
  )

---

Home Index