Metamath Proof Explorer


Theorem subrngsubg

Description: A subring is a subgroup. (Contributed by AV, 14-Feb-2025)

Ref Expression
Assertion subrngsubg A SubRng R A SubGrp R

Proof

Step Hyp Ref Expression
1 subrngrcl A SubRng R R Rng
2 rnggrp R Rng R Grp
3 1 2 syl A SubRng R R Grp
4 eqid Base R = Base R
5 4 subrngss A SubRng R A Base R
6 eqid R 𝑠 A = R 𝑠 A
7 6 subrngrng A SubRng R R 𝑠 A Rng
8 rnggrp R 𝑠 A Rng R 𝑠 A Grp
9 7 8 syl A SubRng 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 SubRng R A SubGrp R