Metamath Proof Explorer

Theorem pwsco1mhm

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

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

Proof

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