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