Nuprl Lemma : mod_action_mssum_r
∀s:DSet. ∀r:Rng. ∀m:r-Module. ∀f:|s| ⟶ |r|. ∀u:m.car. ∀a:MSet{s}.
(((Σx ∈ a. f[x]) m.act u) = (Σm x ∈ a. (f[x] m.act u)) ∈ m.car)
Proof
Definitions occuring in Statement :
mod_mssum: mod_mssum,
rng_mssum: rng_mssum,
mset: MSet{s}
,
module: A-Module
,
alg_act: a.act
,
alg_car: a.car
,
infix_ap: x f y
,
so_apply: x[s]
,
all: ∀x:A. B[x]
,
function: x:A ⟶ B[x]
,
equal: s = t ∈ T
,
rng: Rng
,
rng_car: |r|
,
dset: DSet
,
set_car: |p|
Definitions unfolded in proof :
all: ∀x:A. B[x]
,
mod_mssum: mod_mssum,
rng_mssum: rng_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
,
module: A-Module
,
dset: DSet
,
infix_ap: x f y
,
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
,
tlambda: λx:T. b[x]
,
monoid_hom: MonHom(M1,M2)
Lemmas referenced :
mset_wf,
alg_car_wf,
rng_car_wf,
set_car_wf,
module_wf,
rng_wf,
dset_wf,
dist_hom_over_mset_for,
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,
grp_of_module_wf2,
module_act_grp_hom_l,
alg_act_wf,
add_grp_of_rng_wf,
monoid_hom_p_wf,
grp_of_module_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
hypothesisEquality,
isectElimination,
setElimination,
rename,
functionEquality,
applyEquality,
instantiate,
setEquality,
cumulativity,
lambdaEquality,
independent_isectElimination,
dependent_set_memberEquality
Latex:
\mforall{}s:DSet. \mforall{}r:Rng. \mforall{}m:r-Module. \mforall{}f:|s| {}\mrightarrow{} |r|. \mforall{}u:m.car. \mforall{}a:MSet\{s\}.
(((\mSigma{}x \mmember{} a. f[x]) m.act u) = (\mSigma{}m x \mmember{} a. (f[x] m.act u)))
Date html generated:
2016_05_16-AM-08_12_22
Last ObjectModification:
2015_12_28-PM-06_06_38
Theory : list_3
Home
Index