Metamath Proof Explorer

Theorem pwsco2mhm

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

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

Proof

Step Hyp Ref Expression
1 pwsco2mhm.y 
 |-  Y = ( R ^s A )
2 pwsco2mhm.z 
 |-  Z = ( S ^s A )
3 pwsco2mhm.b 
 |-  B = ( Base ` Y )
4 pwsco2mhm.a 
 |-  ( ph -> A e. V )
5 pwsco2mhm.f 
 |-  ( ph -> F e. ( R MndHom S ) )
6 mhmrcl1 
 |-  ( F e. ( R MndHom S ) -> R e. Mnd )
7 5 6 syl 
 |-  ( ph -> R e. Mnd )
8 1 pwsmnd 
 |-  ( ( R e. Mnd /\ A e. V ) -> Y e. Mnd )
9 7 4 8 syl2anc 
 |-  ( ph -> Y e. Mnd )
10 mhmrcl2 
 |-  ( F e. ( R MndHom S ) -> S e. Mnd )
11 5 10 syl 
 |-  ( ph -> S e. Mnd )
12 2 pwsmnd 
 |-  ( ( S e. Mnd /\ A e. V ) -> Z e. Mnd )
13 11 4 12 syl2anc 
 |-  ( ph -> Z e. Mnd )
14 eqid 
 |-  ( Base ` R ) = ( Base ` R )
15 eqid 
 |-  ( Base ` S ) = ( Base ` S )
16 14 15 mhmf 
 |-  ( F e. ( R MndHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
17 5 16 syl 
 |-  ( ph -> F : ( Base ` R ) --> ( Base ` S ) )
18 7 adantr 
 |-  ( ( ph /\ g e. B ) -> R e. Mnd )
19 4 adantr 
 |-  ( ( ph /\ g e. B ) -> A e. V )
20 simpr 
 |-  ( ( ph /\ g e. B ) -> g e. B )
21 1 14 3 18 19 20 pwselbas 
 |-  ( ( ph /\ g e. B ) -> g : A --> ( Base ` R ) )
22 fco 
 |-  ( ( F : ( Base ` R ) --> ( Base ` S ) /\ g : A --> ( Base ` R ) ) -> ( F o. g ) : A --> ( Base ` S ) )
23 17 21 22 syl2an2r 
 |-  ( ( ph /\ g e. B ) -> ( F o. g ) : A --> ( Base ` S ) )
24 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
25 2 15 24 pwselbasb 
 |-  ( ( S e. Mnd /\ A e. V ) -> ( ( F o. g ) e. ( Base ` Z ) <-> ( F o. g ) : A --> ( Base ` S ) ) )
26 11 19 25 syl2an2r 
 |-  ( ( ph /\ g e. B ) -> ( ( F o. g ) e. ( Base ` Z ) <-> ( F o. g ) : A --> ( Base ` S ) ) )
27 23 26 mpbird 
 |-  ( ( ph /\ g e. B ) -> ( F o. g ) e. ( Base ` Z ) )
28 27 fmpttd 
 |-  ( ph -> ( g e. B |-> ( F o. g ) ) : B --> ( Base ` Z ) )
29 5 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F e. ( R MndHom S ) )
30 29 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> F e. ( R MndHom S ) )
31 29 6 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> R e. Mnd )
32 4 adantr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> A e. V )
33 simprl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x e. B )
34 1 14 3 31 32 33 pwselbas 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x : A --> ( Base ` R ) )
35 34 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( x ` w ) e. ( Base ` R ) )
36 simprr 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y e. B )
37 1 14 3 31 32 36 pwselbas 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y : A --> ( Base ` R ) )
38 37 ffvelrnda 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( y ` w ) e. ( Base ` R ) )
39 eqid 
 |-  ( +g ` R ) = ( +g ` R )
40 eqid 
 |-  ( +g ` S ) = ( +g ` S )
41 14 39 40 mhmlin 
 |-  ( ( F e. ( R MndHom S ) /\ ( x ` w ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` w ) ) ( +g ` S ) ( F ` ( y ` w ) ) ) )
