Theorem zrh0

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

	Ref	Expression
Hypotheses	zrh0.l	|- L = ( ZRHom ` R )
	zrh0.z	|- .0. = ( 0g ` R )
Assertion	zrh0	|- ( R e. Ring -> ( L ` 0 ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		zrh0.l	|- L = ( ZRHom ` R )
2		zrh0.z	|- .0. = ( 0g ` R )
3	1	zrhrhm	|- ( R e. Ring -> L e. ( ZZring RingHom R ) )
4		rhmghm	|- ( L e. ( ZZring RingHom R ) -> L e. ( ZZring GrpHom R ) )
5		zring0	|- 0 = ( 0g ` ZZring )
6	5 2	ghmid	|- ( L e. ( ZZring GrpHom R ) -> ( L ` 0 ) = .0. )
7	3 4 6	3syl	|- ( R e. Ring -> ( L ` 0 ) = .0. )