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 ffvelcdmda 
 |-  ( ( ( 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 7 5 fexd 
 |-  ( ph -> F e. _V )
73 72 adantr 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> F e. _V )
74 coexg 
 |-  ( ( ( x ( +g ` Z ) y ) e. _V /\ F e. _V ) -> ( ( x ( +g ` Z ) y ) o. F ) e. _V )
75 71 73 74 sylancr 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( x ( +g ` Z ) y ) o. F ) e. _V )
76 66 67 70 75 fvmptd3 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( g e. C |-> ( g o. F ) ) ` ( x ( +g ` Z ) y ) ) = ( ( x ( +g ` Z ) y ) o. F ) )
77 coeq1 
 |-  ( g = x -> ( g o. F ) = ( x o. F ) )
78 coexg 
 |-  ( ( x e. C /\ F e. _V ) -> ( x o. F ) e. _V )
79 33 73 78 syl2anc 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x o. F ) e. _V )
80 66 77 33 79 fvmptd3 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( g e. C |-> ( g o. F ) ) ` x ) = ( x o. F ) )
81 coeq1 
 |-  ( g = y -> ( g o. F ) = ( y o. F ) )
82 coexg 
 |-  ( ( y e. C /\ F e. _V ) -> ( y o. F ) e. _V )
83 38 73 82 syl2anc 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( y o. F ) e. _V )
84 66 81 38 83 fvmptd3 
 |-  ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( ( g e. C |-> ( g o. F ) ) ` y ) = ( y o. F ) )
85 80 84 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 ) ) )
86 65 76 85 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 ) ) )
87 86 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 ) ) )
88 coeq1 
 |-  ( g = ( 0g ` Z ) -> ( g o. F ) = ( ( 0g ` Z ) o. F ) )
89 eqid 
 |-  ( 0g ` Z ) = ( 0g ` Z )
90 3 89 mndidcl 
 |-  ( Z e. Mnd -> ( 0g ` Z ) e. C )
91 9 90 syl 
 |-  ( ph -> ( 0g ` Z ) e. C )
92 coexg 
 |-  ( ( ( 0g ` Z ) e. C /\ F e. _V ) -> ( ( 0g ` Z ) o. F ) e. _V )
93 91 72 92 syl2anc 
 |-  ( ph -> ( ( 0g ` Z ) o. F ) e. _V )
94 66 88 91 93 fvmptd3 
 |-  ( ph -> ( ( g e. C |-> ( g o. F ) ) ` ( 0g ` Z ) ) = ( ( 0g ` Z ) o. F ) )
95 2 12 3 4 6 91 pwselbas 
 |-  ( ph -> ( 0g ` Z ) : B --> ( Base ` R ) )
96 fco 
 |-  ( ( ( 0g ` Z ) : B --> ( Base ` R ) /\ F : A --> B ) -> ( ( 0g ` Z ) o. F ) : A --> ( Base ` R ) )
97 95 7 96 syl2anc 
 |-  ( ph -> ( ( 0g ` Z ) o. F ) : A --> ( Base ` R ) )
98 97 ffnd 
 |-  ( ph -> ( ( 0g ` Z ) o. F ) Fn A )
99 fvexd 
 |-  ( ph -> ( 0g ` R ) e. _V )
100 fnconstg 
 |-  ( ( 0g ` R ) e. _V -> ( A X. { ( 0g ` R ) } ) Fn A )
101 99 100 syl 
 |-  ( ph -> ( A X. { ( 0g ` R ) } ) Fn A )
102 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
103 2 102 pws0g 
 |-  ( ( R e. Mnd /\ B e. W ) -> ( B X. { ( 0g ` R ) } ) = ( 0g ` Z ) )
104 4 6 103 syl2anc 
 |-  ( ph -> ( B X. { ( 0g ` R ) } ) = ( 0g ` Z ) )
105 104 fveq1d 
 |-  ( ph -> ( ( B X. { ( 0g ` R ) } ) ` ( F ` x ) ) = ( ( 0g ` Z ) ` ( F ` x ) ) )
106 105 adantr 
 |-  ( ( ph /\ x e. A ) -> ( ( B X. { ( 0g ` R ) } ) ` ( F ` x ) ) = ( ( 0g ` Z ) ` ( F ` x ) ) )
107 fvex 
 |-  ( 0g ` R ) e. _V
108 7 ffvelcdmda 
 |-  ( ( ph /\ x e. A ) -> ( F ` x ) e. B )
109 fvconst2g 
 |-  ( ( ( 0g ` R ) e. _V /\ ( F ` x ) e. B ) -> ( ( B X. { ( 0g ` R ) } ) ` ( F ` x ) ) = ( 0g ` R ) )
110 107 108 109 sylancr 
 |-  ( ( ph /\ x e. A ) -> ( ( B X. { ( 0g ` R ) } ) ` ( F ` x ) ) = ( 0g ` R ) )
111 106 110 eqtr3d 
 |-  ( ( ph /\ x e. A ) -> ( ( 0g ` Z ) ` ( F ` x ) ) = ( 0g ` R ) )
112 fvco3 
 |-  ( ( F : A --> B /\ x e. A ) -> ( ( ( 0g ` Z ) o. F ) ` x ) = ( ( 0g ` Z ) ` ( F ` x ) ) )
113 7 112 sylan 
 |-  ( ( ph /\ x e. A ) -> ( ( ( 0g ` Z ) o. F ) ` x ) = ( ( 0g ` Z ) ` ( F ` x ) ) )
114 fvconst2g 
 |-  ( ( ( 0g ` R ) e. _V /\ x e. A ) -> ( ( A X. { ( 0g ` R ) } ) ` x ) = ( 0g ` R ) )
115 99 114 sylan 
 |-  ( ( ph /\ x e. A ) -> ( ( A X. { ( 0g ` R ) } ) ` x ) = ( 0g ` R ) )
116 111 113 115 3eqtr4d 
 |-  ( ( ph /\ x e. A ) -> ( ( ( 0g ` Z ) o. F ) ` x ) = ( ( A X. { ( 0g ` R ) } ) ` x ) )
117 98 101 116 eqfnfvd 
 |-  ( ph -> ( ( 0g ` Z ) o. F ) = ( A X. { ( 0g ` R ) } ) )
118 1 102 pws0g 
 |-  ( ( R e. Mnd /\ A e. V ) -> ( A X. { ( 0g ` R ) } ) = ( 0g ` Y ) )
119 4 5 118 syl2anc 
 |-  ( ph -> ( A X. { ( 0g ` R ) } ) = ( 0g ` Y ) )
120 94 117 119 3eqtrd 
 |-  ( ph -> ( ( g e. C |-> ( g o. F ) ) ` ( 0g ` Z ) ) = ( 0g ` Y ) )
121 24 87 120 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 ) ) )
122 eqid 
 |-  ( 0g ` Y ) = ( 0g ` Y )
123 3 19 57 55 89 122 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 ) ) ) )
124 9 11 121 123 syl21anbrc 
 |-  ( ph -> ( g e. C |-> ( g o. F ) ) e. ( Z MndHom Y ) )