### 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