Theorem rngabl 20201

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

Syntax hints:   → wi 4   ∧ wa 399   = wceq 1560   ∈ wcel 2142  ∀wral 3076  ‘cfv 6521  (class class class)co 7396  Basecbs 17245  +_gcplusg 17286  ._rcmulr 17287  Smgrpcsgrp 18752  Abelcabl 19821  mulGrpcmgp 20186  Rngcrng 20198

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734  ax-nul 5256

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1100  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-ne 2958  df-ral 3077  df-rab 3415  df-v 3456  df-sbc 3745  df-dif 3907  df-un 3909  df-ss 3921  df-nul 4286  df-if 4481  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-br 5101  df-iota 6477  df-fv 6529  df-ov 7399  df-rng 20199

This theorem is referenced by:  rnggrp  20204  rnglz  20211  rngansg  20216  prdsrngd  20222  imasrng  20223  isringrng  20337  opprrng  20394  isrnghm  20490  isrnghmd  20500  idrnghm  20507  c0rnghm  20585  zrrnghm  20586  subrngringnsg  20603  issubrng2  20608  rnglidlrng  21317  2idlcpblrng  21341  qus2idrng  21343  rngqiprngimf1lem  21364  rngqiprngimfo  21371  rngqiprngfulem2  21382  rngqiprngfulem4  21384