Nuprl Lemma : omral_alg_wf2
∀g:OCMon. ∀r:CDRng. (omral_alg(g;r) ∈ CAlg(r))
Proof
Definitions occuring in Statement :
omral_alg: omral_alg(g;r),
calgebra: CAlg(A),
all: ∀x:A. B[x],
member: t ∈ T,
cdrng: CDRng,
ocmon: OCMon
Definitions unfolded in proof :
all: ∀x:A. B[x],
member: t ∈ T,
calgebra: CAlg(A),
algebra: algebra{i:l}(A),
module: A-Module,
and: P ∧ Q,
cand: A c∧ B,
uall: ∀[x:A]. B[x],
cdrng: CDRng,
crng: CRng,
rng: Rng,
prop: ℙ,
so_lambda: λ2x.t[x],
so_apply: x[s],
grp_car: |g|,
pi1: fst(t),
add_grp_of_rng: r↓+gp,
rng_car: |r|,
grp_eq: =b,
pi2: snd(t),
rng_eq: =b,
abdgrp: AbDGrp,
abgrp: AbGrp,
grp: Group{i},
mon: Mon,
subtype_rel: A ⊆r B,
ocmon: OCMon,
omon: OMon,
abmonoid: AbMon,
so_lambda: λ2x y.t[x; y],
so_apply: x[s1;s2],
implies: P ⇒ Q,
bool: 𝔹,
unit: Unit,
it: ⋅,
btrue: tt,
band: p ∧b q,
ifthenelse: if b then t else f fi ,
uiff: uiff(P;Q),
uimplies: b supposing a,
bfalse: ff,
infix_ap: x f y,
oal_grp: oal_grp(s;g),
grp_op: *,
grp_id: e,
grp_inv: ~,
omral_alg: omral_alg(g;r),
alg_car: a.car,
alg_plus: a.plus,
alg_zero: a.zero,
alg_minus: a.minus,
omral_minus: --ps,
omral_zero: 00g,r,
omral_plus: ps ++ qs,
omralist: omral(g;r),
monoid_p: IsMonoid(T;op;id),
group_p: IsGroup(T;op;id;inv),
oset_of_ocmon: g↓oset,
comm: Comm(T;op),
oalist: oal(a;b),
dset_set: dset_set,
mk_dset: mk_dset(T, eq),
set_car: |p|,
dset_list: s List,
set_prod: s × t,
dset_of_mon: g↓set,
action_p: IsAction(A;x;e;S;f),
inverse: Inverse(T;op;id;inv),
ident: Ident(T;op;id),
assoc: Assoc(T;op),
alg_act: a.act,
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f),
dset: DSet,
alg_times: a.times,
alg_one: a.one,
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op)
Lemmas referenced :
group_p_wf,
alg_car_wf,
rng_car_wf,
alg_plus_wf,
alg_zero_wf,
alg_minus_wf,
comm_wf,
action_p_wf,
rng_times_wf,
rng_one_wf,
alg_act_wf,
bilinear_p_wf,
rng_plus_wf,
monoid_p_wf,
alg_times_wf,
alg_one_wf,
bilinear_wf,
all_wf,
dist_1op_2op_lr_wf,
cdrng_wf,
ocmon_wf,
omral_alg_wf,
cdrng_properties,
add_grp_of_rng_wf_b,
eqfun_p_wf,
grp_car_wf,
grp_eq_wf,
oal_grp_wf,
oset_of_ocmon_wf,
subtype_rel_sets,
abmonoid_wf,
ulinorder_wf,
assert_wf,
infix_ap_wf,
bool_wf,
grp_le_wf,
equal_wf,
eqtt_to_assert,
cancel_wf,
grp_op_wf,
uall_wf,
monot_wf,
grp_properties,
mon_properties,
omral_plus_comm,
omral_action_times,
omral_action_one,
omral_action_plus_l,
set_car_wf,
omralist_wf,
dset_wf,
omral_action_plus_r,
omral_times_assoc,
omral_times_ident_r,
omral_times_ident_l,
omral_bilinear,
omral_action_times_r1,
omral_action_times_r2,
omral_times_comm_a
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
dependent_set_memberEquality,
independent_pairFormation,
hypothesis,
productEquality,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
dependent_functionElimination,
setElimination,
rename,
because_Cache,
hypothesisEquality,
sqequalRule,
lambdaEquality,
applyEquality,
instantiate,
cumulativity,
universeEquality,
functionEquality,
unionElimination,
equalityElimination,
productElimination,
independent_isectElimination,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
setEquality,
applyLambdaEquality,
isect_memberFormation,
isect_memberEquality,
axiomEquality,
independent_pairEquality
Latex:
\mforall{}g:OCMon. \mforall{}r:CDRng. (omral\_alg(g;r) \mmember{} CAlg(r))
Date html generated:
2017_10_01-AM-10_07_14
Last ObjectModification:
2017_03_03-PM-01_16_29
Theory : polynom_3
Home
Index