Theorem zrhpropd

Description: The ZZ ring homomorphism depends only on the ring attributes of a structure. (Contributed by Mario Carneiro, 15-Jun-2015)

	Ref	Expression
Hypotheses	zrhpropd.1	|- ( ph -> B = ( Base ` K ) )
	zrhpropd.2	|- ( ph -> B = ( Base ` L ) )
	zrhpropd.3	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
	zrhpropd.4	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
Assertion	zrhpropd	|- ( ph -> ( ZRHom ` K ) = ( ZRHom ` L ) )

Proof

Step	Hyp	Ref	Expression
1		zrhpropd.1	|- ( ph -> B = ( Base ` K ) )
2		zrhpropd.2	|- ( ph -> B = ( Base ` L ) )
3		zrhpropd.3	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )
4		zrhpropd.4	|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )
5		eqidd	|- ( ph -> ( Base ` ZZring ) = ( Base ` ZZring ) )
6		eqidd	|- ( ( ph /\ ( x e. ( Base ` ZZring ) /\ y e. ( Base ` ZZring ) ) ) -> ( x ( +g ` ZZring ) y ) = ( x ( +g ` ZZring ) y ) )
7		eqidd	|- ( ( ph /\ ( x e. ( Base ` ZZring ) /\ y e. ( Base ` ZZring ) ) ) -> ( x ( .r ` ZZring ) y ) = ( x ( .r ` ZZring ) y ) )
8	5 1 5 2 6 3 7 4	rhmpropd	|- ( ph -> ( ZZring RingHom K ) = ( ZZring RingHom L ) )
9	8	unieqd	|- ( ph -> U. ( ZZring RingHom K ) = U. ( ZZring RingHom L ) )
10		eqid	|- ( ZRHom ` K ) = ( ZRHom ` K )
11	10	zrhval	|- ( ZRHom ` K ) = U. ( ZZring RingHom K )
12		eqid	|- ( ZRHom ` L ) = ( ZRHom ` L )
13	12	zrhval	|- ( ZRHom ` L ) = U. ( ZZring RingHom L )
14	9 11 13	3eqtr4g	|- ( ph -> ( ZRHom ` K ) = ( ZRHom ` L ) )