Nuprl Lemma : mod_times_mssum_l

s:DSet. ∀r:Rng. ∀m:algebra{i:l}(r). ∀f:|s| ⟶ m.car. ∀u:m.car. ∀a:MSet{s}.
  ((u m.times x ∈ a. f[x])) x ∈ a. (u m.times f[x])) ∈ m.car)


Proof




Definitions occuring in Statement :  mod_mssum: mod_mssum mset: MSet{s} algebra: algebra{i:l}(A) alg_times: a.times alg_car: a.car infix_ap: y so_apply: x[s] all: x:A. B[x] function: x:A ⟶ B[x] equal: t ∈ T rng: Rng dset: DSet set_car: |p|
Definitions unfolded in proof :  all: x:A. B[x] mod_mssum: mod_mssum grp_of_module: m↓grp add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) rng_of_alg: a↓rg rng_car: |r| member: t ∈ T uall: [x:A]. B[x] rng: Rng algebra: algebra{i:l}(A) module: A-Module dset: DSet 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 infix_ap: y monoid_hom: MonHom(M1,M2) guard: {T} grp_op: * pi2: snd(t) rng_plus: +r squash: T and: P ∧ Q true: True iff: ⇐⇒ Q rev_implies:  Q
Lemmas referenced :  mset_wf alg_car_wf rng_car_wf set_car_wf algebra_wf rng_wf dset_wf dist_hom_over_mset_for grp_of_module_wf2 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 alg_times_wf monoid_hom_p_wf grp_of_module_wf grp_hom_formation grp_subtype_igrp abgrp_subtype_grp subtype_rel_transitivity abgrp_wf grp_wf igrp_wf equal_wf squash_wf true_wf algebra_bilinear infix_ap_wf alg_plus_wf iff_weakening_equal
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity lambdaFormation cut sqequalRule hypothesis introduction extract_by_obid sqequalHypSubstitution dependent_functionElimination thin hypothesisEquality isectElimination setElimination rename functionEquality applyEquality instantiate setEquality cumulativity because_Cache lambdaEquality independent_isectElimination functionExtensionality dependent_set_memberEquality imageElimination equalityTransitivity equalitySymmetry universeEquality productElimination natural_numberEquality imageMemberEquality baseClosed independent_functionElimination

Latex:
\mforall{}s:DSet.  \mforall{}r:Rng.  \mforall{}m:algebra\{i:l\}(r).  \mforall{}f:|s|  {}\mrightarrow{}  m.car.  \mforall{}u:m.car.  \mforall{}a:MSet\{s\}.
    ((u  m.times  (\mSigma{}m  x  \mmember{}  a.  f[x]))  =  (\mSigma{}m  x  \mmember{}  a.  (u  m.times  f[x])))



Date html generated: 2017_10_01-AM-10_01_01
Last ObjectModification: 2017_03_03-PM-01_03_37

Theory : list_3


Home Index