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