MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rnggrp Structured version   Visualization version   GIF version

Theorem rnggrp 20098
Description: A non-unital ring is a (additive) group. (Contributed by AV, 16-Feb-2025.)
Assertion
Ref Expression
rnggrp (𝑅 ∈ Rng → 𝑅 ∈ Grp)

Proof of Theorem rnggrp
StepHypRef Expression
1 rngabl 20095 . 2 (𝑅 ∈ Rng → 𝑅 ∈ Abel)
21ablgrpd 19741 1 (𝑅 ∈ Rng → 𝑅 ∈ Grp)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2099  Grpcgrp 18890  Rngcrng 20092
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-abl 19738  df-rng 20093
This theorem is referenced by:  rngacl  20102  rng0cl  20103  rngrz  20106  rngmneg1  20107  rngmneg2  20108  rngm2neg  20109  rngsubdi  20111  rngsubdir  20112  prdsrngd  20116  subrngsubg  20489  cntzsubrng  20504  rnglidlmcl  21112  rnglidl0  21125  rnglidl1  21128  2idlcpblrng  21165  rngqiprngimfolem  21180  rngqiprngimf1lem  21184  rngqiprngghm  21189  rngqiprngimf1  21190  rngqiprngimfo  21191  rngqiprngfulem3  21203  rngqiprngfulem4  21204  rngqiprngfulem5  21205  pzriprnglem4  21410  pzriprnglem10  21416
  Copyright terms: Public domain W3C validator