Metamath Proof Explorer


Theorem pwsco2rhm

Description: Left composition with a ring homomorphism yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco2rhm.y
|- Y = ( R ^s A )
pwsco2rhm.z
|- Z = ( S ^s A )
pwsco2rhm.b
|- B = ( Base ` Y )
pwsco2rhm.a
|- ( ph -> A e. V )
pwsco2rhm.f
|- ( ph -> F e. ( R RingHom S ) )
Assertion pwsco2rhm
|- ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y RingHom Z ) )

Proof

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