### Nuprl Lemma : drng_properties

`∀[r:DRng]. (IsRing(|r|;+r;0;-r;*;1) ∧ IsEqFun(|r|;=b))`

Proof

Definitions occuring in Statement :  drng: `DRng` ring_p: `IsRing(T;plus;zero;neg;times;one)` rng_one: `1` rng_times: `*` rng_minus: `-r` rng_zero: `0` rng_plus: `+r` rng_eq: `=b` rng_car: `|r|` eqfun_p: `IsEqFun(T;eq)` uall: `∀[x:A]. B[x]` and: `P ∧ Q`
Definitions unfolded in proof :  uall: `∀[x:A]. B[x]` member: `t ∈ T` and: `P ∧ Q` cand: `A c∧ B` drng: `DRng` ring_p: `IsRing(T;plus;zero;neg;times;one)` prop: `ℙ` implies: `P `` Q` sq_stable: `SqStable(P)` monoid_p: `IsMonoid(T;op;id)` assoc: `Assoc(T;op)` ident: `Ident(T;op;id)` bilinear: `BiLinear(T;pl;tm)` squash: `↓T` group_p: `IsGroup(T;op;id;inv)` inverse: `Inverse(T;op;id;inv)` eqfun_p: `IsEqFun(T;eq)` uiff: `uiff(P;Q)` uimplies: `b supposing a` infix_ap: `x f y`
Lemmas referenced :  drng_wf equal_wf assert_witness assert_wf rng_eq_wf sq_stable__eqfun_p squash_wf sq_stable__bilinear sq_stable__monoid_p sq_stable__group_p bilinear_wf rng_one_wf rng_times_wf monoid_p_wf and_wf rng_minus_wf rng_zero_wf rng_plus_wf rng_car_wf group_p_wf sq_stable__and
Rules used in proof :  sqequalSubstitution sqequalTransitivity computationStep sqequalReflexivity isect_memberFormation introduction cut sqequalHypSubstitution setElimination thin rename lemma_by_obid isectElimination hypothesisEquality hypothesis isect_memberEquality independent_functionElimination lambdaFormation because_Cache sqequalRule lambdaEquality dependent_functionElimination productElimination independent_pairEquality axiomEquality imageMemberEquality baseClosed imageElimination independent_pairFormation applyEquality equalityTransitivity equalitySymmetry

Latex:
\mforall{}[r:DRng].  (IsRing(|r|;+r;0;-r;*;1)  \mwedge{}  IsEqFun(|r|;=\msubb{}))

Date html generated: 2016_05_15-PM-00_20_33
Last ObjectModification: 2016_01_15-AM-08_51_43

Theory : rings_1

Home Index