### Nuprl Lemma : mul-mono-poly-ringeq

`∀[r:CRng]. ∀[m:iMonomial()]. ∀[p:iMonomial() List].`
`  ipolynomial-term(mul-mono-poly(m;p)) ≡ imonomial-term(m) (*) ipolynomial-term(p)`

Proof

Definitions occuring in Statement :  ringeq_int_terms: `t1 ≡ t2` crng: `CRng` mul-mono-poly: `mul-mono-poly(m;p)` ipolynomial-term: `ipolynomial-term(p)` imonomial-term: `imonomial-term(m)` iMonomial: `iMonomial()` itermMultiply: `left (*) right` list: `T List` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` so_lambda: `λ2x.t[x]` iMonomial: `iMonomial()` int_nzero: `ℤ-o` crng: `CRng` so_apply: `x[s]` implies: `P `` Q` mul-mono-poly: `mul-mono-poly(m;p)` all: `∀x:A. B[x]` so_lambda: `so_lambda(x,y,z.t[x; y; z])` top: `Top` so_apply: `x[s1;s2;s3]` has-value: `(a)↓` uimplies: `b supposing a` prop: `ℙ` ringeq_int_terms: `t1 ≡ t2` rng: `Rng` ipolynomial-term: `ipolynomial-term(p)` ifthenelse: `if b then t else f fi ` btrue: `tt` and: `P ∧ Q` subtype_rel: `A ⊆r B` uiff: `uiff(P;Q)` rev_uimplies: `rev_uimplies(P;Q)`
Lemmas referenced :  list_induction ringeq_int_terms_wf ipolynomial-term_wf mul-mono-poly_wf1 itermMultiply_wf imonomial-term_wf list_wf iMonomial_wf list_ind_nil_lemma list_ind_cons_lemma value-type-has-value iMonomial-value-type mul-monomials_wf rng_car_wf crng_wf null_nil_lemma ring_term_value_const_lemma ring_term_value_mul_lemma rng_times_zero ring_term_value_wf int-to-ring-zero list-value-type equal_wf ipolynomial-term-cons-ringeq mul-monomials-ringeq cons_wf itermAdd_wf subtype_rel_product int_nzero_wf sorted_wf subtype_rel_self int_term_wf ringeq_int_terms_functionality ringeq_int_terms_transitivity itermAdd_functionality_wrt_ringeq itermMultiply_functionality_wrt_ringeq ringeq_int_terms_weakening ring_term_value_add_lemma rng_times_over_plus
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut thin extract_by_obid sqequalHypSubstitution isectElimination because_Cache sqequalRule lambdaEquality hypothesisEquality hypothesis productElimination independent_pairEquality setElimination rename independent_functionElimination dependent_functionElimination isect_memberEquality voidElimination voidEquality lambdaFormation callbyvalueReduce independent_isectElimination axiomEquality functionEquality intEquality equalitySymmetry equalityTransitivity applyEquality setEquality

Latex:
\mforall{}[r:CRng].  \mforall{}[m:iMonomial()].  \mforall{}[p:iMonomial()  List].
ipolynomial-term(mul-mono-poly(m;p))  \mequiv{}  imonomial-term(m)  (*)  ipolynomial-term(p)

Date html generated: 2018_05_21-PM-03_17_09
Last ObjectModification: 2018_05_19-AM-08_08_15

Theory : rings_1

Home Index