### Nuprl Lemma : rng_plus_inv_assoc

[r:Rng]. ∀[a,b:|r|].  (((a +r ((-r a) +r b)) b ∈ |r|) ∧ (((-r a) +r (a +r b)) b ∈ |r|))

Proof

Definitions occuring in Statement :  rng: Rng rng_minus: -r rng_plus: +r rng_car: |r| uall: [x:A]. B[x] infix_ap: y and: P ∧ Q apply: a equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) grp_inv: ~ and: P ∧ Q rng: Rng
Lemmas referenced :  grp_inv_assoc add_grp_of_rng_wf_a grp_subtype_igrp 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 applyEquality sqequalRule isect_memberEquality productElimination independent_pairEquality axiomEquality setElimination rename

Latex:
\mforall{}[r:Rng].  \mforall{}[a,b:|r|].    (((a  +r  ((-r  a)  +r  b))  =  b)  \mwedge{}  (((-r  a)  +r  (a  +r  b))  =  b))

Date html generated: 2016_05_15-PM-00_21_21
Last ObjectModification: 2015_12_27-AM-00_02_17

Theory : rings_1

Home Index