Users' Mathboxes Mathbox for Kunhao Zheng < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  amgmwlem Structured version   Visualization version   GIF version

Theorem amgmwlem 45269
Description: Weighted version of amgmlem 25573. (Contributed by Kunhao Zheng, 19-Jun-2021.)
Hypotheses
Ref Expression
amgmwlem.0 𝑀 = (mulGrp‘ℂfld)
amgmwlem.1 (𝜑𝐴 ∈ Fin)
amgmwlem.2 (𝜑𝐴 ≠ ∅)
amgmwlem.3 (𝜑𝐹:𝐴⟶ℝ+)
amgmwlem.4 (𝜑𝑊:𝐴⟶ℝ+)
amgmwlem.5 (𝜑 → (ℂfld Σg 𝑊) = 1)
Assertion
Ref Expression
amgmwlem (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) ≤ (ℂfld Σg (𝐹f · 𝑊)))

Proof of Theorem amgmwlem
Dummy variables 𝑎 𝑏 𝑠 𝑢 𝑣 𝑘 𝑦 𝑤 𝑥 𝑡 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 amgmwlem.1 . . . . . . . 8 (𝜑𝐴 ∈ Fin)
2 amgmwlem.3 . . . . . . . . . . . 12 (𝜑𝐹:𝐴⟶ℝ+)
32ffvelrnda 6833 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
4 amgmwlem.4 . . . . . . . . . . . . 13 (𝜑𝑊:𝐴⟶ℝ+)
54ffvelrnda 6833 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
65rpred 12419 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
73, 6rpcxpcld 25321 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(𝑊𝑘)) ∈ ℝ+)
87relogcld 25212 . . . . . . . . 9 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
98recnd 10658 . . . . . . . 8 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
101, 9gsumfsum 20156 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
119negnegd 10977 . . . . . . . 8 ((𝜑𝑘𝐴) → --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
1211sumeq2dv 15051 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
138renegcld 11056 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
1413recnd 10658 . . . . . . . . 9 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
151, 14fsumneg 15133 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
163, 6logcxpd 25322 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = ((𝑊𝑘) · (log‘(𝐹𝑘))))
1716negeqd 10869 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
1817sumeq2dv 15051 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
1918negeqd 10869 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
205rpcnd 12421 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℂ)
213relogcld 25212 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
2221recnd 10658 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℂ)
2320, 22mulneg2d 11083 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
2423eqcomd 2828 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -((𝑊𝑘) · (log‘(𝐹𝑘))) = ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2524sumeq2dv 15051 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2625negeqd 10869 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2715, 19, 263eqtrd 2861 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2810, 12, 273eqtr2rd 2864 . . . . . 6 (𝜑 → -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
29 negex 10873 . . . . . . . . . . 11 -(log‘(𝐹𝑘)) ∈ V
3029a1i 11 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ V)
314feqmptd 6715 . . . . . . . . . 10 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
32 eqidd 2823 . . . . . . . . . 10 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
331, 5, 30, 31, 32offval2 7411 . . . . . . . . 9 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘)))))
3433oveq2d 7156 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))))
3522negcld 10973 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℂ)
3620, 35mulcld 10650 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) ∈ ℂ)
371, 36gsumfsum 20156 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
3834, 37eqtrd 2857 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
3938negeqd 10869 . . . . . 6 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
40 relogf1o 25156 . . . . . . . . . 10 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
41 f1of 6597 . . . . . . . . . 10 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
4240, 41ax-mp 5 . . . . . . . . 9 (log ↾ ℝ+):ℝ+⟶ℝ
43 rpre 12385 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
4443anim2i 619 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
4544adantl 485 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
46 rpcxpcl 25265 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
4745, 46syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
48 inidm 4169 . . . . . . . . . 10 (𝐴𝐴) = 𝐴
4947, 2, 4, 1, 1, 48off 7409 . . . . . . . . 9 (𝜑 → (𝐹f𝑐𝑊):𝐴⟶ℝ+)
50 fcompt 6877 . . . . . . . . 9 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹f𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))))
5142, 49, 50sylancr 590 . . . . . . . 8 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))))
5249ffvelrnda 6833 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹f𝑐𝑊)‘𝑘) ∈ ℝ+)
53 fvres 6671 . . . . . . . . . . 11 (((𝐹f𝑐𝑊)‘𝑘) ∈ ℝ+ → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹f𝑐𝑊)‘𝑘)))
5452, 53syl 17 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹f𝑐𝑊)‘𝑘)))
552ffnd 6495 . . . . . . . . . . . 12 (𝜑𝐹 Fn 𝐴)
564ffnd 6495 . . . . . . . . . . . 12 (𝜑𝑊 Fn 𝐴)
57 eqidd 2823 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) = (𝐹𝑘))
58 eqidd 2823 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) = (𝑊𝑘))
5955, 56, 1, 1, 48, 57, 58ofval 7403 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹f𝑐𝑊)‘𝑘) = ((𝐹𝑘)↑𝑐(𝑊𝑘)))
6059fveq2d 6656 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
6154, 60eqtrd 2857 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
6261mpteq2dva 5137 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
6351, 62eqtrd 2857 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
6463oveq2d 7156 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
6528, 39, 643eqtr4d 2867 . . . . 5 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))))
66 amgmwlem.0 . . . . . . . . . . . . 13 𝑀 = (mulGrp‘ℂfld)
6766oveq1i 7150 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
6867rpmsubg 20153 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
69 subgsubm 18292 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
7068, 69ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
71 cnring 20111 . . . . . . . . . . 11 fld ∈ Ring
72 cnfldbas 20093 . . . . . . . . . . . . 13 ℂ = (Base‘ℂfld)
73 cnfld0 20113 . . . . . . . . . . . . 13 0 = (0g‘ℂfld)
74 cndrng 20118 . . . . . . . . . . . . 13 fld ∈ DivRing
7572, 73, 74drngui 19499 . . . . . . . . . . . 12 (ℂ ∖ {0}) = (Unit‘ℂfld)
7675, 66unitsubm 19414 . . . . . . . . . . 11 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
77 eqid 2822 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
7877subsubm 17972 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
7971, 76, 78mp2b 10 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
8070, 79mpbi 233 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
8180simpli 487 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
82 eqid 2822 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
8382submbas 17970 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀s+)))
8481, 83ax-mp 5 . . . . . . 7 + = (Base‘(𝑀s+))
85 cnfld1 20114 . . . . . . . . 9 1 = (1r‘ℂfld)
8666, 85ringidval 19244 . . . . . . . 8 1 = (0g𝑀)
87 eqid 2822 . . . . . . . . . 10 (0g𝑀) = (0g𝑀)
8882, 87subm0 17971 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (0g𝑀) = (0g‘(𝑀s+)))
8981, 88ax-mp 5 . . . . . . . 8 (0g𝑀) = (0g‘(𝑀s+))
9086, 89eqtri 2845 . . . . . . 7 1 = (0g‘(𝑀s+))
91 cncrng 20110 . . . . . . . . 9 fld ∈ CRing
9266crngmgp 19296 . . . . . . . . 9 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
9391, 92mp1i 13 . . . . . . . 8 (𝜑𝑀 ∈ CMnd)
9482submmnd 17969 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
9581, 94mp1i 13 . . . . . . . 8 (𝜑 → (𝑀s+) ∈ Mnd)
9682subcmn 18948 . . . . . . . 8 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
9793, 95, 96syl2anc 587 . . . . . . 7 (𝜑 → (𝑀s+) ∈ CMnd)
98 resubdrg 20295 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
9998simpli 487 . . . . . . . . 9 ℝ ∈ (SubRing‘ℂfld)
100 df-refld 20292 . . . . . . . . . 10 fld = (ℂflds ℝ)
101100subrgring 19529 . . . . . . . . 9 (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
10299, 101ax-mp 5 . . . . . . . 8 fld ∈ Ring
103 ringmnd 19298 . . . . . . . 8 (ℝfld ∈ Ring → ℝfld ∈ Mnd)
104102, 103mp1i 13 . . . . . . 7 (𝜑 → ℝfld ∈ Mnd)
10566oveq1i 7150 . . . . . . . . . 10 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
106105reloggim 25188 . . . . . . . . 9 (log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld)
107 gimghm 18395 . . . . . . . . 9 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld))
108106, 107ax-mp 5 . . . . . . . 8 (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld)
109 ghmmhm 18359 . . . . . . . 8 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
110108, 109mp1i 13 . . . . . . 7 (𝜑 → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
111 1red 10631 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
11249, 1, 111fdmfifsupp 8831 . . . . . . 7 (𝜑 → (𝐹f𝑐𝑊) finSupp 1)
11384, 90, 97, 104, 1, 110, 49, 112gsummhm 19049 . . . . . 6 (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹f𝑐𝑊))))
114 subrgsubg 19532 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
11599, 114ax-mp 5 . . . . . . . . 9 ℝ ∈ (SubGrp‘ℂfld)
116 subgsubm 18292 . . . . . . . . 9 (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
117115, 116ax-mp 5 . . . . . . . 8 ℝ ∈ (SubMnd‘ℂfld)
118117a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
11940, 41mp1i 13 . . . . . . . 8 (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
120 fco 6512 . . . . . . . 8 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹f𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)):𝐴⟶ℝ)
121119, 49, 120syl2anc 587 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)):𝐴⟶ℝ)
1221, 118, 121, 100gsumsubm 17990 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))))
12381a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
1241, 123, 49, 82gsumsubm 17990 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) = ((𝑀s+) Σg (𝐹f𝑐𝑊)))
125124fveq2d 6656 . . . . . 6 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹f𝑐𝑊))))
126113, 122, 1253eqtr4d 2867 . . . . 5 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))))
12786, 93, 1, 123, 49, 112gsumsubmcl 19030 . . . . . 6 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) ∈ ℝ+)
128 fvres 6671 . . . . . 6 ((𝑀 Σg (𝐹f𝑐𝑊)) ∈ ℝ+ → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
129127, 128syl 17 . . . . 5 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
13065, 126, 1293eqtrd 2861 . . . 4 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
131 simprl 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
132131rpcnd 12421 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
133 simprr 772 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
134133rpcnd 12421 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
135132, 134mulcomd 10651 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
1361, 4, 2, 135caofcom 7426 . . . . . . . 8 (𝜑 → (𝑊f · 𝐹) = (𝐹f · 𝑊))
137136oveq2d 7156 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = (ℂfld Σg (𝐹f · 𝑊)))
1382feqmptd 6715 . . . . . . . . . . 11 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
1391, 5, 3, 31, 138offval2 7411 . . . . . . . . . 10 (𝜑 → (𝑊f · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
140139oveq2d 7156 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
1415, 3rpmulcld 12435 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
142141rpcnd 12421 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
1431, 142gsumfsum 20156 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
144140, 143eqtrd 2857 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
145 amgmwlem.2 . . . . . . . . 9 (𝜑𝐴 ≠ ∅)
1461, 145, 141fsumrpcl 15085 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
147144, 146eqeltrd 2914 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) ∈ ℝ+)
148137, 147eqeltrrd 2915 . . . . . 6 (𝜑 → (ℂfld Σg (𝐹f · 𝑊)) ∈ ℝ+)
149148relogcld 25212 . . . . 5 (𝜑 → (log‘(ℂfld Σg (𝐹f · 𝑊))) ∈ ℝ)
150 ringcmn 19325 . . . . . . 7 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
15171, 150mp1i 13 . . . . . 6 (𝜑 → ℂfld ∈ CMnd)
152 remulcl 10611 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
153152adantl 485 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
154 rpssre 12384 . . . . . . . 8 + ⊆ ℝ
155 fss 6508 . . . . . . . 8 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
1564, 154, 155sylancl 589 . . . . . . 7 (𝜑𝑊:𝐴⟶ℝ)
15721renegcld 11056 . . . . . . . 8 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℝ)
158157fmpttd 6861 . . . . . . 7 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))):𝐴⟶ℝ)
159153, 156, 158, 1, 1, 48off 7409 . . . . . 6 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))):𝐴⟶ℝ)
160 0red 10633 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
161159, 1, 160fdmfifsupp 8831 . . . . . 6 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) finSupp 0)
16273, 151, 1, 118, 159, 161gsumsubmcl 19030 . . . . 5 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ∈ ℝ)
163154a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ⊆ ℝ)
164 simpr 488 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
165164relogcld 25212 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
166165renegcld 11056 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
167166fmpttd 6861 . . . . . . . 8 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
168 simpl 486 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
169 ioorp 12803 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
170168, 169eleqtrrdi 2925 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
171 simpr 488 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
172171, 169eleqtrrdi 2925 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
173 iccssioo2 12798 . . . . . . . . . . 11 ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
174170, 172, 173syl2anc 587 . . . . . . . . . 10 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
175174, 169sseqtrdi 3992 . . . . . . . . 9 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
176175adantl 485 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
177 ioossico 12816 . . . . . . . . . 10 (0(,)+∞) ⊆ (0[,)+∞)
178169, 177eqsstrri 3977 . . . . . . . . 9 + ⊆ (0[,)+∞)
179 fss 6508 . . . . . . . . 9 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞))
1804, 178, 179sylancl 589 . . . . . . . 8 (𝜑𝑊:𝐴⟶(0[,)+∞))
181 0lt1 11151 . . . . . . . . 9 0 < 1
182 amgmwlem.5 . . . . . . . . 9 (𝜑 → (ℂfld Σg 𝑊) = 1)
183181, 182breqtrrid 5080 . . . . . . . 8 (𝜑 → 0 < (ℂfld Σg 𝑊))
184 logccv 25252 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
1851843adant1 1127 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
186 elioore 12756 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
1871863ad2ant3 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
188 simp21 1203 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
189188relogcld 25212 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
190187, 189remulcld 10660 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
191 1red 10631 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
192191, 186resubcld 11057 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
1931923ad2ant3 1132 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
194 simp22 1204 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
195194relogcld 25212 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
196193, 195remulcld 10660 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
197190, 196readdcld 10659 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
198 eliooord 12784 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
199198simpld 498 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < 𝑡)
200186, 199elrpd 12416 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
2012003ad2ant3 1132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
202201, 188rpmulcld 12435 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
203 0red 10633 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
204198simprd 499 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (0(,)1) → 𝑡 < 1)
205 1m0e1 11746 . . . . . . . . . . . . . . . . . . 19 (1 − 0) = 1
206204, 205breqtrrdi 5084 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
207186, 191, 203, 206ltsub13d 11235 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
208192, 207elrpd 12416 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
2092083ad2ant3 1132 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
210209, 194rpmulcld 12435 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
211 rpaddcl 12399 . . . . . . . . . . . . . 14 (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
212202, 210, 211syl2anc 587 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
213212relogcld 25212 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
214197, 213ltnegd 11207 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
215185, 214mpbid 235 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
216 eqidd 2823 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
217 fveq2 6652 . . . . . . . . . . . . 13 (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
218217adantl 485 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
219218negeqd 10869 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
220 negex 10873 . . . . . . . . . . . 12 -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
221220a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V)
222216, 219, 212, 221fvmptd 6757 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
223 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
224223negeqd 10869 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
225 eqid 2822 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
226 negex 10873 . . . . . . . . . . . . . . . 16 -(log‘𝑤) ∈ V
227224, 225, 226fvmpt3i 6755 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
228188, 227syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
229228oveq2d 7156 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
230187recnd 10658 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
231189recnd 10658 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
232230, 231mulneg2d 11083 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
233229, 232eqtrd 2857 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
234 fveq2 6652 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
235234negeqd 10869 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
236235, 225, 226fvmpt3i 6755 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
237194, 236syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
238237oveq2d 7156 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
239209rpcnd 12421 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
240195recnd 10658 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
241239, 240mulneg2d 11083 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
242238, 241eqtrd 2857 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
243233, 242oveq12d 7158 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
244190recnd 10658 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
245196recnd 10658 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
246244, 245negdid 10999 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
247243, 246eqtr4d 2860 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
248215, 222, 2473brtr4d 5074 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
249163, 167, 176, 248scvxcvx 25569 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ ℝ+𝑣 ∈ ℝ+𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
250163, 167, 176, 1, 180, 2, 183, 249jensen 25572 . . . . . . 7 (𝜑 → (((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊)) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊))))
251250simprd 499 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)))
252182oveq2d 7156 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊f · 𝐹)) / 1))
253252fveq2d 6656 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / 1)))
254147rpcnd 12421 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) ∈ ℂ)
255254div1d 11397 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊f · 𝐹)) / 1) = (ℂfld Σg (𝑊f · 𝐹)))
256255fveq2d 6656 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / 1)) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))))
257 fveq2 6652 . . . . . . . . . . 11 (𝑤 = (ℂfld Σg (𝑊f · 𝐹)) → (log‘𝑤) = (log‘(ℂfld Σg (𝑊f · 𝐹))))
258257negeqd 10869 . . . . . . . . . 10 (𝑤 = (ℂfld Σg (𝑊f · 𝐹)) → -(log‘𝑤) = -(log‘(ℂfld Σg (𝑊f · 𝐹))))
259258, 225, 226fvmpt3i 6755 . . . . . . . . 9 ((ℂfld Σg (𝑊f · 𝐹)) ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝑊f · 𝐹))))
260147, 259syl 17 . . . . . . . 8 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝑊f · 𝐹))))
261137fveq2d 6656 . . . . . . . . 9 (𝜑 → (log‘(ℂfld Σg (𝑊f · 𝐹))) = (log‘(ℂfld Σg (𝐹f · 𝑊))))
262261negeqd 10869 . . . . . . . 8 (𝜑 → -(log‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
263260, 262eqtrd 2857 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
264253, 256, 2633eqtrd 2861 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
265182oveq2d 7156 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1))
266 ringmnd 19298 . . . . . . . . . . 11 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
26771, 266ax-mp 5 . . . . . . . . . 10 fld ∈ Mnd
26872submid 17966 . . . . . . . . . 10 (ℂfld ∈ Mnd → ℂ ∈ (SubMnd‘ℂfld))
269267, 268mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (SubMnd‘ℂfld))
270 mulcl 10610 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
271270adantl 485 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
272 rpcn 12387 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
273272ssriv 3946 . . . . . . . . . . . 12 + ⊆ ℂ
274273a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ+ ⊆ ℂ)
2754, 274fssd 6509 . . . . . . . . . 10 (𝜑𝑊:𝐴⟶ℂ)
276165recnd 10658 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
277276negcld 10973 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
278277fmpttd 6861 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
279 fco 6512 . . . . . . . . . . 11 (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
280278, 2, 279syl2anc 587 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
281271, 275, 280, 1, 1, 48off 7409 . . . . . . . . 9 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
282281, 1, 160fdmfifsupp 8831 . . . . . . . . 9 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) finSupp 0)
28373, 151, 1, 269, 281, 282gsumsubmcl 19030 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) ∈ ℂ)
284283div1d 11397 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1) = (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))))
285 eqidd 2823 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
286 fveq2 6652 . . . . . . . . . . 11 (𝑤 = (𝐹𝑘) → (log‘𝑤) = (log‘(𝐹𝑘)))
287286negeqd 10869 . . . . . . . . . 10 (𝑤 = (𝐹𝑘) → -(log‘𝑤) = -(log‘(𝐹𝑘)))
2883, 138, 285, 287fmptco 6873 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
289288oveq2d 7156 . . . . . . . 8 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))))
290289oveq2d 7156 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
291265, 284, 2903eqtrd 2861 . . . . . 6 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
292251, 264, 2913brtr3d 5073 . . . . 5 (𝜑 → -(log‘(ℂfld Σg (𝐹f · 𝑊))) ≤ (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
293149, 162, 292lenegcon1d 11211 . . . 4 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))))
294130, 293eqbrtrrd 5066 . . 3 (𝜑 → (log‘(𝑀 Σg (𝐹f𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))))
295127relogcld 25212 . . . 4 (𝜑 → (log‘(𝑀 Σg (𝐹f𝑐𝑊))) ∈ ℝ)
296 efle 15462 . . . 4 (((log‘(𝑀 Σg (𝐹f𝑐𝑊))) ∈ ℝ ∧ (log‘(ℂfld Σg (𝐹f · 𝑊))) ∈ ℝ) → ((log‘(𝑀 Σg (𝐹f𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊))))))
297295, 149, 296syl2anc 587 . . 3 (𝜑 → ((log‘(𝑀 Σg (𝐹f𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊))))))
298294, 297mpbid 235 . 2 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))))
299127reeflogd 25213 . . 3 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) = (𝑀 Σg (𝐹f𝑐𝑊)))
300299eqcomd 2828 . 2 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) = (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))))
301148reeflogd 25213 . . 3 (𝜑 → (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))) = (ℂfld Σg (𝐹f · 𝑊)))
302301eqcomd 2828 . 2 (𝜑 → (ℂfld Σg (𝐹f · 𝑊)) = (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))))
303298, 300, 3023brtr4d 5074 1 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) ≤ (ℂfld Σg (𝐹f · 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 209  wa 399  w3a 1084   = wceq 1538  wcel 2114  wne 3011  Vcvv 3469  cdif 3905  wss 3908  c0 4265  {csn 4539   class class class wbr 5042  cmpt 5122  cres 5534  ccom 5536  wf 6330  1-1-ontowf1o 6333  cfv 6334  (class class class)co 7140  f cof 7392  Fincfn 8496  cc 10524  cr 10525  0cc0 10526  1c1 10527   + caddc 10529   · cmul 10531  +∞cpnf 10661   < clt 10664  cle 10665  cmin 10859  -cneg 10860   / cdiv 11286  +crp 12377  (,)cioo 12726  [,)cico 12728  [,]cicc 12729  Σcsu 15033  expce 15406  Basecbs 16474  s cress 16475  0gc0g 16704   Σg cgsu 16705  Mndcmnd 17902   MndHom cmhm 17945  SubMndcsubmnd 17946  SubGrpcsubg 18264   GrpHom cghm 18346   GrpIso cgim 18388  CMndccmn 18897  mulGrpcmgp 19230  Ringcrg 19288  CRingccrg 19289  DivRingcdr 19493  SubRingcsubrg 19522  fldccnfld 20089  fldcrefld 20291  logclog 25144  𝑐ccxp 25145
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2178  ax-ext 2794  ax-rep 5166  ax-sep 5179  ax-nul 5186  ax-pow 5243  ax-pr 5307  ax-un 7446  ax-inf2 9092  ax-cnex 10582  ax-resscn 10583  ax-1cn 10584  ax-icn 10585  ax-addcl 10586  ax-addrcl 10587  ax-mulcl 10588  ax-mulrcl 10589  ax-mulcom 10590  ax-addass 10591  ax-mulass 10592  ax-distr 10593  ax-i2m1 10594  ax-1ne0 10595  ax-1rid 10596  ax-rnegex 10597  ax-rrecex 10598  ax-cnre 10599  ax-pre-lttri 10600  ax-pre-lttrn 10601  ax-pre-ltadd 10602  ax-pre-mulgt0 10603  ax-pre-sup 10604  ax-addf 10605  ax-mulf 10606
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2622  df-eu 2653  df-clab 2801  df-cleq 2815  df-clel 2894  df-nfc 2962  df-ne 3012  df-nel 3116  df-ral 3135  df-rex 3136  df-reu 3137  df-rmo 3138  df-rab 3139  df-v 3471  df-sbc 3748  df-csb 3856  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-pss 3927  df-nul 4266  df-if 4440  df-pw 4513  df-sn 4540  df-pr 4542  df-tp 4544  df-op 4546  df-uni 4814  df-int 4852  df-iun 4896  df-iin 4897  df-br 5043  df-opab 5105  df-mpt 5123  df-tr 5149  df-id 5437  df-eprel 5442  df-po 5451  df-so 5452  df-fr 5491  df-se 5492  df-we 5493  df-xp 5538  df-rel 5539  df-cnv 5540  df-co 5541  df-dm 5542  df-rn 5543  df-res 5544  df-ima 5545  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6293  df-fun 6336  df-fn 6337  df-f 6338  df-f1 6339  df-fo 6340  df-f1o 6341  df-fv 6342  df-isom 6343  df-riota 7098  df-ov 7143  df-oprab 7144  df-mpo 7145  df-of 7394  df-om 7566  df-1st 7675  df-2nd 7676  df-supp 7818  df-tpos 7879  df-wrecs 7934  df-recs 7995  df-rdg 8033  df-1o 8089  df-2o 8090  df-oadd 8093  df-er 8276  df-map 8395  df-pm 8396  df-ixp 8449  df-en 8497  df-dom 8498  df-sdom 8499  df-fin 8500  df-fsupp 8822  df-fi 8863  df-sup 8894  df-inf 8895  df-oi 8962  df-card 9356  df-pnf 10666  df-mnf 10667  df-xr 10668  df-ltxr 10669  df-le 10670  df-sub 10861  df-neg 10862  df-div 11287  df-nn 11626  df-2 11688  df-3 11689  df-4 11690  df-5 11691  df-6 11692  df-7 11693  df-8 11694  df-9 11695  df-n0 11886  df-z 11970  df-dec 12087  df-uz 12232  df-q 12337  df-rp 12378  df-xneg 12495  df-xadd 12496  df-xmul 12497  df-ioo 12730  df-ioc 12731  df-ico 12732  df-icc 12733  df-fz 12886  df-fzo 13029  df-fl 13157  df-mod 13233  df-seq 13365  df-exp 13426  df-fac 13630  df-bc 13659  df-hash 13687  df-shft 14417  df-cj 14449  df-re 14450  df-im 14451  df-sqrt 14585  df-abs 14586  df-limsup 14819  df-clim 14836  df-rlim 14837  df-sum 15034  df-ef 15412  df-sin 15414  df-cos 15415  df-pi 15417  df-struct 16476  df-ndx 16477  df-slot 16478  df-base 16480  df-sets 16481  df-ress 16482  df-plusg 16569  df-mulr 16570  df-starv 16571  df-sca 16572  df-vsca 16573  df-ip 16574  df-tset 16575  df-ple 16576  df-ds 16578  df-unif 16579  df-hom 16580  df-cco 16581  df-rest 16687  df-topn 16688  df-0g 16706  df-gsum 16707  df-topgen 16708  df-pt 16709  df-prds 16712  df-xrs 16766  df-qtop 16771  df-imas 16772  df-xps 16774  df-mre 16848  df-mrc 16849  df-acs 16851  df-mgm 17843  df-sgrp 17892  df-mnd 17903  df-mhm 17947  df-submnd 17948  df-grp 18097  df-minusg 18098  df-mulg 18216  df-subg 18267  df-ghm 18347  df-gim 18390  df-cntz 18438  df-cmn 18899  df-abl 18900  df-mgp 19231  df-ur 19243  df-ring 19290  df-cring 19291  df-oppr 19367  df-dvdsr 19385  df-unit 19386  df-invr 19416  df-dvr 19427  df-drng 19495  df-subrg 19524  df-psmet 20081  df-xmet 20082  df-met 20083  df-bl 20084  df-mopn 20085  df-fbas 20086  df-fg 20087  df-cnfld 20090  df-refld 20292  df-top 21497  df-topon 21514  df-topsp 21536  df-bases 21549  df-cld 21622  df-ntr 21623  df-cls 21624  df-nei 21701  df-lp 21739  df-perf 21740  df-cn 21830  df-cnp 21831  df-haus 21918  df-cmp 21990  df-tx 22165  df-hmeo 22358  df-fil 22449  df-fm 22541  df-flim 22542  df-flf 22543  df-xms 22925  df-ms 22926  df-tms 22927  df-cncf 23481  df-limc 24467  df-dv 24468  df-log 25146  df-cxp 25147
This theorem is referenced by:  amgmlemALT  45270  amgmw2d  45271
  Copyright terms: Public domain W3C validator