Nuprl Lemma : omral_fact_a
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|. (ps = (msFor{omral_alg(g;r)↓grp} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)
Proof
Definitions occuring in Statement :
omral_alg: omral_alg(g;r),
omral_inj: inj(k,v),
omral_dom: dom(ps),
omralist: omral(g;r),
lookup: as[k],
mset_for: mset_for,
grp_of_module: m↓grp,
all: ∀x:A. B[x],
equal: s = t ∈ T,
cdrng: CDRng,
rng_zero: 0,
oset_of_ocmon: g↓oset,
ocmon: OCMon,
set_car: |p|
Definitions unfolded in proof :
mset_for: mset_for,
mon_for: For{g} x ∈ as. f[x],
oset_of_ocmon: g↓oset,
dset_of_mon: g↓set,
set_car: |p|,
pi1: fst(t),
oal_mon: oal_mon(a;b),
grp_op: *,
pi2: snd(t),
grp_id: e,
grp_of_module: m↓grp,
add_grp_of_rng: r↓+gp,
rng_of_alg: a↓rg,
rng_plus: +r,
rng_zero: 0,
omral_alg: omral_alg(g;r),
alg_plus: a.plus,
alg_zero: a.zero,
omral_plus: ps ++ qs,
omral_zero: 00g,r
Lemmas referenced :
omral_fact
Rules used in proof :
sqequalSubstitution,
sqequalRule,
sqequalReflexivity,
sqequalTransitivity,
computationStep,
lemma_by_obid
Latex:
\mforall{}g:OCMon. \mforall{}r:CDRng. \mforall{}ps:|omral(g;r)|.
(ps = (msFor\{omral\_alg(g;r)\mdownarrow{}grp\} k' \mmember{} dom(ps). inj(k',ps[k'])))
Date html generated:
2016_05_16-AM-08_24_21
Last ObjectModification:
2015_12_28-PM-06_39_07
Theory : polynom_3
Home
Index