Nuprl Lemma : imonomial-ringeq-lemma

∀r:Rng. ∀f:ℤ ⟶ |r|. ∀ws:ℤ List. ∀t:int_term().
  (ring_term_value(f;accumulate (with value t and list item v):
                      t (*) vv
                     over list:
                       ws
                     with starting value:
                      t))
  = (ring_term_value(f;t) 
     * 
     ring_term_value(f;accumulate (with value t and list item v):
                        t (*) vv
                       over list:
                         ws
                       with starting value:
                        "1")))
  ∈ |r|)


Proof



Definitions occuring in Statement :  ring_term_value: ring_term_value(f;t),  rng: Rng,  rng_times: *,  rng_car: |r|,  itermMultiply: left (*) right,  itermVar: vvar,  itermConstant: "const",  int_term: int_term(),  list_accum: list_accum,  list: T List,  infix_ap: x f y,  all: ∀x:A. B[x],  function: x:A ⟶ B[x],  natural_number: $n,  int: ℤ,  equal: s = t ∈ T
Definitions unfolded in proof :  prop: ℙ,  itermConstant: "const",  itermVar: vvar,  int_term_ind: int_term_ind,  itermMultiply: left (*) right,  ring_term_value: ring_term_value(f;t),  rev_implies: P ⇐ Q,  and: P ∧ Q,  iff: P ⇐⇒ Q,  guard: {T},  uimplies: b supposing a,  subtype_rel: A ⊆r B,  true: True,  infix_ap: x f y,  squash: ↓T,  top: Top,  implies: P ⇒ Q,  so_apply: x[s],  so_apply: x[s1;s2],  so_lambda: λ2x y.t[x; y],  rng: Rng,  so_lambda: λ2x.t[x],  member: t ∈ T,  uall: ∀[x:A]. B[x],  all: ∀x:A. B[x]
Lemmas referenced :  rng_one_wf,  rng_times_one,  rng_wf,  iff_weakening_equal,  list_accum_cons_lemma,  ring_term_value_const_lemma,  list_accum_nil_lemma,  list_wf,  itermConstant_wf,  rng_times_wf,  infix_ap_wf,  itermVar_wf,  itermMultiply_wf,  list_accum_wf,  ring_term_value_wf,  rng_car_wf,  equal_wf,  int_term_wf,  all_wf,  list_induction,  squash_wf,  true_wf,  int-to-ring-one,  rng_times_assoc
Rules used in proof :  functionEquality,  productElimination,  independent_isectElimination,  equalitySymmetry,  equalityTransitivity,  baseClosed,  imageMemberEquality,  imageElimination,  voidEquality,  voidElimination,  isect_memberEquality,  dependent_functionElimination,  independent_functionElimination,  natural_numberEquality,  applyEquality,  functionExtensionality,  hypothesisEquality,  because_Cache,  rename,  setElimination,  hypothesis,  lambdaEquality,  sqequalRule,  intEquality,  isectElimination,  sqequalHypSubstitution,  extract_by_obid,  introduction,  thin,  cut,  lambdaFormation,  sqequalReflexivity,  computationStep,  sqequalTransitivity,  sqequalSubstitution,  universeEquality
Latex:
\mforall{}r:Rng.  \mforall{}f:\mBbbZ{}  {}\mrightarrow{}  |r|.  \mforall{}ws:\mBbbZ{}  List.  \mforall{}t:int\_term().
    (ring\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                            t  (*)  vv
                                          over  list:
                                              ws
                                          with  starting  value:
                                            t))
    =  (ring\_term\_value(f;t) 
          * 
          ring\_term\_value(f;accumulate  (with  value  t  and  list  item  v):
                                                t  (*)  vv
                                              over  list:
                                                  ws
                                              with  starting  value:
                                                "1"))))


Date html generated: 2018_05_21-PM-03_16_21
Last ObjectModification: 2018_01_25-PM-02_19_22

Theory : rings_1


Home Index