Theorem rngabl 20040

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 2729	. . 3 ⊢ (Base‘𝑅) = (Base‘𝑅)
2		eqid 2729	. . 3 ⊢ (mulGrp‘𝑅) = (mulGrp‘𝑅)
3		eqid 2729	. . 3 ⊢ (+g‘𝑅) = (+g‘𝑅)
4		eqid 2729	. . 3 ⊢ (.r‘𝑅) = (.r‘𝑅)
5	1, 2, 3, 4	isrng 20039	. 2 ⊢ (𝑅 ∈ Rng ↔ (𝑅 ∈ Abel ∧ (mulGrp‘𝑅) ∈ Smgrp ∧ ∀𝑥 ∈ (Base‘𝑅)∀𝑦 ∈ (Base‘𝑅)∀𝑧 ∈ (Base‘𝑅)((𝑥(.r‘𝑅)(𝑦(+g‘𝑅)𝑧)) = ((𝑥(.r‘𝑅)𝑦)(+g‘𝑅)(𝑥(.r‘𝑅)𝑧)) ∧ ((𝑥(+g‘𝑅)𝑦)(.r‘𝑅)𝑧) = ((𝑥(.r‘𝑅)𝑧)(+g‘𝑅)(𝑦(.r‘𝑅)𝑧)))))
6	5	simp1bi 1145	1 ⊢ (𝑅 ∈ Rng → 𝑅 ∈ Abel)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2109  ∀wral 3044  ‘cfv 6499  (class class class)co 7369  Basecbs 17155  +_gcplusg 17196  ._rcmulr 17197  Smgrpcsgrp 18621  Abelcabl 19687  mulGrpcmgp 20025  Rngcrng 20037

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-nul 5256

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-ne 2926  df-ral 3045  df-rab 3403  df-v 3446  df-sbc 3751  df-dif 3914  df-un 3916  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-uni 4868  df-br 5103  df-iota 6452  df-fv 6507  df-ov 7372  df-rng 20038

This theorem is referenced by:  rnggrp  20043  rnglz  20050  rngansg  20055  prdsrngd  20061  imasrng  20062  isringrng  20172  opprrng  20230  isrnghm  20326  isrnghmd  20336  idrnghm  20343  c0rnghm  20420  zrrnghm  20421  subrngringnsg  20438  issubrng2  20443  rnglidlrng  21133  2idlcpblrng  21157  qus2idrng  21159  rngqiprngimf1lem  21180  rngqiprngimfo  21187  rngqiprngfulem2  21198  rngqiprngfulem4  21200