Nuprl Lemma : rng_all_properties
∀[r:Rng]. (Assoc(|r|;+r) ∧ Ident(|r|;+r;0) ∧ Inverse(|r|;+r;0;-r) ∧ Assoc(|r|;*) ∧ Ident(|r|;*;1) ∧ BiLinear(|r|;+r;*))
Proof
Definitions occuring in Statement :
rng: Rng,
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),
assoc: Assoc(T;op),
uall: ∀[x:A]. B[x],
and: P ∧ Q
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
rng: Rng,
and: P ∧ Q,
assoc: Assoc(T;op),
ident: Ident(T;op;id),
inverse: Inverse(T;op;id;inv),
bilinear: BiLinear(T;pl;tm),
ring_p: IsRing(T;plus;zero;neg;times;one),
monoid_p: IsMonoid(T;op;id),
group_p: IsGroup(T;op;id;inv),
cand: A c∧ B
Lemmas referenced :
rng_properties,
rng_car_wf,
rng_wf
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:Rng]
(Assoc(|r|;+r)
\mwedge{} Ident(|r|;+r;0)
\mwedge{} Inverse(|r|;+r;0;-r)
\mwedge{} Assoc(|r|;*)
\mwedge{} Ident(|r|;*;1)
\mwedge{} BiLinear(|r|;+r;*))
Date html generated:
2016_05_15-PM-00_20_35
Last ObjectModification:
2015_12_27-AM-00_02_49
Theory : rings_1
Home
Index