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 𝐴 )
	subrg0.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	subrg0	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		subrg0.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
2		subrg0.2	⊢ 0 = ( 0g ‘ 𝑅 )
3		subrgsubg	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 𝐴 ∈ ( SubGrp ‘ 𝑅 ) )
4	1 2	subg0	⊢ ( 𝐴 ∈ ( SubGrp ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )
5	3 4	syl	⊢ ( 𝐴 ∈ ( SubRing ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )