This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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