Nuprl Lemma : rng_to_alg_wf
∀R:CRng. (rng_to_alg(R) ∈ algebra{i:l}(R))
Proof
Definitions occuring in Statement :
rng_to_alg: rng_to_alg(r),
algebra: algebra{i:l}(A),
all: ∀x:A. B[x],
member: t ∈ T,
crng: CRng
Definitions unfolded in proof :
all: ∀x:A. B[x],
uall: ∀[x:A]. B[x],
member: t ∈ T,
crng: CRng,
algebra: algebra{i:l}(A),
module: A-Module,
rng: Rng,
rng_to_alg: rng_to_alg(r),
algebra_sig: algebra_sig{i:l}(A),
alg_car: a.car,
pi1: fst(t),
alg_plus: a.plus,
pi2: snd(t),
alg_zero: a.zero,
alg_minus: a.minus,
alg_act: a.act,
ring_p: IsRing(T;plus;zero;neg;times;one),
and: P ∧ Q,
cand: A c∧ B,
action_p: IsAction(A;x;e;S;f),
true: True,
squash: ↓T,
prop: ℙ,
subtype_rel: A ⊆r B,
uimplies: b supposing a,
guard: {T},
iff: P ⇐⇒ Q,
rev_implies: P ⇐ Q,
implies: P ⇒ Q,
bilinear_p: IsBilinear(A;B;C;+a;+b;+c;f),
monoid_p: IsMonoid(T;op;id),
assoc: Assoc(T;op),
ident: Ident(T;op;id),
alg_times: a.times,
alg_one: a.one,
dist_1op_2op_lr: Dist1op2opLR(A;1op;2op),
infix_ap: x f y,
so_lambda: λ2x.t[x],
so_apply: x[s]
Lemmas referenced :
crng_properties,
crng_wf,
rng_properties,
rng_car_wf,
rng_eq_wf,
rng_le_wf,
rng_plus_wf,
rng_zero_wf,
rng_minus_wf,
rng_times_wf,
rng_one_wf,
rng_div_wf,
unit_wf2,
bool_wf,
rng_plus_comm2,
infix_ap_wf,
equal_wf,
squash_wf,
true_wf,
rng_times_assoc,
iff_weakening_equal,
rng_times_one,
rng_times_over_plus,
group_p_wf,
alg_car_wf,
alg_plus_wf,
alg_zero_wf,
alg_minus_wf,
comm_wf,
action_p_wf,
alg_act_wf,
bilinear_p_wf,
crng_times_ac_1,
ring_p_wf,
monoid_p_wf,
alg_times_wf,
alg_one_wf,
bilinear_wf,
all_wf,
dist_1op_2op_lr_wf
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
lambdaFormation,
cut,
introduction,
extract_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
setElimination,
rename,
dependent_set_memberEquality,
dependent_pairEquality,
because_Cache,
functionEquality,
productEquality,
unionEquality,
cumulativity,
sqequalRule,
productElimination,
independent_pairFormation,
isect_memberFormation,
lambdaEquality,
dependent_functionElimination,
axiomEquality,
isect_memberEquality,
natural_numberEquality,
applyEquality,
imageElimination,
equalityTransitivity,
equalitySymmetry,
universeEquality,
imageMemberEquality,
baseClosed,
independent_isectElimination,
independent_functionElimination,
independent_pairEquality
Latex:
\mforall{}R:CRng. (rng\_to\_alg(R) \mmember{} algebra\{i:l\}(R))
Date html generated:
2017_10_01-AM-09_52_01
Last ObjectModification:
2017_03_03-PM-00_46_53
Theory : algebras_1
Home
Index