Metamath Proof Explorer


Theorem subrg0

Description: A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014)

Ref Expression
Hypotheses subrg0.1
|- S = ( R |`s A )
subrg0.2
|- .0. = ( 0g ` R )
Assertion subrg0
|- ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) )

Proof

Step Hyp Ref Expression
1 subrg0.1
 |-  S = ( R |`s A )
2 subrg0.2
 |-  .0. = ( 0g ` R )
3 subrgsubg
 |-  ( A e. ( SubRing ` R ) -> A e. ( SubGrp ` R ) )
4 1 2 subg0
 |-  ( A e. ( SubGrp ` R ) -> .0. = ( 0g ` S ) )
5 3 4 syl
 |-  ( A e. ( SubRing ` R ) -> .0. = ( 0g ` S ) )