### Nuprl Lemma : mul-monomials-ringeq

`∀[r:CRng]. ∀[m1,m2:iMonomial()].  imonomial-term(mul-monomials(m1;m2)) ≡ imonomial-term(m1) (*) imonomial-term(m2)`

Proof

Definitions occuring in Statement :  ringeq_int_terms: `t1 ≡ t2` crng: `CRng` mul-monomials: `mul-monomials(m1;m2)` imonomial-term: `imonomial-term(m)` iMonomial: `iMonomial()` itermMultiply: `left (*) right` uall: `∀[x:A]. B[x]`
Definitions unfolded in proof :  iMonomial: `iMonomial()` mul-monomials: `mul-monomials(m1;m2)` has-value: `(a)↓` uall: `∀[x:A]. B[x]` member: `t ∈ T` uimplies: `b supposing a` int_nzero: `ℤ-o` ringeq_int_terms: `t1 ≡ t2` all: `∀x:A. B[x]` top: `Top` crng: `CRng` rng: `Rng` true: `True` squash: `↓T` prop: `ℙ` infix_ap: `x f y` subtype_rel: `A ⊆r B` guard: `{T}` iff: `P `⇐⇒` Q` and: `P ∧ Q` rev_implies: `P `` Q` implies: `P `` Q` so_lambda: `λ2x.t[x]` so_apply: `x[s]` merge-int: `merge-int(as;bs)` imonomial-term: `imonomial-term(m)` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` ring_term_value: `ring_term_value(f;t)` insert-int: `insert-int(x;l)` so_lambda: `so_lambda(x,y,z.t[x; y; z])` so_apply: `x[s1;s2;s3]` itermConstant: `"const"` int_term_ind: int_term_ind itermMultiply: `left (*) right` itermVar: `vvar` bool: `𝔹` unit: `Unit` it: `⋅` btrue: `tt` uiff: `uiff(P;Q)` less_than: `a < b` less_than': `less_than'(a;b)` not: `¬A` false: `False` bfalse: `ff` exists: `∃x:A. B[x]` or: `P ∨ Q` sq_type: `SQType(T)` bnot: `¬bb` ifthenelse: `if b then t else f fi ` assert: `↑b`
Lemmas referenced :  value-type-has-value int-value-type list_wf list-value-type merge-int-accum_wf ring_term_value_mul_lemma rng_car_wf rng_times_wf iMonomial_wf crng_wf equal_wf squash_wf true_wf imonomial-term-linear-ringeq subtype_rel_self iff_weakening_equal merge-int-accum-sq int-to-ring_wf ring_term_value_wf imonomial-term_wf list_induction all_wf merge-int_wf infix_ap_wf reduce_nil_lemma list_accum_nil_lemma ring_term_value_const_lemma list_accum_wf int_term_wf itermConstant_wf itermMultiply_wf itermVar_wf rng_times_one int-to-ring-one reduce_cons_lemma insert-int_wf cons_wf list_ind_nil_lemma list_accum_cons_lemma crng_times_comm list_ind_cons_lemma lt_int_wf bool_wf eqtt_to_assert assert_of_lt_int top_wf less_than_wf eqff_to_assert bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot imonomial-cons-ringeq crng_times_ac_1 int-to-ring-mul rng_times_assoc
Rules used in proof :  sqequalHypSubstitution sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity productElimination thin sqequalRule callbyvalueReduce cut introduction extract_by_obid isectElimination intEquality independent_isectElimination hypothesis multiplyEquality setElimination rename hypothesisEquality lambdaFormation dependent_functionElimination isect_memberEquality voidElimination voidEquality functionEquality because_Cache natural_numberEquality isect_memberFormation lambdaEquality axiomEquality applyEquality imageElimination equalityTransitivity equalitySymmetry universeEquality imageMemberEquality baseClosed instantiate independent_functionElimination independent_pairEquality functionExtensionality unionElimination equalityElimination lessCases sqequalAxiom independent_pairFormation dependent_pairFormation promote_hyp cumulativity equalityUniverse levelHypothesis

Latex:
\mforall{}[r:CRng].  \mforall{}[m1,m2:iMonomial()].
imonomial-term(mul-monomials(m1;m2))  \mequiv{}  imonomial-term(m1)  (*)  imonomial-term(m2)

Date html generated: 2018_05_21-PM-03_17_03
Last ObjectModification: 2018_05_19-AM-08_08_12

Theory : rings_1

Home Index