Nuprl Lemma : imonomial-term-add-ringeq
∀r:Rng. ∀vs:ℤ List. ∀a,b:ℤ-o. ∀f:ℤ ⟶ |r|. ((ring_term_value(f;imonomial-term(<a, vs>)) +r ring_term_value(f;imonomial-\000Cterm(<b, vs>))) = ring_term_value(f;imonomial-term(<a + b, vs>)) ∈ |r|)
Proof
Definitions occuring in Statement :
ring_term_value: ring_term_value(f;t),
rng: Rng,
rng_plus: +r,
rng_car: |r|,
imonomial-term: imonomial-term(m),
list: T List,
int_nzero: ℤ-o,
infix_ap: x f y,
all: ∀x:A. B[x],
function: x:A ⟶ B[x],
pair: <a, b>,
add: n + m,
int: ℤ,
equal: s = t ∈ T
Definitions unfolded in proof :
implies: P ⇒ Q,
rev_implies: P ⇐ Q,
and: P ∧ Q,
iff: P ⇐⇒ Q,
guard: {T},
uimplies: b supposing a,
subtype_rel: A ⊆r B,
infix_ap: x f y,
squash: ↓T,
true: True,
int_nzero: ℤ-o,
rng: Rng,
uall: ∀[x:A]. B[x],
member: t ∈ T,
all: ∀x:A. B[x],
prop: ℙ
Lemmas referenced :
rng_times_over_plus,
iff_weakening_equal,
int-to-ring-add,
imonomial-term_wf,
ring_term_value_wf,
int-to-ring_wf,
rng_times_wf,
infix_ap_wf,
equal_wf,
rng_plus_wf,
rng_wf,
list_wf,
int_nzero_wf,
rng_car_wf,
squash_wf,
true_wf,
imonomial-term-linear-ringeq
Rules used in proof :
independent_functionElimination,
productElimination,
independent_isectElimination,
equalitySymmetry,
equalityTransitivity,
baseClosed,
imageMemberEquality,
sqequalRule,
independent_pairEquality,
functionExtensionality,
imageElimination,
lambdaEquality,
applyEquality,
natural_numberEquality,
addEquality,
because_Cache,
hypothesisEquality,
rename,
setElimination,
thin,
isectElimination,
sqequalHypSubstitution,
extract_by_obid,
introduction,
intEquality,
functionEquality,
hypothesis,
cut,
lambdaFormation,
sqequalReflexivity,
computationStep,
sqequalTransitivity,
sqequalSubstitution,
universeEquality,
dependent_functionElimination
Latex:
\mforall{}r:Rng. \mforall{}vs:\mBbbZ{} List. \mforall{}a,b:\mBbbZ{}\msupminus{}\msupzero{}. \mforall{}f:\mBbbZ{} {}\mrightarrow{} |r|.
((ring\_term\_value(f;imonomial-term(<a, vs>)) +r ring\_term\_value(f;imonomial-term(<b, vs>))) = ring\000C\_term\_value(f;imonomial-term(<a + b, vs>)))
Date html generated:
2018_05_21-PM-03_16_28
Last ObjectModification:
2018_01_25-PM-02_19_38
Theory : rings_1
Home
Index