### Nuprl Lemma : mul-ipoly-ringeq

`∀r:CRng. ∀p,q:iMonomial() List.  ipolynomial-term(mul-ipoly(p;q)) ≡ ipolynomial-term(p) (*) ipolynomial-term(q)`

Proof

Definitions occuring in Statement :  ringeq_int_terms: `t1 ≡ t2` crng: `CRng` mul-ipoly: `mul-ipoly(p;q)` ipolynomial-term: `ipolynomial-term(p)` iMonomial: `iMonomial()` itermMultiply: `left (*) right` list: `T List` all: `∀x:A. B[x]`
Definitions unfolded in proof :  all: `∀x:A. B[x]` member: `t ∈ T` uall: `∀[x:A]. B[x]` or: `P ∨ Q` mul-ipoly: `mul-ipoly(p;q)` uimplies: `b supposing a` callbyvalueall: callbyvalueall has-value: `(a)↓` has-valueall: `has-valueall(a)` ifthenelse: `if b then t else f fi ` btrue: `tt` cons: `[a / b]` iMonomial: `iMonomial()` so_lambda: `λ2x.t[x]` prop: `ℙ` so_apply: `x[s]` implies: `P `` Q` int_nzero: `ℤ-o` top: `Top` so_lambda: `λ2x y.t[x; y]` so_apply: `x[s1;s2]` bfalse: `ff` ipolynomial-term: `ipolynomial-term(p)` null: `null(as)` nil: `[]` it: `⋅` itermConstant: `"const"` ringeq_int_terms: `t1 ≡ t2` crng: `CRng` rng: `Rng` and: `P ∧ Q` bool: `𝔹` unit: `Unit` uiff: `uiff(P;Q)` exists: `∃x:A. B[x]` sq_type: `SQType(T)` guard: `{T}` bnot: `¬bb` assert: `↑b` false: `False` not: `¬A` rev_uimplies: `rev_uimplies(P;Q)` true: `True` squash: `↓T` infix_ap: `x f y` subtype_rel: `A ⊆r B` iff: `P `⇐⇒` Q` rev_implies: `P `` Q`
Lemmas referenced :  iMonomial_wf list-cases valueall-type-has-valueall list_wf list-valueall-type void-valueall-type nil_wf evalall-reduce null_nil_lemma product_subtype_list product-valueall-type int_nzero_wf sorted_wf subtype_rel_self set-valueall-type nequal_wf int-valueall-type cons_wf null_cons_lemma spread_cons_lemma crng_wf ring_term_value_const_lemma ring_term_value_mul_lemma rng_car_wf rng_times_zero ring_term_value_wf ipolynomial-term_wf int-to-ring-zero null_wf bool_wf eqtt_to_assert assert_of_null eqff_to_assert equal_wf bool_cases_sqequal subtype_base_sq bool_subtype_base assert-bnot equal-wf-T-base btrue_wf and_wf bfalse_wf btrue_neq_bfalse ipolynomial-term-cons-ringeq eager-accum_wf mul-mono-poly_wf1 add-ipoly_wf1 itermMultiply_wf itermAdd_wf imonomial-term_wf int_term_wf ring_term_value_add_lemma rng_times_over_plus ringeq_int_terms_functionality ringeq_int_terms_weakening itermMultiply_functionality_wrt_ringeq mul-mono-poly-ringeq ringeq_int_terms_transitivity itermAdd_functionality_wrt_ringeq list_induction all_wf ringeq_int_terms_wf list_accum_wf list_accum_nil_lemma list_accum_cons_lemma rng_plus_wf squash_wf true_wf rng_plus_zero iff_weakening_equal add-ipoly-ringeq rng_times_wf rng_plus_assoc rng_plus_ac_1 rng_plus_comm eager-accum-list_accum
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid hypothesis sqequalHypSubstitution isectElimination thin dependent_functionElimination hypothesisEquality unionElimination sqequalRule voidEquality independent_isectElimination callbyvalueReduce promote_hyp hypothesis_subsumption productElimination lambdaEquality setEquality intEquality because_Cache independent_functionElimination natural_numberEquality isect_memberEquality voidElimination functionEquality setElimination rename equalitySymmetry equalityElimination equalityTransitivity dependent_pairFormation instantiate cumulativity baseClosed dependent_set_memberEquality independent_pairFormation applyLambdaEquality independent_pairEquality applyEquality imageElimination universeEquality imageMemberEquality

Latex:
\mforall{}r:CRng.  \mforall{}p,q:iMonomial()  List.
ipolynomial-term(mul-ipoly(p;q))  \mequiv{}  ipolynomial-term(p)  (*)  ipolynomial-term(q)

Date html generated: 2018_05_21-PM-03_17_17
Last ObjectModification: 2018_05_19-AM-08_08_31

Theory : rings_1

Home Index