Metamath Proof Explorer


Theorem subrgsubg

Description: A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014)

Ref Expression
Assertion subrgsubg A SubRing R A SubGrp R

Proof

Step Hyp Ref Expression
1 subrgrcl A SubRing R R Ring
2 ringgrp R Ring R Grp
3 1 2 syl A SubRing R R Grp
4 eqid Base R = Base R
5 4 subrgss A SubRing R A Base R
6 eqid R 𝑠 A = R 𝑠 A
7 6 subrgring A SubRing R R 𝑠 A Ring
8 ringgrp R 𝑠 A Ring R 𝑠 A Grp
9 7 8 syl A SubRing R R 𝑠 A Grp
10 4 issubg A SubGrp R R Grp A Base R R 𝑠 A Grp
11 3 5 9 10 syl3anbrc A SubRing R A SubGrp R