Metamath Proof Explorer

Theorem subrngsubg

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

Ref Expression
Assertion subrngsubg 
|- ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )

Proof

Step Hyp Ref Expression
1 subrngrcl 
 |-  ( A e. ( SubRng ` R ) -> R e. Rng )
2 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
3 1 2 syl 
 |-  ( A e. ( SubRng ` R ) -> R e. Grp )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 subrngss 
 |-  ( A e. ( SubRng ` R ) -> A C_ ( Base ` R ) )
6 eqid 
 |-  ( R |`s A ) = ( R |`s A )
7 6 subrngrng 
 |-  ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Rng )
8 rnggrp 
 |-  ( ( R |`s A ) e. Rng -> ( R |`s A ) e. Grp )
9 7 8 syl 
 |-  ( A e. ( SubRng ` R ) -> ( R |`s A ) e. Grp )
10 4 issubg 
 |-  ( A e. ( SubGrp ` R ) <-> ( R e. Grp /\ A C_ ( Base ` R ) /\ ( R |`s A ) e. Grp ) )
11 3 5 9 10 syl3anbrc 
 |-  ( A e. ( SubRng ` R ) -> A e. ( SubGrp ` R ) )