Metamath Proof Explorer

Theorem subrgsubg

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

Ref Expression
Assertion subrgsubg 
|- ( A e. ( SubRing ` R ) -> A e. ( SubGrp ` R ) )

Proof

Step Hyp Ref Expression
1 subrgrcl 
 |-  ( A e. ( SubRing ` R ) -> R e. Ring )
2 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
3 1 2 syl 
 |-  ( A e. ( SubRing ` R ) -> R e. Grp )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 4 subrgss 
 |-  ( A e. ( SubRing ` R ) -> A C_ ( Base ` R ) )
6 eqid 
 |-  ( R |`s A ) = ( R |`s A )
7 6 subrgring 
 |-  ( A e. ( SubRing ` R ) -> ( R |`s A ) e. Ring )
8 ringgrp 
 |-  ( ( R |`s A ) e. Ring -> ( R |`s A ) e. Grp )
9 7 8 syl 
 |-  ( A e. ( SubRing ` 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. ( SubRing ` R ) -> A e. ( SubGrp ` R ) )