Nuprl Lemma : rng_mssum_dom_shift

s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀p,q:MSet{s}.
  ((↑(p ⊆b q))  (∀x:|s|. ((↑(x ∈b p))  (f[x] 0 ∈ |r|)))  ((Σx ∈ p. f[x]) x ∈ q. f[x]) ∈ |r|))


Proof




Definitions occuring in Statement :  rng_mssum: rng_mssum bsubmset: a ⊆b b mset_diff: b mset_mem: mset_mem mset: MSet{s} assert: b so_apply: x[s] all: x:A. B[x] implies:  Q function: x:A ⟶ B[x] equal: t ∈ T rng: Rng rng_zero: 0 rng_car: |r| dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] member: t ∈ T uall: [x:A]. B[x] subtype_rel: A ⊆B abgrp: AbGrp grp: Group{i} mon: Mon iabmonoid: IAbMonoid imon: IMonoid prop: so_lambda: λ2x.t[x] so_apply: x[s] uimplies: supposing a implies:  Q rng_mssum: rng_mssum add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) grp_id: e pi2: snd(t)
Lemmas referenced :  mset_for_dom_shift add_grp_of_rng_wf_b subtype_rel_sets grp_sig_wf monoid_p_wf grp_car_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf comm_wf set_wf rng_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut lemma_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination hypothesis applyEquality sqequalRule instantiate setEquality cumulativity setElimination rename lambdaEquality independent_isectElimination

Latex:
\mforall{}s:DSet.  \mforall{}r:Rng.  \mforall{}f:|s|  {}\mrightarrow{}  |r|.  \mforall{}p,q:MSet\{s\}.
    ((\muparrow{}(p  \msubseteq{}\msubb{}  q))  {}\mRightarrow{}  (\mforall{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  q  -  p))  {}\mRightarrow{}  (f[x]  =  0)))  {}\mRightarrow{}  ((\mSigma{}x  \mmember{}  p.  f[x])  =  (\mSigma{}x  \mmember{}  q.  f[x])))



Date html generated: 2016_05_16-AM-08_12_02
Last ObjectModification: 2015_12_28-PM-06_06_21

Theory : list_3


Home Index