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 𝑠 A
pwsco2mhm.z Z = S 𝑠 A
pwsco2mhm.b B = Base Y
pwsco2mhm.a φ A V
pwsco2mhm.f φ F R MndHom S
Assertion pwsco2mhm φ g B F g Y MndHom Z

Proof

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