Step
*
1
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|
⊢ (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|
BY
{ (Assert ⌜ring_term_value(f;imonomial-term(<1, merge-int(m6;m4)>)) = (ring_term_value(f;imonomial-term(<1, m6>)) * ring\000C_term_value(f;imonomial-term(<1, m4>))) ∈ |r|⌝⋅
THENM ((Subst' merge-int-accum(m6;m4) ~ merge-int(m6;m4) 0 THENA Auto) THEN (RWO "-1" 0 THENA Auto))
) }
1
.....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|
2
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|
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|
\mvdash{} (int-to-ring(r;m5 * m3) * ring\_term\_value(f;imonomial-term(ə, merge-int-accum(m6;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:
(Assert \mkleeneopen{}ring\_term\_value(f;imonomial-term(ə, merge-int(m6;m4)>)) = (ring\_term\_value(f;imonomial-ter\000Cm(ə, m6>)) * ring\_term\_value(f;imonomial-term(ə, m4>)))\mkleeneclose{}\mcdot{}
THENM ((Subst' merge-int-accum(m6;m4) \msim{} merge-int(m6;m4) 0 THENA Auto) THEN (RWO "-1" 0 THENA Auto))
)
Home
Index