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: y all: x:A. B[x] equal: 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 ⊆B prop: infix_ap: 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