Theorem zrh0

Description: Interpretation of 0 in a ring. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	zrh0.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrh0.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	zrh0	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 0 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		zrh0.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		zrh0.z	⊢ 0 = ( 0g ‘ 𝑅 )
3	1	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
4		rhmghm	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
5		zring0	⊢ 0 = ( 0g ‘ ℤring )
6	5 2	ghmid	⊢ ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) → ( 𝐿 ‘ 0 ) = 0 )
7	3 4 6	3syl	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 0 ) = 0 )