Theorem rngabl 20279

Description: A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020.)

Assertion

Ref	Expression
rngabl	⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)

Proof of Theorem rngabl

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eqid 2765	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2765	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2765	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2765	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isrng 20278	. 2 ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ (mulGrp‘𝑅) ∈ Smgrp ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1163	1 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   = wceq 1570   ∈ wcel 2146  ∀wral 3081  ‘cfv 6540  (class class class)co 7419  Basecbs 17293  +_gcplusg 17334  ._rcmulr 17335  Smgrpcsgrp 18810  Abelcabl 19897  mulGrpcmgp 20262  Rngcrng 20276

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737  ax-nul 5271

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-ne 2961  df-ral 3082  df-rab 3419  df-v 3459  df-sbc 3747  df-dif 3909  df-un 3911  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4875  df-br 5112  df-iota 6496  df-fv 6548  df-ov 7422  df-rng 20277

This theorem is used by:  rnggrp  20282  rnglz  20289  rngansg  20294  prdsrngd  20300  imasrng  20301  isringrng  20417  opprrng  20475  isrnghm  20571  isrnghmd  20581  idrnghm  20588  c0rnghm  20686  zrrnghm  20687  subrngringnsg  20704  issubrng2  20709  rnglidlrng  21433  2idlcpblrng  21462  qus2idrng  21464  rngqiprngimf1lem  21486  rngqiprngimfo  21493  rngqiprngfulem2  21504  rngqiprngfulem4  21506