### Nuprl Lemma : rng_mssum_functionality_wrt_bsubmset

`∀s:DSet. ∀r:Rng. ∀f,f':|s| ⟶ |r|. ∀p,q:MSet{s}.`
`  ((∀x:|s|. ((↑(x ∈b q - p)) `` (f'[x] = 0 ∈ |r|)))`
`  `` (↑(p ⊆b q))`
`  `` (∀x:|s|. ((↑(x ∈b p)) `` (f[x] = f'[x] ∈ |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: `a - b` mset_mem: mset_mem mset: `MSet{s}` assert: `↑b` so_apply: `x[s]` all: `∀x:A. B[x]` implies: `P `` Q` function: `x:A ⟶ B[x]` equal: `s = 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 ⊆r B` abgrp: `AbGrp` grp: `Group{i}` mon: `Mon` iabmonoid: `IAbMonoid` imon: `IMonoid` prop: `ℙ` so_lambda: `λ2x.t[x]` so_apply: `x[s]` uimplies: `b supposing a` implies: `P `` 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_functionality_wrt_bsubmset 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,f':|s|  {}\mrightarrow{}  |r|.  \mforall{}p,q:MSet\{s\}.
((\mforall{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  q  -  p))  {}\mRightarrow{}  (f'[x]  =  0)))
{}\mRightarrow{}  (\muparrow{}(p  \msubseteq{}\msubb{}  q))
{}\mRightarrow{}  (\mforall{}x:|s|.  ((\muparrow{}(x  \mmember{}\msubb{}  p))  {}\mRightarrow{}  (f[x]  =  f'[x])))
{}\mRightarrow{}  ((\mSigma{}x  \mmember{}  p.  f[x])  =  (\mSigma{}x  \mmember{}  q.  f'[x])))

Date html generated: 2016_05_16-AM-08_11_52
Last ObjectModification: 2015_12_28-PM-06_06_24

Theory : list_3

Home Index