Theorem zrh1

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

	Ref	Expression
Hypotheses	zrh1.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrh1.o	⊢ 1 = ( 1r ‘ 𝑅 )
Assertion	zrh1	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 1 ) = 1 )

Proof

Step	Hyp	Ref	Expression
1		zrh1.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
2		zrh1.o	⊢ 1 = ( 1r ‘ 𝑅 )
3	1	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
4		zring1	⊢ 1 = ( 1r ‘ ℤring )
5	4 2	rhm1	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → ( 𝐿 ‘ 1 ) = 1 )
6	3 5	syl	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 1 ) = 1 )