### Nuprl Lemma : imonomial-term-linear-ringeq

`∀r:Rng. ∀f:ℤ ⟶ |r|. ∀ws:ℤ List. ∀c:ℤ.  (ring_term_value(f;imonomial-term(<c, ws>)) = (int-to-ring(r;c) * ring_term_valu\000Ce(f;imonomial-term(<1, ws>))) ∈ |r|)`

Proof

Definitions occuring in Statement :  ring_term_value: `ring_term_value(f;t)` int-to-ring: `int-to-ring(r;n)` rng: `Rng` rng_times: `*` rng_car: `|r|` imonomial-term: `imonomial-term(m)` list: `T List` infix_ap: `x f y` all: `∀x:A. B[x]` function: `x:A ⟶ B[x]` pair: `<a, b>` natural_number: `\$n` int: `ℤ` equal: `s = t ∈ T`
Definitions unfolded in proof :  top: `Top` implies: `P `` Q` rev_implies: `P `` Q` and: `P ∧ Q` iff: `P `⇐⇒` Q` guard: `{T}` uimplies: `b supposing a` subtype_rel: `A ⊆r B` true: `True` so_apply: `x[s1;s2]` so_lambda: `λ2x y.t[x; y]` rng: `Rng` prop: `ℙ` uall: `∀[x:A]. B[x]` squash: `↓T` member: `t ∈ T` imonomial-term: `imonomial-term(m)` all: `∀x:A. B[x]`
Lemmas referenced :  rng_wf list_wf ring_term_value_const_lemma iff_weakening_equal itermVar_wf itermMultiply_wf int_term_wf list_accum_wf ring_term_value_wf int-to-ring_wf rng_times_wf infix_ap_wf itermConstant_wf imonomial-ringeq-lemma rng_car_wf true_wf squash_wf equal_wf
Rules used in proof :  functionEquality voidEquality voidElimination isect_memberEquality independent_functionElimination productElimination independent_isectElimination baseClosed imageMemberEquality natural_numberEquality intEquality functionExtensionality because_Cache dependent_functionElimination rename setElimination universeEquality equalitySymmetry hypothesis equalityTransitivity hypothesisEquality isectElimination extract_by_obid introduction imageElimination sqequalHypSubstitution lambdaEquality thin applyEquality sqequalRule cut lambdaFormation sqequalReflexivity computationStep sqequalTransitivity sqequalSubstitution

Latex:
\mforall{}r:Rng.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  |r|.  \mforall{}ws:\mBbbZ{}  List.  \mforall{}c:\mBbbZ{}.
(ring\_term\_value(f;imonomial-term(<c,  ws>))  =  (int-to-ring(r;c)  *  ring\_term\_value(f;imonomial-term\000C(ə,  ws>))))

Date html generated: 2018_05_21-PM-03_16_24
Last ObjectModification: 2018_01_25-PM-02_19_31

Theory : rings_1

Home Index