Nuprl Lemma : drng_all_properties
∀[r:DRng]
(Assoc(|r|;+r)
∧ Ident(|r|;+r;0)
∧ Inverse(|r|;+r;0;-r)
∧ Assoc(|r|;*)
∧ Ident(|r|;*;1)
∧ BiLinear(|r|;+r;*)
∧ IsEqFun(|r|;=b))
Proof
Definitions occuring in Statement :
drng: DRng,
rng_one: 1,
rng_times: *,
rng_minus: -r,
rng_zero: 0,
rng_plus: +r,
rng_eq: =b,
rng_car: |r|,
bilinear: BiLinear(T;pl;tm),
ident: Ident(T;op;id),
eqfun_p: IsEqFun(T;eq),
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,
drng: DRng,
and: P ∧ Q,
assoc: Assoc(T;op),
ident: Ident(T;op;id),
inverse: Inverse(T;op;id;inv),
bilinear: BiLinear(T;pl;tm),
eqfun_p: IsEqFun(T;eq),
uiff: uiff(P;Q),
uimplies: b supposing a,
prop: ℙ,
infix_ap: x f y,
implies: P ⇒ Q,
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 :
drng_properties,
rng_car_wf,
assert_wf,
rng_eq_wf,
assert_witness,
equal_wf,
drng_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,
applyEquality,
equalityTransitivity,
equalitySymmetry,
independent_functionElimination,
independent_pairFormation
Latex:
\mforall{}[r:DRng]
(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;*)
\mwedge{} IsEqFun(|r|;=\msubb{}))
Date html generated:
2016_05_15-PM-00_20_36
Last ObjectModification:
2015_12_27-AM-00_02_50
Theory : rings_1
Home
Index