Metamath Proof Explorer


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 ) )