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