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