Nuprl Lemma : crng_all_properties
∀[r:CRng]
(Assoc(|r|;+r)
∧ Ident(|r|;+r;0)
∧ Inverse(|r|;+r;0;-r)
∧ Assoc(|r|;*)
∧ Comm(|r|;*)
∧ Ident(|r|;*;1)
∧ BiLinear(|r|;+r;*))
Proof
Definitions occuring in Statement :
crng: CRng,
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
rng_car: |r|,
bilinear: BiLinear(T;pl;tm),
ident: Ident(T;op;id),
inverse: Inverse(T;op;id;inv),
comm: Comm(T;op),
assoc: Assoc(T;op),
uall: ∀[x:A]. B[x],
and: P ∧ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
crng: CRng,
and: P ∧ Q,
assoc: Assoc(T;op),
rng: Rng,
ident: Ident(T;op;id),
inverse: Inverse(T;op;id;inv),
comm: Comm(T;op),
bilinear: BiLinear(T;pl;tm),
cand: A c∧ B
Lemmas referenced :
crng_properties,
rng_car_wf,
crng_wf,
rng_all_properties
Rules used in proof :
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
introduction,
cut,
lemma_by_obid,
sqequalHypSubstitution,
isectElimination,
thin,
hypothesisEquality,
hypothesis,
setElimination,
rename,
sqequalRule,
productElimination,
independent_pairEquality,
isect_memberEquality,
axiomEquality,
independent_pairFormation
Latex:
\mforall{}[r:CRng]
(Assoc(|r|;+r)
\mwedge{} Ident(|r|;+r;0)
\mwedge{} Inverse(|r|;+r;0;-r)
\mwedge{} Assoc(|r|;*)
\mwedge{} Comm(|r|;*)
\mwedge{} Ident(|r|;*;1)
\mwedge{} BiLinear(|r|;+r;*))
Date html generated:
2016_05_15-PM-00_20_58
Last ObjectModification:
2015_12_27-AM-00_02_34
Theory : rings_1
Home
Index