Metamath Proof Explorer


Theorem amgmwlem

Description: Weighted version of amgmlem . (Contributed by Kunhao Zheng, 19-Jun-2021)

Ref Expression
Hypotheses amgmwlem.0 M = mulGrp fld
amgmwlem.1 φ A Fin
amgmwlem.2 φ A
amgmwlem.3 φ F : A +
amgmwlem.4 φ W : A +
amgmwlem.5 φ fld W = 1
Assertion amgmwlem φ M F c f W fld F × f W

Proof

Step Hyp Ref Expression
1 amgmwlem.0 M = mulGrp fld
2 amgmwlem.1 φ A Fin
3 amgmwlem.2 φ A
4 amgmwlem.3 φ F : A +
5 amgmwlem.4 φ W : A +
6 amgmwlem.5 φ fld W = 1
7 4 ffvelrnda φ k A F k +
8 5 ffvelrnda φ k A W k +
9 8 rpred φ k A W k
10 7 9 rpcxpcld φ k A F k W k +
11 10 relogcld φ k A log F k W k
12 11 recnd φ k A log F k W k
13 2 12 gsumfsum φ fld k A log F k W k = k A log F k W k
14 12 negnegd φ k A log F k W k = log F k W k
15 14 sumeq2dv φ k A log F k W k = k A log F k W k
16 11 renegcld φ k A log F k W k
17 16 recnd φ k A log F k W k
18 2 17 fsumneg φ k A log F k W k = k A log F k W k
19 7 9 logcxpd φ k A log F k W k = W k log F k
20 19 negeqd φ k A log F k W k = W k log F k
21 20 sumeq2dv φ k A log F k W k = k A W k log F k
22 21 negeqd φ k A log F k W k = k A W k log F k
23 8 rpcnd φ k A W k
24 7 relogcld φ k A log F k
25 24 recnd φ k A log F k
26 23 25 mulneg2d φ k A W k log F k = W k log F k
27 26 eqcomd φ k A W k log F k = W k log F k
28 27 sumeq2dv φ k A W k log F k = k A W k log F k
29 28 negeqd φ k A W k log F k = k A W k log F k
30 18 22 29 3eqtrd φ k A log F k W k = k A W k log F k
31 13 15 30 3eqtr2rd φ k A W k log F k = fld k A log F k W k
32 negex log F k V
33 32 a1i φ k A log F k V
34 5 feqmptd φ W = k A W k
35 eqidd φ k A log F k = k A log F k
36 2 8 33 34 35 offval2 φ W × f k A log F k = k A W k log F k
37 36 oveq2d φ fld W × f k A log F k = fld k A W k log F k
38 25 negcld φ k A log F k
39 23 38 mulcld φ k A W k log F k
40 2 39 gsumfsum φ fld k A W k log F k = k A W k log F k
41 37 40 eqtrd φ fld W × f k A log F k = k A W k log F k
42 41 negeqd φ fld W × f k A log F k = k A W k log F k
43 relogf1o log + : + 1-1 onto
44 f1of log + : + 1-1 onto log + : +
45 43 44 ax-mp log + : +
46 rpre y + y
47 46 anim2i x + y + x + y
48 47 adantl φ x + y + x + y
49 rpcxpcl x + y x y +
50 48 49 syl φ x + y + x y +
51 inidm A A = A
52 50 4 5 2 2 51 off φ F c f W : A +
53 fcompt log + : + F c f W : A + log + F c f W = k A log + F c f W k
54 45 52 53 sylancr φ log + F c f W = k A log + F c f W k
55 52 ffvelrnda φ k A F c f W k +
56 fvres F c f W k + log + F c f W k = log F c f W k
57 55 56 syl φ k A log + F c f W k = log F c f W k
58 4 ffnd φ F Fn A
59 5 ffnd φ W Fn A
60 eqidd φ k A F k = F k
61 eqidd φ k A W k = W k
62 58 59 2 2 51 60 61 ofval φ k A F c f W k = F k W k
63 62 fveq2d φ k A log F c f W k = log F k W k
64 57 63 eqtrd φ k A log + F c f W k = log F k W k
65 64 mpteq2dva φ k A log + F c f W k = k A log F k W k
66 54 65 eqtrd φ log + F c f W = k A log F k W k
67 66 oveq2d φ fld log + F c f W = fld k A log F k W k
68 31 42 67 3eqtr4d φ fld W × f k A log F k = fld log + F c f W
69 1 oveq1i M 𝑠 0 = mulGrp fld 𝑠 0
70 69 rpmsubg + SubGrp M 𝑠 0
71 subgsubm + SubGrp M 𝑠 0 + SubMnd M 𝑠 0
72 70 71 ax-mp + SubMnd M 𝑠 0
73 cnring fld Ring
74 cnfldbas = Base fld
75 cnfld0 0 = 0 fld
76 cndrng fld DivRing
77 74 75 76 drngui 0 = Unit fld
78 77 1 unitsubm fld Ring 0 SubMnd M
79 eqid M 𝑠 0 = M 𝑠 0
80 79 subsubm 0 SubMnd M + SubMnd M 𝑠 0 + SubMnd M + 0
81 73 78 80 mp2b + SubMnd M 𝑠 0 + SubMnd M + 0
82 72 81 mpbi + SubMnd M + 0
83 82 simpli + SubMnd M
84 eqid M 𝑠 + = M 𝑠 +
85 84 submbas + SubMnd M + = Base M 𝑠 +
86 83 85 ax-mp + = Base M 𝑠 +
87 cnfld1 1 = 1 fld
88 1 87 ringidval 1 = 0 M
89 eqid 0 M = 0 M
90 84 89 subm0 + SubMnd M 0 M = 0 M 𝑠 +
91 83 90 ax-mp 0 M = 0 M 𝑠 +
92 88 91 eqtri 1 = 0 M 𝑠 +
93 cncrng fld CRing
94 1 crngmgp fld CRing M CMnd
95 93 94 mp1i φ M CMnd
96 84 submmnd + SubMnd M M 𝑠 + Mnd
97 83 96 mp1i φ M 𝑠 + Mnd
98 84 subcmn M CMnd M 𝑠 + Mnd M 𝑠 + CMnd
99 95 97 98 syl2anc φ M 𝑠 + CMnd
100 resubdrg SubRing fld fld DivRing
101 100 simpli SubRing fld
102 df-refld fld = fld 𝑠
103 102 subrgring SubRing fld fld Ring
104 101 103 ax-mp fld Ring
105 ringmnd fld Ring fld Mnd
106 104 105 mp1i φ fld Mnd
107 1 oveq1i M 𝑠 + = mulGrp fld 𝑠 +
108 107 reloggim log + M 𝑠 + GrpIso fld
109 gimghm log + M 𝑠 + GrpIso fld log + M 𝑠 + GrpHom fld
110 108 109 ax-mp log + M 𝑠 + GrpHom fld
111 ghmmhm log + M 𝑠 + GrpHom fld log + M 𝑠 + MndHom fld
112 110 111 mp1i φ log + M 𝑠 + MndHom fld
113 1red φ 1
114 52 2 113 fdmfifsupp φ finSupp 1 F c f W
115 86 92 99 106 2 112 52 114 gsummhm φ fld log + F c f W = log + M 𝑠 + F c f W
116 subrgsubg SubRing fld SubGrp fld
117 101 116 ax-mp SubGrp fld
118 subgsubm SubGrp fld SubMnd fld
119 117 118 ax-mp SubMnd fld
120 119 a1i φ SubMnd fld
121 43 44 mp1i φ log + : +
122 fco log + : + F c f W : A + log + F c f W : A
123 121 52 122 syl2anc φ log + F c f W : A
124 2 120 123 102 gsumsubm φ fld log + F c f W = fld log + F c f W
125 83 a1i φ + SubMnd M
126 2 125 52 84 gsumsubm φ M F c f W = M 𝑠 + F c f W
127 126 fveq2d φ log + M F c f W = log + M 𝑠 + F c f W
128 115 124 127 3eqtr4d φ fld log + F c f W = log + M F c f W
129 88 95 2 125 52 114 gsumsubmcl φ M F c f W +
130 fvres M F c f W + log + M F c f W = log M F c f W
131 129 130 syl φ log + M F c f W = log M F c f W
132 68 128 131 3eqtrd φ fld W × f k A log F k = log M F c f W
133 simprl φ x + y + x +
134 133 rpcnd φ x + y + x
135 simprr φ x + y + y +
136 135 rpcnd φ x + y + y
137 134 136 mulcomd φ x + y + x y = y x
138 2 5 4 137 caofcom φ W × f F = F × f W
139 138 oveq2d φ fld W × f F = fld F × f W
140 4 feqmptd φ F = k A F k
141 2 8 7 34 140 offval2 φ W × f F = k A W k F k
142 141 oveq2d φ fld W × f F = fld k A W k F k
143 8 7 rpmulcld φ k A W k F k +
144 143 rpcnd φ k A W k F k
145 2 144 gsumfsum φ fld k A W k F k = k A W k F k
146 142 145 eqtrd φ fld W × f F = k A W k F k
147 2 3 143 fsumrpcl φ k A W k F k +
148 146 147 eqeltrd φ fld W × f F +
149 139 148 eqeltrrd φ fld F × f W +
150 149 relogcld φ log fld F × f W
151 ringcmn fld Ring fld CMnd
152 73 151 mp1i φ fld CMnd
153 remulcl x y x y
154 153 adantl φ x y x y
155 rpssre +
156 fss W : A + + W : A
157 5 155 156 sylancl φ W : A
158 24 renegcld φ k A log F k
159 158 fmpttd φ k A log F k : A
160 154 157 159 2 2 51 off φ W × f k A log F k : A
161 0red φ 0
162 160 2 161 fdmfifsupp φ finSupp 0 W × f k A log F k
163 75 152 2 120 160 162 gsumsubmcl φ fld W × f k A log F k
164 155 a1i φ +
165 simpr φ w + w +
166 165 relogcld φ w + log w
167 166 renegcld φ w + log w
168 167 fmpttd φ w + log w : +
169 simpl a + b + a +
170 ioorp 0 +∞ = +
171 169 170 eleqtrrdi a + b + a 0 +∞
172 simpr a + b + b +
173 172 170 eleqtrrdi a + b + b 0 +∞
174 iccssioo2 a 0 +∞ b 0 +∞ a b 0 +∞
175 171 173 174 syl2anc a + b + a b 0 +∞
176 175 170 sseqtrdi a + b + a b +
177 176 adantl φ a + b + a b +
178 ioossico 0 +∞ 0 +∞
179 170 178 eqsstrri + 0 +∞
180 fss W : A + + 0 +∞ W : A 0 +∞
181 5 179 180 sylancl φ W : A 0 +∞
182 0lt1 0 < 1
183 182 6 breqtrrid φ 0 < fld W
184 logccv x + y + x < y t 0 1 t log x + 1 t log y < log t x + 1 t y
185 184 3adant1 φ x + y + x < y t 0 1 t log x + 1 t log y < log t x + 1 t y
186 elioore t 0 1 t
187 186 3ad2ant3 φ x + y + x < y t 0 1 t
188 simp21 φ x + y + x < y t 0 1 x +
189 188 relogcld φ x + y + x < y t 0 1 log x
190 187 189 remulcld φ x + y + x < y t 0 1 t log x
191 1red t 0 1 1
192 191 186 resubcld t 0 1 1 t
193 192 3ad2ant3 φ x + y + x < y t 0 1 1 t
194 simp22 φ x + y + x < y t 0 1 y +
195 194 relogcld φ x + y + x < y t 0 1 log y
196 193 195 remulcld φ x + y + x < y t 0 1 1 t log y
197 190 196 readdcld φ x + y + x < y t 0 1 t log x + 1 t log y
198 eliooord t 0 1 0 < t t < 1
199 198 simpld t 0 1 0 < t
200 186 199 elrpd t 0 1 t +
201 200 3ad2ant3 φ x + y + x < y t 0 1 t +
202 201 188 rpmulcld φ x + y + x < y t 0 1 t x +
203 0red t 0 1 0
204 198 simprd t 0 1 t < 1
205 1m0e1 1 0 = 1
206 204 205 breqtrrdi t 0 1 t < 1 0
207 186 191 203 206 ltsub13d t 0 1 0 < 1 t
208 192 207 elrpd t 0 1 1 t +
209 208 3ad2ant3 φ x + y + x < y t 0 1 1 t +
210 209 194 rpmulcld φ x + y + x < y t 0 1 1 t y +
211 rpaddcl t x + 1 t y + t x + 1 t y +
212 202 210 211 syl2anc φ x + y + x < y t 0 1 t x + 1 t y +
213 212 relogcld φ x + y + x < y t 0 1 log t x + 1 t y
214 197 213 ltnegd φ x + y + x < y t 0 1 t log x + 1 t log y < log t x + 1 t y log t x + 1 t y < t log x + 1 t log y
215 185 214 mpbid φ x + y + x < y t 0 1 log t x + 1 t y < t log x + 1 t log y
216 eqidd φ x + y + x < y t 0 1 w + log w = w + log w
217 fveq2 w = t x + 1 t y log w = log t x + 1 t y
218 217 adantl φ x + y + x < y t 0 1 w = t x + 1 t y log w = log t x + 1 t y
219 218 negeqd φ x + y + x < y t 0 1 w = t x + 1 t y log w = log t x + 1 t y
220 negex log t x + 1 t y V
221 220 a1i φ x + y + x < y t 0 1 log t x + 1 t y V
222 216 219 212 221 fvmptd φ x + y + x < y t 0 1 w + log w t x + 1 t y = log t x + 1 t y
223 fveq2 w = x log w = log x
224 223 negeqd w = x log w = log x
225 eqid w + log w = w + log w
226 negex log w V
227 224 225 226 fvmpt3i x + w + log w x = log x
228 188 227 syl φ x + y + x < y t 0 1 w + log w x = log x
229 228 oveq2d φ x + y + x < y t 0 1 t w + log w x = t log x
230 187 recnd φ x + y + x < y t 0 1 t
231 189 recnd φ x + y + x < y t 0 1 log x
232 230 231 mulneg2d φ x + y + x < y t 0 1 t log x = t log x
233 229 232 eqtrd φ x + y + x < y t 0 1 t w + log w x = t log x
234 fveq2 w = y log w = log y
235 234 negeqd w = y log w = log y
236 235 225 226 fvmpt3i y + w + log w y = log y
237 194 236 syl φ x + y + x < y t 0 1 w + log w y = log y
238 237 oveq2d φ x + y + x < y t 0 1 1 t w + log w y = 1 t log y
239 209 rpcnd φ x + y + x < y t 0 1 1 t
240 195 recnd φ x + y + x < y t 0 1 log y
241 239 240 mulneg2d φ x + y + x < y t 0 1 1 t log y = 1 t log y
242 238 241 eqtrd φ x + y + x < y t 0 1 1 t w + log w y = 1 t log y
243 233 242 oveq12d φ x + y + x < y t 0 1 t w + log w x + 1 t w + log w y = - t log x + 1 t log y
244 190 recnd φ x + y + x < y t 0 1 t log x
245 196 recnd φ x + y + x < y t 0 1 1 t log y
246 244 245 negdid φ x + y + x < y t 0 1 t log x + 1 t log y = - t log x + 1 t log y
247 243 246 eqtr4d φ x + y + x < y t 0 1 t w + log w x + 1 t w + log w y = t log x + 1 t log y
248 215 222 247 3brtr4d φ x + y + x < y t 0 1 w + log w t x + 1 t y < t w + log w x + 1 t w + log w y
249 164 168 177 248 scvxcvx φ u + v + s 0 1 w + log w s u + 1 s v s w + log w u + 1 s w + log w v
250 164 168 177 2 181 4 183 249 jensen φ fld W × f F fld W + w + log w fld W × f F fld W fld W × f w + log w F fld W
251 250 simprd φ w + log w fld W × f F fld W fld W × f w + log w F fld W
252 6 oveq2d φ fld W × f F fld W = fld W × f F 1
253 252 fveq2d φ w + log w fld W × f F fld W = w + log w fld W × f F 1
254 148 rpcnd φ fld W × f F
255 254 div1d φ fld W × f F 1 = fld W × f F
256 255 fveq2d φ w + log w fld W × f F 1 = w + log w fld W × f F
257 fveq2 w = fld W × f F log w = log fld W × f F
258 257 negeqd w = fld W × f F log w = log fld W × f F
259 258 225 226 fvmpt3i fld W × f F + w + log w fld W × f F = log fld W × f F
260 148 259 syl φ w + log w fld W × f F = log fld W × f F
261 139 fveq2d φ log fld W × f F = log fld F × f W
262 261 negeqd φ log fld W × f F = log fld F × f W
263 260 262 eqtrd φ w + log w fld W × f F = log fld F × f W
264 253 256 263 3eqtrd φ w + log w fld W × f F fld W = log fld F × f W
265 6 oveq2d φ fld W × f w + log w F fld W = fld W × f w + log w F 1
266 ringmnd fld Ring fld Mnd
267 73 266 ax-mp fld Mnd
268 74 submid fld Mnd SubMnd fld
269 267 268 mp1i φ SubMnd fld
270 mulcl x y x y
271 270 adantl φ x y x y
272 rpcn x + x
273 272 ssriv +
274 273 a1i φ +
275 5 274 fssd φ W : A
276 166 recnd φ w + log w
277 276 negcld φ w + log w
278 277 fmpttd φ w + log w : +
279 fco w + log w : + F : A + w + log w F : A
280 278 4 279 syl2anc φ w + log w F : A
281 271 275 280 2 2 51 off φ W × f w + log w F : A
282 281 2 161 fdmfifsupp φ finSupp 0 W × f w + log w F
283 75 152 2 269 281 282 gsumsubmcl φ fld W × f w + log w F
284 283 div1d φ fld W × f w + log w F 1 = fld W × f w + log w F
285 eqidd φ w + log w = w + log w
286 fveq2 w = F k log w = log F k
287 286 negeqd w = F k log w = log F k
288 7 140 285 287 fmptco φ w + log w F = k A log F k
289 288 oveq2d φ W × f w + log w F = W × f k A log F k
290 289 oveq2d φ fld W × f w + log w F = fld W × f k A log F k
291 265 284 290 3eqtrd φ fld W × f w + log w F fld W = fld W × f k A log F k
292 251 264 291 3brtr3d φ log fld F × f W fld W × f k A log F k
293 150 163 292 lenegcon1d φ fld W × f k A log F k log fld F × f W
294 132 293 eqbrtrrd φ log M F c f W log fld F × f W
295 129 relogcld φ log M F c f W
296 efle log M F c f W log fld F × f W log M F c f W log fld F × f W e log M F c f W e log fld F × f W
297 295 150 296 syl2anc φ log M F c f W log fld F × f W e log M F c f W e log fld F × f W
298 294 297 mpbid φ e log M F c f W e log fld F × f W
299 129 reeflogd φ e log M F c f W = M F c f W
300 299 eqcomd φ M F c f W = e log M F c f W
301 149 reeflogd φ e log fld F × f W = fld F × f W
302 301 eqcomd φ fld F × f W = e log fld F × f W
303 298 300 302 3brtr4d φ M F c f W fld F × f W