Nuprl Lemma : rng_sum_split

[r:Rng]. ∀[a,b,c:ℤ].
  (∀[E:{a..c-} ⟶ |r|]. ((Σ(r) a ≤ j < c. E[j]) ((Σ(r) a ≤ j < b. E[j]) +r (r) b ≤ j < c. E[j])) ∈ |r|)) supposing 
     ((b ≤ c) and 
     (a ≤ b))


Definitions occuring in Statement :  rng_sum: rng_sum rng: Rng rng_plus: +r rng_car: |r| int_seg: {i..j-} uimplies: supposing a uall: [x:A]. B[x] infix_ap: y so_apply: x[s] le: A ≤ B function: x:A ⟶ B[x] int: equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B grp: Group{i} mon: Mon imon: IMonoid prop: rng_sum: rng_sum add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) uimplies: supposing a rng: Rng
Lemmas referenced :  mon_itop_split add_grp_of_rng_wf_a grp_sig_wf monoid_p_wf grp_car_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf int_seg_wf rng_car_wf le_wf rng_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut lemma_by_obid sqequalHypSubstitution isectElimination thin hypothesisEquality hypothesis applyEquality sqequalRule lambdaEquality setElimination rename setEquality cumulativity isect_memberEquality axiomEquality functionEquality equalityTransitivity equalitySymmetry intEquality

\mforall{}[r:Rng].  \mforall{}[a,b,c:\mBbbZ{}].
    (\mforall{}[E:\{a..c\msupminus{}\}  {}\mrightarrow{}  |r|]
          ((\mSigma{}(r)  a  \mleq{}  j  <  c.  E[j])  =  ((\mSigma{}(r)  a  \mleq{}  j  <  b.  E[j])  +r  (\mSigma{}(r)  b  \mleq{}  j  <  c.  E[j]))))  supposing 
          ((b  \mleq{}  c)  and 
          (a  \mleq{}  b))

Date html generated: 2016_05_15-PM-00_28_14
Last ObjectModification: 2015_12_26-PM-11_58_15

Theory : rings_1

Home Index