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