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: 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