[r:Rng]. ∀[e:|r|]. ∀[a,b:ℕ].  (((a b) ⋅e) ((a ⋅e) +r (b ⋅e)) ∈ |r|)

Proof

Definitions occuring in Statement :  rng_nat_op: n ⋅e rng: Rng rng_plus: +r rng_car: |r| nat: uall: [x:A]. B[x] infix_ap: y add: m equal: t ∈ T
Definitions unfolded in proof :  uall: [x:A]. B[x] member: t ∈ T subtype_rel: A ⊆B grp: Group{i} mon: Mon imon: IMonoid prop: rng_nat_op: n ⋅e add_grp_of_rng: r↓+gp grp_car: |g| pi1: fst(t) grp_op: * pi2: snd(t) rng: Rng
Lemmas referenced :  mon_nat_op_add add_grp_of_rng_wf_a grp_sig_wf monoid_p_wf grp_car_wf grp_op_wf grp_id_wf inverse_wf grp_inv_wf nat_wf 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 lambdaEquality setElimination rename setEquality cumulativity isect_memberEquality axiomEquality

Latex:
\mforall{}[r:Rng].  \mforall{}[e:|r|].  \mforall{}[a,b:\mBbbN{}].    (((a  +  b)  \mcdot{}r  e)  =  ((a  \mcdot{}r  e)  +r  (b  \mcdot{}r  e)))

Date html generated: 2016_05_15-PM-00_27_25
Last ObjectModification: 2015_12_26-PM-11_58_54

Theory : rings_1

Home Index