42 30 35 38 41 syl3anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) = ( ( F ` ( x ` w ) ) ( +g ` S ) ( F ` ( y ` w ) ) ) )
43 42 mpteq2dva 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( w e. A |-> ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) ) = ( w e. A |-> ( ( F ` ( x ` w ) ) ( +g ` S ) ( F ` ( y ` w ) ) ) ) )
44 fvexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( F ` ( x ` w ) ) e. _V )
45 fvexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( F ` ( y ` w ) ) e. _V )
46 34 feqmptd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> x = ( w e. A |-> ( x ` w ) ) )
47 29 16 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F : ( Base ` R ) --> ( Base ` S ) )
48 47 feqmptd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> F = ( z e. ( Base ` R ) |-> ( F ` z ) ) )
49 fveq2 
 |-  ( z = ( x ` w ) -> ( F ` z ) = ( F ` ( x ` w ) ) )
50 35 46 48 49 fmptco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. x ) = ( w e. A |-> ( F ` ( x ` w ) ) ) )
51 37 feqmptd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> y = ( w e. A |-> ( y ` w ) ) )
52 fveq2 
 |-  ( z = ( y ` w ) -> ( F ` z ) = ( F ` ( y ` w ) ) )
53 38 51 48 52 fmptco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. y ) = ( w e. A |-> ( F ` ( y ` w ) ) ) )
54 32 44 45 50 53 offval2 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F o. x ) oF ( +g ` S ) ( F o. y ) ) = ( w e. A |-> ( ( F ` ( x ` w ) ) ( +g ` S ) ( F ` ( y ` w ) ) ) ) )
55 43 54 eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( w e. A |-> ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) ) = ( ( F o. x ) oF ( +g ` S ) ( F o. y ) ) )
56 31 adantr 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> R e. Mnd )
57 14 39 mndcl 
 |-  ( ( R e. Mnd /\ ( x ` w ) e. ( Base ` R ) /\ ( y ` w ) e. ( Base ` R ) ) -> ( ( x ` w ) ( +g ` R ) ( y ` w ) ) e. ( Base ` R ) )
58 56 35 38 57 syl3anc 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( ( x ` w ) ( +g ` R ) ( y ` w ) ) e. ( Base ` R ) )
59 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
60 1 3 31 32 33 36 39 59 pwsplusgval 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` Y ) y ) = ( x oF ( +g ` R ) y ) )
61 fvexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( x ` w ) e. _V )
62 fvexd 
 |-  ( ( ( ph /\ ( x e. B /\ y e. B ) ) /\ w e. A ) -> ( y ` w ) e. _V )
63 32 61 62 46 51 offval2 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x oF ( +g ` R ) y ) = ( w e. A |-> ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) )
64 60 63 eqtrd 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` Y ) y ) = ( w e. A |-> ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) )
65 fveq2 
 |-  ( z = ( ( x ` w ) ( +g ` R ) ( y ` w ) ) -> ( F ` z ) = ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) )
66 58 64 48 65 fmptco 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. ( x ( +g ` Y ) y ) ) = ( w e. A |-> ( F ` ( ( x ` w ) ( +g ` R ) ( y ` w ) ) ) ) )
67 29 10 syl 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> S e. Mnd )
68 fco 
 |-  ( ( F : ( Base ` R ) --> ( Base ` S ) /\ x : A --> ( Base ` R ) ) -> ( F o. x ) : A --> ( Base ` S ) )
69 47 34 68 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. x ) : A --> ( Base ` S ) )
70 2 15 24 pwselbasb 
 |-  ( ( S e. Mnd /\ A e. V ) -> ( ( F o. x ) e. ( Base ` Z ) <-> ( F o. x ) : A --> ( Base ` S ) ) )
71 67 32 70 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F o. x ) e. ( Base ` Z ) <-> ( F o. x ) : A --> ( Base ` S ) ) )
72 69 71 mpbird 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. x ) e. ( Base ` Z ) )
73 fco 
 |-  ( ( F : ( Base ` R ) --> ( Base ` S ) /\ y : A --> ( Base ` R ) ) -> ( F o. y ) : A --> ( Base ` S ) )
74 47 37 73 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. y ) : A --> ( Base ` S ) )
75 2 15 24 pwselbasb 
 |-  ( ( S e. Mnd /\ A e. V ) -> ( ( F o. y ) e. ( Base ` Z ) <-> ( F o. y ) : A --> ( Base ` S ) ) )
76 67 32 75 syl2anc 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F o. y ) e. ( Base ` Z ) <-> ( F o. y ) : A --> ( Base ` S ) ) )
77 74 76 mpbird 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. y ) e. ( Base ` Z ) )
78 eqid 
 |-  ( +g ` Z ) = ( +g ` Z )
