Theorem zrh1

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

	Ref	Expression
Hypotheses	zrh1.l	|- L = ( ZRHom ` R )
	zrh1.o	|- .1. = ( 1r ` R )
Assertion	zrh1	|- ( R e. Ring -> ( L ` 1 ) = .1. )

Proof

Step	Hyp	Ref	Expression
1		zrh1.l	|- L = ( ZRHom ` R )
2		zrh1.o	|- .1. = ( 1r ` R )
3	1	zrhrhm	|- ( R e. Ring -> L e. ( ZZring RingHom R ) )
4		zring1	|- 1 = ( 1r ` ZZring )
5	4 2	rhm1	|- ( L e. ( ZZring RingHom R ) -> ( L ` 1 ) = .1. )
6	3 5	syl	|- ( R e. Ring -> ( L ` 1 ) = .1. )