Metamath Proof Explorer

Theorem rhmpropd

Description: Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses rhmpropd.a 
|- ( ph -> B = ( Base ` J ) )
rhmpropd.b 
|- ( ph -> C = ( Base ` K ) )
rhmpropd.c 
|- ( ph -> B = ( Base ` L ) )
rhmpropd.d 
|- ( ph -> C = ( Base ` M ) )
rhmpropd.e 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
rhmpropd.f 
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
rhmpropd.g 
|- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` J ) y ) = ( x ( .r ` L ) y ) )
rhmpropd.h 
|- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` M ) y ) )
Assertion rhmpropd 
|- ( ph -> ( J RingHom K ) = ( L RingHom M ) )

Proof

Step Hyp Ref Expression
1 rhmpropd.a 
 |-  ( ph -> B = ( Base ` J ) )
2 rhmpropd.b 
 |-  ( ph -> C = ( Base ` K ) )
3 rhmpropd.c 
 |-  ( ph -> B = ( Base ` L ) )
4 rhmpropd.d 
 |-  ( ph -> C = ( Base ` M ) )
5 rhmpropd.e 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )
6 rhmpropd.f 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )
7 rhmpropd.g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` J ) y ) = ( x ( .r ` L ) y ) )
8 rhmpropd.h 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` M ) y ) )
9 1 3 5 7 ringpropd 
 |-  ( ph -> ( J e. Ring <-> L e. Ring ) )
10 2 4 6 8 ringpropd 
 |-  ( ph -> ( K e. Ring <-> M e. Ring ) )
11 9 10 anbi12d 
 |-  ( ph -> ( ( J e. Ring /\ K e. Ring ) <-> ( L e. Ring /\ M e. Ring ) ) )
12 1 2 3 4 5 6 ghmpropd 
 |-  ( ph -> ( J GrpHom K ) = ( L GrpHom M ) )
13 12 eleq2d 
 |-  ( ph -> ( f e. ( J GrpHom K ) <-> f e. ( L GrpHom M ) ) )
14 eqid 
 |-  ( mulGrp ` J ) = ( mulGrp ` J )
15 eqid 
 |-  ( Base ` J ) = ( Base ` J )
16 14 15 mgpbas 
 |-  ( Base ` J ) = ( Base ` ( mulGrp ` J ) )
17 1 16 syl6eq 
 |-  ( ph -> B = ( Base ` ( mulGrp ` J ) ) )
18 eqid 
 |-  ( mulGrp ` K ) = ( mulGrp ` K )
19 eqid 
 |-  ( Base ` K ) = ( Base ` K )
20 18 19 mgpbas 
 |-  ( Base ` K ) = ( Base ` ( mulGrp ` K ) )
21 2 20 syl6eq 
 |-  ( ph -> C = ( Base ` ( mulGrp ` K ) ) )
22 eqid 
 |-  ( mulGrp ` L ) = ( mulGrp ` L )
23 eqid 
 |-  ( Base ` L ) = ( Base ` L )
24 22 23 mgpbas 
 |-  ( Base ` L ) = ( Base ` ( mulGrp ` L ) )
25 3 24 syl6eq 
 |-  ( ph -> B = ( Base ` ( mulGrp ` L ) ) )
26 eqid 
 |-  ( mulGrp ` M ) = ( mulGrp ` M )
27 eqid 
 |-  ( Base ` M ) = ( Base ` M )
28 26 27 mgpbas 
 |-  ( Base ` M ) = ( Base ` ( mulGrp ` M ) )
29 4 28 syl6eq 
 |-  ( ph -> C = ( Base ` ( mulGrp ` M ) ) )
30 eqid 
 |-  ( .r ` J ) = ( .r ` J )
31 14 30 mgpplusg 
 |-  ( .r ` J ) = ( +g ` ( mulGrp ` J ) )
32 31 oveqi 
 |-  ( x ( .r ` J ) y ) = ( x ( +g ` ( mulGrp ` J ) ) y )
33 eqid 
 |-  ( .r ` L ) = ( .r ` L )
34 22 33 mgpplusg 
 |-  ( .r ` L ) = ( +g ` ( mulGrp ` L ) )
35 34 oveqi 
 |-  ( x ( .r ` L ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y )
36 7 32 35 3eqtr3g 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` ( mulGrp ` J ) ) y ) = ( x ( +g ` ( mulGrp ` L ) ) y ) )
37 eqid 
 |-  ( .r ` K ) = ( .r ` K )
38 18 37 mgpplusg 
 |-  ( .r ` K ) = ( +g ` ( mulGrp ` K ) )
39 38 oveqi 
 |-  ( x ( .r ` K ) y ) = ( x ( +g ` ( mulGrp ` K ) ) y )
40 eqid 
 |-  ( .r ` M ) = ( .r ` M )
41 26 40 mgpplusg 
 |-  ( .r ` M ) = ( +g ` ( mulGrp ` M ) )
42 41 oveqi 
 |-  ( x ( .r ` M ) y ) = ( x ( +g ` ( mulGrp ` M ) ) y )
43 8 39 42 3eqtr3g 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` ( mulGrp ` K ) ) y ) = ( x ( +g ` ( mulGrp ` M ) ) y ) )
44 17 21 25 29 36 43 mhmpropd 
 |-  ( ph -> ( ( mulGrp ` J ) MndHom ( mulGrp ` K ) ) = ( ( mulGrp ` L ) MndHom ( mulGrp ` M ) ) )
45 44 eleq2d 
 |-  ( ph -> ( f e. ( ( mulGrp ` J ) MndHom ( mulGrp ` K ) ) <-> f e. ( ( mulGrp ` L ) MndHom ( mulGrp ` M ) ) ) )
46 13 45 anbi12d 
 |-  ( ph -> ( ( f e. ( J GrpHom K ) /\ f e. ( ( mulGrp ` J ) MndHom ( mulGrp ` K ) ) ) <-> ( f e. ( L GrpHom M ) /\ f e. ( ( mulGrp ` L ) MndHom ( mulGrp ` M ) ) ) ) )
47 11 46 anbi12d 
 |-  ( ph -> ( ( ( J e. Ring /\ K e. Ring ) /\ ( f e. ( J GrpHom K ) /\ f e. ( ( mulGrp ` J ) MndHom ( mulGrp ` K ) ) ) ) <-> ( ( L e. Ring /\ M e. Ring ) /\ ( f e. ( L GrpHom M ) /\ f e. ( ( mulGrp ` L ) MndHom ( mulGrp ` M ) ) ) ) ) )
48 14 18 isrhm 
 |-  ( f e. ( J RingHom K ) <-> ( ( J e. Ring /\ K e. Ring ) /\ ( f e. ( J GrpHom K ) /\ f e. ( ( mulGrp ` J ) MndHom ( mulGrp ` K ) ) ) ) )
49 22 26 isrhm 
 |-  ( f e. ( L RingHom M ) <-> ( ( L e. Ring /\ M e. Ring ) /\ ( f e. ( L GrpHom M ) /\ f e. ( ( mulGrp ` L ) MndHom ( mulGrp ` M ) ) ) ) )
50 47 48 49 3bitr4g 
 |-  ( ph -> ( f e. ( J RingHom K ) <-> f e. ( L RingHom M ) ) )
51 50 eqrdv 
 |-  ( ph -> ( J RingHom K ) = ( L RingHom M ) )