79 2 24 67 32 72 77 40 78 pwsplusgval 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( F o. x ) ( +g ` Z ) ( F o. y ) ) = ( ( F o. x ) oF ( +g ` S ) ( F o. y ) ) )
80 55 66 79 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. ( x ( +g ` Y ) y ) ) = ( ( F o. x ) ( +g ` Z ) ( F o. y ) ) )
81 eqid 
 |-  ( g e. B |-> ( F o. g ) ) = ( g e. B |-> ( F o. g ) )
82 coeq2 
 |-  ( g = ( x ( +g ` Y ) y ) -> ( F o. g ) = ( F o. ( x ( +g ` Y ) y ) ) )
83 3 59 mndcl 
 |-  ( ( Y e. Mnd /\ x e. B /\ y e. B ) -> ( x ( +g ` Y ) y ) e. B )
84 83 3expb 
 |-  ( ( Y e. Mnd /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` Y ) y ) e. B )
85 9 84 sylan 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` Y ) y ) e. B )
86 coexg 
 |-  ( ( F e. ( R MndHom S ) /\ ( x ( +g ` Y ) y ) e. B ) -> ( F o. ( x ( +g ` Y ) y ) ) e. _V )
87 5 85 86 syl2an2r 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F o. ( x ( +g ` Y ) y ) ) e. _V )
88 81 82 85 87 fvmptd3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( g e. B |-> ( F o. g ) ) ` ( x ( +g ` Y ) y ) ) = ( F o. ( x ( +g ` Y ) y ) ) )
89 coeq2 
 |-  ( g = x -> ( F o. g ) = ( F o. x ) )
90 81 89 33 72 fvmptd3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( g e. B |-> ( F o. g ) ) ` x ) = ( F o. x ) )
91 coeq2 
 |-  ( g = y -> ( F o. g ) = ( F o. y ) )
92 81 91 36 77 fvmptd3 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( g e. B |-> ( F o. g ) ) ` y ) = ( F o. y ) )
93 90 92 oveq12d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( ( g e. B |-> ( F o. g ) ) ` x ) ( +g ` Z ) ( ( g e. B |-> ( F o. g ) ) ` y ) ) = ( ( F o. x ) ( +g ` Z ) ( F o. y ) ) )
94 80 88 93 3eqtr4d 
 |-  ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( ( g e. B |-> ( F o. g ) ) ` ( x ( +g ` Y ) y ) ) = ( ( ( g e. B |-> ( F o. g ) ) ` x ) ( +g ` Z ) ( ( g e. B |-> ( F o. g ) ) ` y ) ) )
95 94 ralrimivva 
 |-  ( ph -> A. x e. B A. y e. B ( ( g e. B |-> ( F o. g ) ) ` ( x ( +g ` Y ) y ) ) = ( ( ( g e. B |-> ( F o. g ) ) ` x ) ( +g ` Z ) ( ( g e. B |-> ( F o. g ) ) ` y ) ) )
96 coeq2 
 |-  ( g = ( 0g ` Y ) -> ( F o. g ) = ( F o. ( 0g ` Y ) ) )
97 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
98 3 97 mndidcl 
 |-  ( Y e. Mnd -> ( 0g ` Y ) e. B )
99 9 98 syl 
 |-  ( ph -> ( 0g ` Y ) e. B )
100 coexg 
 |-  ( ( F e. ( R MndHom S ) /\ ( 0g ` Y ) e. B ) -> ( F o. ( 0g ` Y ) ) e. _V )
101 5 99 100 syl2anc 
 |-  ( ph -> ( F o. ( 0g ` Y ) ) e. _V )
