Theorem subrng0

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

	Ref	Expression
Hypotheses	subrng0.1	⊢ 𝑆 = ( 𝑅 ↾s 𝐴 )
	subrng0.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	subrng0	⊢ ( 𝐴 ∈ ( SubRng ‘ 𝑅 ) → 0 = ( 0g ‘ 𝑆 ) )

Proof

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