This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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