102 81 96 99 101 fvmptd3 
 |-  ( ph -> ( ( g e. B |-> ( F o. g ) ) ` ( 0g ` Y ) ) = ( F o. ( 0g ` Y ) ) )
103 17 ffnd 
 |-  ( ph -> F Fn ( Base ` R ) )
104 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
105 14 104 mndidcl 
 |-  ( R e. Mnd -> ( 0g ` R ) e. ( Base ` R ) )
106 7 105 syl 
 |-  ( ph -> ( 0g ` R ) e. ( Base ` R ) )
107 fcoconst 
 |-  ( ( F Fn ( Base ` R ) /\ ( 0g ` R ) e. ( Base ` R ) ) -> ( F o. ( A X. { ( 0g ` R ) } ) ) = ( A X. { ( F ` ( 0g ` R ) ) } ) )
108 103 106 107 syl2anc 
 |-  ( ph -> ( F o. ( A X. { ( 0g ` R ) } ) ) = ( A X. { ( F ` ( 0g ` R ) ) } ) )
109 1 104 pws0g 
 |-  ( ( R e. Mnd /\ A e. V ) -> ( A X. { ( 0g ` R ) } ) = ( 0g ` Y ) )
110 7 4 109 syl2anc 
 |-  ( ph -> ( A X. { ( 0g ` R ) } ) = ( 0g ` Y ) )
111 110 coeq2d 
 |-  ( ph -> ( F o. ( A X. { ( 0g ` R ) } ) ) = ( F o. ( 0g ` Y ) ) )
112 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
113 104 112 mhm0 
 |-  ( F e. ( R MndHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
114 5 113 syl 
 |-  ( ph -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
115 114 sneqd 
 |-  ( ph -> { ( F ` ( 0g ` R ) ) } = { ( 0g ` S ) } )
116 115 xpeq2d 
 |-  ( ph -> ( A X. { ( F ` ( 0g ` R ) ) } ) = ( A X. { ( 0g ` S ) } ) )
117 108 111 116 3eqtr3d 
 |-  ( ph -> ( F o. ( 0g ` Y ) ) = ( A X. { ( 0g ` S ) } ) )
118 2 112 pws0g 
 |-  ( ( S e. Mnd /\ A e. V ) -> ( A X. { ( 0g ` S ) } ) = ( 0g ` Z ) )
119 11 4 118 syl2anc 
 |-  ( ph -> ( A X. { ( 0g ` S ) } ) = ( 0g ` Z ) )
120 102 117 119 3eqtrd 
 |-  ( ph -> ( ( g e. B |-> ( F o. g ) ) ` ( 0g ` Y ) ) = ( 0g ` Z ) )
121 28 95 120 3jca 
 |-  ( ph -> ( ( g e. B |-> ( F o. g ) ) : B --> ( Base ` Z ) /\ A. x e. B A. y e. B ( ( g e. B |-> ( F o. g ) ) ` ( x ( +g ` Y ) y ) ) = ( ( ( g e. B |-> ( F o. g ) ) ` x ) ( +g ` Z ) ( ( g e. B |-> ( F o. g ) ) ` y ) ) /\ ( ( g e. B |-> ( F o. g ) ) ` ( 0g ` Y ) ) = ( 0g ` Z ) ) )
122 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
123 3 24 59 78 97 122 ismhm 
 |-  ( ( g e. B |-> ( F o. g ) ) e. ( Y MndHom Z ) <-> ( ( Y e. Mnd /\ Z e. Mnd ) /\ ( ( g e. B |-> ( F o. g ) ) : B --> ( Base ` Z ) /\ A. x e. B A. y e. B ( ( g e. B |-> ( F o. g ) ) ` ( x ( +g ` Y ) y ) ) = ( ( ( g e. B |-> ( F o. g ) ) ` x ) ( +g ` Z ) ( ( g e. B |-> ( F o. g ) ) ` y ) ) /\ ( ( g e. B |-> ( F o. g ) ) ` ( 0g ` Y ) ) = ( 0g ` Z ) ) ) )
124 9 13 121 123 syl21anbrc 
 |-  ( ph -> ( g e. B |-> ( F o. g ) ) e. ( Y MndHom Z ) )