Theorem subrng0

Description: A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025)

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

Proof

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