Nuprl Lemma : mod_action_when_l
∀r:Rng. ∀m:r-Module. ∀u:|r|. ∀x:m.car. ∀b:𝔹. ((u m.act (when b. x)) = (when b. (u m.act x)) ∈ m.car)
Proof
Definitions occuring in Statement :
module: A-Module,
grp_of_module: m↓grp,
alg_act: a.act,
alg_car: a.car,
bool: 𝔹,
infix_ap: x f y,
all: ∀x:A. B[x],
equal: s = t ∈ T,
rng: Rng,
rng_car: |r|,
mon_when: when b. p
Definitions unfolded in proof :
all: ∀x:A. B[x],
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|,
uall: ∀[x:A]. B[x],
member: t ∈ T,
rng: Rng,
module: A-Module,
monoid_hom: MonHom(M1,M2),
subtype_rel: A ⊆r B,
prop: ℙ,
infix_ap: x f y
Lemmas referenced :
mon_when_hom_swap,
grp_of_module_wf,
rng_car_wf,
module_act_is_grp_hom,
alg_act_wf,
alg_car_wf,
monoid_hom_p_wf,
bool_wf,
module_wf,
rng_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
dependent_functionElimination,
setElimination,
rename,
hypothesisEquality,
hypothesis,
because_Cache,
dependent_set_memberEquality,
applyEquality,
lambdaEquality,
functionEquality,
equalitySymmetry
Latex:
\mforall{}r:Rng. \mforall{}m:r-Module. \mforall{}u:|r|. \mforall{}x:m.car. \mforall{}b:\mBbbB{}. ((u m.act (when b. x)) = (when b. (u m.act x)))
Date html generated:
2016_05_16-AM-08_12_24
Last ObjectModification:
2015_12_28-PM-06_06_31
Theory : list_3
Home
Index