Nuprl Lemma : rng_times_mssum_l

s:DSet. ∀r:Rng. ∀f:|s| ⟶ |r|. ∀u:|r|. ∀a:MSet{s}.  ((u x ∈ a. f[x])) x ∈ a. (u f[x])) ∈ |r|)


Proof




Definitions occuring in Statement :  rng_mssum: rng_mssum mset: MSet{s} infix_ap: y so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] equal: t ∈ T rng: Rng rng_times: * 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] dset: DSet so_lambda: λ2x.t[x] so_apply: x[s] top: Top rng: Rng infix_ap: y implies:  Q iff: ⇐⇒ Q and: P ∧ Q rev_implies:  Q prop:
Lemmas referenced :  rng_times_lsum_l set_car_wf list_wf rng_mssum_elim_lemma all_mset_elim equal_wf rng_car_wf rng_times_wf rng_mssum_wf mset_wf sq_stable__equal all_wf rng_lsum_wf rng_wf dset_wf
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination setElimination rename hypothesis sqequalRule lambdaEquality applyEquality because_Cache addLevel isect_memberEquality voidElimination voidEquality independent_functionElimination productElimination levelHypothesis functionEquality

Latex:
\mforall{}s:DSet.  \mforall{}r:Rng.  \mforall{}f:|s|  {}\mrightarrow{}  |r|.  \mforall{}u:|r|.  \mforall{}a:MSet\{s\}.    ((u  *  (\mSigma{}x  \mmember{}  a.  f[x]))  =  (\mSigma{}x  \mmember{}  a.  (u  *  f[x])))



Date html generated: 2018_05_22-AM-07_46_06
Last ObjectModification: 2018_05_19-AM-08_30_29

Theory : list_3


Home Index