### Nuprl Lemma : rng_times_over_plus

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

Proof

Definitions occuring in Statement :  rng: Rng rng_times: * rng_plus: +r rng_car: |r| uall: [x:A]. B[x] infix_ap: y and: P ∧ Q equal: t ∈ T
Definitions unfolded in proof :  bilinear: BiLinear(T;pl;tm) uall: [x:A]. B[x] member: t ∈ T and: P ∧ Q rng: Rng
Lemmas referenced :  rng_car_wf rng_wf rng_all_properties
Rules used in proof :  sqequalSubstitution sqequalRule sqequalReflexivity sqequalTransitivity computationStep isect_memberFormation introduction cut sqequalHypSubstitution isect_memberEquality isectElimination thin hypothesisEquality productElimination independent_pairEquality axiomEquality hypothesis lemma_by_obid setElimination rename

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

Date html generated: 2016_05_15-PM-00_21_37
Last ObjectModification: 2015_12_27-AM-00_01_51

Theory : rings_1

Home Index