Nuprl Lemma : mod_action_when_r
∀r:Rng. ∀m:r-Module. ∀u:|r|. ∀x:m.car. ∀b:𝔹. (((when b. u) m.act 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_when: rng_when,
rng: Rng,
rng_car: |r|,
mon_when: when b. p
Definitions unfolded in proof :
all: ∀x:A. B[x],
rng_when: rng_when,
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,
infix_ap: x f y,
tlambda: λx:T. b[x],
monoid_hom: MonHom(M1,M2),
subtype_rel: A ⊆r B,
prop: ℙ
Lemmas referenced :
bool_wf,
alg_car_wf,
rng_car_wf,
module_wf,
rng_wf,
mon_when_hom_swap,
add_grp_of_rng_wf,
grp_of_module_wf,
module_act_grp_hom_l,
alg_act_wf,
grp_car_wf,
monoid_hom_p_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
sqequalRule,
hypothesis,
equalitySymmetry,
lemma_by_obid,
sqequalHypSubstitution,
dependent_functionElimination,
thin,
isectElimination,
setElimination,
rename,
hypothesisEquality,
dependent_set_memberEquality,
lambdaEquality,
applyEquality
Latex:
\mforall{}r:Rng. \mforall{}m:r-Module. \mforall{}u:|r|. \mforall{}x:m.car. \mforall{}b:\mBbbB{}. (((when b. u) m.act x) = (when b. (u m.act x)))
Date html generated:
2016_05_16-AM-08_12_26
Last ObjectModification:
2015_12_28-PM-06_06_33
Theory : list_3
Home
Index