Theorem rngogrpo 37934

Description: A ring's addition operation is a group operation. (Contributed by Steve Rodriguez, 9-Sep-2007.) (New usage is discouraged.)

Hypothesis

Ref	Expression
ringgrp.1	⊢ 𝐺 = (1st ‘𝑅)

Assertion

Ref	Expression
rngogrpo	⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp)

Proof of Theorem rngogrpo

Step	Hyp	Ref	Expression
1		ringgrp.1	. . 3 ⊢ 𝐺 = (1st ‘𝑅)
2	1	rngoablo 37932	. 2 ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ AbelOp)
3		ablogrpo 30528	. 2 ⊢ (𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp)
4	2, 3	syl 17	1 ⊢ (𝑅 ∈ RingOps → 𝐺 ∈ GrpOp)

Syntax hints:   → wi 4   = wceq 1540   ∈ wcel 2108  ‘cfv 6531  1^st c1st 7986  GrpOpcgr 30470  AbelOpcablo 30525  RingOpscrngo 37918

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 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402  ax-un 7729

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-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-1st 7988  df-2nd 7989  df-ablo 30526  df-rngo 37919

This theorem is referenced by:  rngone0  37935  rngogcl  37936  rngoaass  37938  rngorcan  37941  rngolcan  37942  rngo0cl  37943  rngo0rid  37944  rngo0lid  37945  rngolz  37946  rngorz  37947  rngosn3  37948  rngonegcl  37951  rngoaddneg1  37952  rngoaddneg2  37953  rngosub  37954  rngodm1dm2  37956  rngorn1  37957  rngonegmn1l  37965  rngonegmn1r  37966  rngogrphom  37995  rngohom0  37996  rngohomsub  37997  rngokerinj  37999  keridl  38056  dmncan1  38100