Step |
Hyp |
Ref |
Expression |
1 |
|
pwsco1rhm.y |
|- Y = ( R ^s A ) |
2 |
|
pwsco1rhm.z |
|- Z = ( R ^s B ) |
3 |
|
pwsco1rhm.c |
|- C = ( Base ` Z ) |
4 |
|
pwsco1rhm.r |
|- ( ph -> R e. Ring ) |
5 |
|
pwsco1rhm.a |
|- ( ph -> A e. V ) |
6 |
|
pwsco1rhm.b |
|- ( ph -> B e. W ) |
7 |
|
pwsco1rhm.f |
|- ( ph -> F : A --> B ) |
8 |
2
|
pwsring |
|- ( ( R e. Ring /\ B e. W ) -> Z e. Ring ) |
9 |
4 6 8
|
syl2anc |
|- ( ph -> Z e. Ring ) |
10 |
1
|
pwsring |
|- ( ( R e. Ring /\ A e. V ) -> Y e. Ring ) |
11 |
4 5 10
|
syl2anc |
|- ( ph -> Y e. Ring ) |
12 |
|
ringmnd |
|- ( R e. Ring -> R e. Mnd ) |
13 |
4 12
|
syl |
|- ( ph -> R e. Mnd ) |
14 |
1 2 3 13 5 6 7
|
pwsco1mhm |
|- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z MndHom Y ) ) |
15 |
|
ringgrp |
|- ( Z e. Ring -> Z e. Grp ) |
16 |
9 15
|
syl |
|- ( ph -> Z e. Grp ) |
17 |
|
ringgrp |
|- ( Y e. Ring -> Y e. Grp ) |
18 |
11 17
|
syl |
|- ( ph -> Y e. Grp ) |
19 |
|
ghmmhmb |
|- ( ( Z e. Grp /\ Y e. Grp ) -> ( Z GrpHom Y ) = ( Z MndHom Y ) ) |
20 |
16 18 19
|
syl2anc |
|- ( ph -> ( Z GrpHom Y ) = ( Z MndHom Y ) ) |
21 |
14 20
|
eleqtrrd |
|- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z GrpHom Y ) ) |
22 |
|
eqid |
|- ( ( mulGrp ` R ) ^s A ) = ( ( mulGrp ` R ) ^s A ) |
23 |
|
eqid |
|- ( ( mulGrp ` R ) ^s B ) = ( ( mulGrp ` R ) ^s B ) |
24 |
|
eqid |
|- ( Base ` ( ( mulGrp ` R ) ^s B ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) |
25 |
|
eqid |
|- ( mulGrp ` R ) = ( mulGrp ` R ) |
26 |
25
|
ringmgp |
|- ( R e. Ring -> ( mulGrp ` R ) e. Mnd ) |
27 |
4 26
|
syl |
|- ( ph -> ( mulGrp ` R ) e. Mnd ) |
28 |
22 23 24 27 5 6 7
|
pwsco1mhm |
|- ( ph -> ( g e. ( Base ` ( ( mulGrp ` R ) ^s B ) ) |-> ( g o. F ) ) e. ( ( ( mulGrp ` R ) ^s B ) MndHom ( ( mulGrp ` R ) ^s A ) ) ) |
29 |
|
eqid |
|- ( Base ` R ) = ( Base ` R ) |
30 |
2 29
|
pwsbas |
|- ( ( R e. Mnd /\ B e. W ) -> ( ( Base ` R ) ^m B ) = ( Base ` Z ) ) |
31 |
13 6 30
|
syl2anc |
|- ( ph -> ( ( Base ` R ) ^m B ) = ( Base ` Z ) ) |
32 |
31 3
|
eqtr4di |
|- ( ph -> ( ( Base ` R ) ^m B ) = C ) |
33 |
25 29
|
mgpbas |
|- ( Base ` R ) = ( Base ` ( mulGrp ` R ) ) |
34 |
23 33
|
pwsbas |
|- ( ( ( mulGrp ` R ) e. Mnd /\ B e. W ) -> ( ( Base ` R ) ^m B ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) ) |
35 |
27 6 34
|
syl2anc |
|- ( ph -> ( ( Base ` R ) ^m B ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) ) |
36 |
32 35
|
eqtr3d |
|- ( ph -> C = ( Base ` ( ( mulGrp ` R ) ^s B ) ) ) |
37 |
36
|
mpteq1d |
|- ( ph -> ( g e. C |-> ( g o. F ) ) = ( g e. ( Base ` ( ( mulGrp ` R ) ^s B ) ) |-> ( g o. F ) ) ) |
38 |
|
eqidd |
|- ( ph -> ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( mulGrp ` Z ) ) ) |
39 |
|
eqidd |
|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) ) |
40 |
|
eqid |
|- ( mulGrp ` Z ) = ( mulGrp ` Z ) |
41 |
|
eqid |
|- ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( mulGrp ` Z ) ) |
42 |
|
eqid |
|- ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( mulGrp ` Z ) ) |
43 |
|
eqid |
|- ( +g ` ( ( mulGrp ` R ) ^s B ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) |
44 |
2 25 23 40 41 24 42 43
|
pwsmgp |
|- ( ( R e. Ring /\ B e. W ) -> ( ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) /\ ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) ) ) |
45 |
4 6 44
|
syl2anc |
|- ( ph -> ( ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) /\ ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) ) ) |
46 |
45
|
simpld |
|- ( ph -> ( Base ` ( mulGrp ` Z ) ) = ( Base ` ( ( mulGrp ` R ) ^s B ) ) ) |
47 |
|
eqid |
|- ( mulGrp ` Y ) = ( mulGrp ` Y ) |
48 |
|
eqid |
|- ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( mulGrp ` Y ) ) |
49 |
|
eqid |
|- ( Base ` ( ( mulGrp ` R ) ^s A ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) |
50 |
|
eqid |
|- ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( mulGrp ` Y ) ) |
51 |
|
eqid |
|- ( +g ` ( ( mulGrp ` R ) ^s A ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) |
52 |
1 25 22 47 48 49 50 51
|
pwsmgp |
|- ( ( R e. Ring /\ A e. V ) -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) ) ) |
53 |
4 5 52
|
syl2anc |
|- ( ph -> ( ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) /\ ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) ) ) |
54 |
53
|
simpld |
|- ( ph -> ( Base ` ( mulGrp ` Y ) ) = ( Base ` ( ( mulGrp ` R ) ^s A ) ) ) |
55 |
45
|
simprd |
|- ( ph -> ( +g ` ( mulGrp ` Z ) ) = ( +g ` ( ( mulGrp ` R ) ^s B ) ) ) |
56 |
55
|
oveqdr |
|- ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Z ) ) /\ y e. ( Base ` ( mulGrp ` Z ) ) ) ) -> ( x ( +g ` ( mulGrp ` Z ) ) y ) = ( x ( +g ` ( ( mulGrp ` R ) ^s B ) ) y ) ) |
57 |
53
|
simprd |
|- ( ph -> ( +g ` ( mulGrp ` Y ) ) = ( +g ` ( ( mulGrp ` R ) ^s A ) ) ) |
58 |
57
|
oveqdr |
|- ( ( ph /\ ( x e. ( Base ` ( mulGrp ` Y ) ) /\ y e. ( Base ` ( mulGrp ` Y ) ) ) ) -> ( x ( +g ` ( mulGrp ` Y ) ) y ) = ( x ( +g ` ( ( mulGrp ` R ) ^s A ) ) y ) ) |
59 |
38 39 46 54 56 58
|
mhmpropd |
|- ( ph -> ( ( mulGrp ` Z ) MndHom ( mulGrp ` Y ) ) = ( ( ( mulGrp ` R ) ^s B ) MndHom ( ( mulGrp ` R ) ^s A ) ) ) |
60 |
28 37 59
|
3eltr4d |
|- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` Y ) ) ) |
61 |
21 60
|
jca |
|- ( ph -> ( ( g e. C |-> ( g o. F ) ) e. ( Z GrpHom Y ) /\ ( g e. C |-> ( g o. F ) ) e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` Y ) ) ) ) |
62 |
40 47
|
isrhm |
|- ( ( g e. C |-> ( g o. F ) ) e. ( Z RingHom Y ) <-> ( ( Z e. Ring /\ Y e. Ring ) /\ ( ( g e. C |-> ( g o. F ) ) e. ( Z GrpHom Y ) /\ ( g e. C |-> ( g o. F ) ) e. ( ( mulGrp ` Z ) MndHom ( mulGrp ` Y ) ) ) ) ) |
63 |
9 11 61 62
|
syl21anbrc |
|- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z RingHom Y ) ) |