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 ) )