Metamath Proof Explorer

Theorem pwsco1rhm

Description: Right composition with a function on the index sets yields a ring homomorphism of structure powers. (Contributed by Mario Carneiro, 12-Jun-2015)

Ref Expression
Hypotheses pwsco1rhm.y 
|- Y = ( R ^s A )
pwsco1rhm.z 
|- Z = ( R ^s B )
pwsco1rhm.c 
|- C = ( Base ` Z )
pwsco1rhm.r 
|- ( ph -> R e. Ring )
pwsco1rhm.a 
|- ( ph -> A e. V )
pwsco1rhm.b 
|- ( ph -> B e. W )
pwsco1rhm.f 
|- ( ph -> F : A --> B )
Assertion pwsco1rhm 
|- ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z RingHom Y ) )

Proof

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