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 46865
Description: Weighted version of amgmlem 26245. (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 (𝜑𝐹:𝐴⟶ℝ+)
32ffvelcdmda 7017 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝐹𝑘) ∈ ℝ+)
4 amgmwlem.4 . . . . . . . . . . . . 13 (𝜑𝑊:𝐴⟶ℝ+)
54ffvelcdmda 7017 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ+)
65rpred 12873 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℝ)
73, 6rpcxpcld 25993 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝐹𝑘)↑𝑐(𝑊𝑘)) ∈ ℝ+)
87relogcld 25884 . . . . . . . . 9 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
98recnd 11104 . . . . . . . 8 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
101, 9gsumfsum 20771 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
119negnegd 11424 . . . . . . . 8 ((𝜑𝑘𝐴) → --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
1211sumeq2dv 15514 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
138renegcld 11503 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℝ)
1413recnd 11104 . . . . . . . . 9 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) ∈ ℂ)
151, 14fsumneg 15598 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
163, 6logcxpd 25994 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = ((𝑊𝑘) · (log‘(𝐹𝑘))))
1716negeqd 11316 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
1817sumeq2dv 15514 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
1918negeqd 11316 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))))
205rpcnd 12875 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) ∈ ℂ)
213relogcld 25884 . . . . . . . . . . . . 13 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℝ)
2221recnd 11104 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (log‘(𝐹𝑘)) ∈ ℂ)
2320, 22mulneg2d 11530 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) = -((𝑊𝑘) · (log‘(𝐹𝑘))))
2423eqcomd 2742 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -((𝑊𝑘) · (log‘(𝐹𝑘))) = ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2524sumeq2dv 15514 . . . . . . . . 9 (𝜑 → Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2625negeqd 11316 . . . . . . . 8 (𝜑 → -Σ𝑘𝐴 -((𝑊𝑘) · (log‘(𝐹𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2715, 19, 263eqtrd 2780 . . . . . . 7 (𝜑 → Σ𝑘𝐴 --(log‘((𝐹𝑘)↑𝑐(𝑊𝑘))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
2810, 12, 273eqtr2rd 2783 . . . . . 6 (𝜑 → -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
29 negex 11320 . . . . . . . . . . 11 -(log‘(𝐹𝑘)) ∈ V
3029a1i 11 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ V)
314feqmptd 6893 . . . . . . . . . 10 (𝜑𝑊 = (𝑘𝐴 ↦ (𝑊𝑘)))
32 eqidd 2737 . . . . . . . . . 10 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
331, 5, 30, 31, 32offval2 7615 . . . . . . . . 9 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) = (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘)))))
3433oveq2d 7353 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))))
3522negcld 11420 . . . . . . . . . 10 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℂ)
3620, 35mulcld 11096 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((𝑊𝑘) · -(log‘(𝐹𝑘))) ∈ ℂ)
371, 36gsumfsum 20771 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
3834, 37eqtrd 2776 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
3938negeqd 11316 . . . . . 6 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = -Σ𝑘𝐴 ((𝑊𝑘) · -(log‘(𝐹𝑘))))
40 relogf1o 25828 . . . . . . . . . 10 (log ↾ ℝ+):ℝ+1-1-onto→ℝ
41 f1of 6767 . . . . . . . . . 10 ((log ↾ ℝ+):ℝ+1-1-onto→ℝ → (log ↾ ℝ+):ℝ+⟶ℝ)
4240, 41ax-mp 5 . . . . . . . . 9 (log ↾ ℝ+):ℝ+⟶ℝ
43 rpre 12839 . . . . . . . . . . . . 13 (𝑦 ∈ ℝ+𝑦 ∈ ℝ)
4443anim2i 617 . . . . . . . . . . . 12 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ+) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
4544adantl 482 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 ∈ ℝ+𝑦 ∈ ℝ))
46 rpcxpcl 25937 . . . . . . . . . . 11 ((𝑥 ∈ ℝ+𝑦 ∈ ℝ) → (𝑥𝑐𝑦) ∈ ℝ+)
4745, 46syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥𝑐𝑦) ∈ ℝ+)
48 inidm 4165 . . . . . . . . . 10 (𝐴𝐴) = 𝐴
4947, 2, 4, 1, 1, 48off 7613 . . . . . . . . 9 (𝜑 → (𝐹f𝑐𝑊):𝐴⟶ℝ+)
50 fcompt 7061 . . . . . . . . 9 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹f𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))))
5142, 49, 50sylancr 587 . . . . . . . 8 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))))
5249ffvelcdmda 7017 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹f𝑐𝑊)‘𝑘) ∈ ℝ+)
53 fvres 6844 . . . . . . . . . . 11 (((𝐹f𝑐𝑊)‘𝑘) ∈ ℝ+ → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹f𝑐𝑊)‘𝑘)))
5452, 53syl 17 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹f𝑐𝑊)‘𝑘)))
552ffnd 6652 . . . . . . . . . . . 12 (𝜑𝐹 Fn 𝐴)
564ffnd 6652 . . . . . . . . . . . 12 (𝜑𝑊 Fn 𝐴)
57 eqidd 2737 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝐹𝑘) = (𝐹𝑘))
58 eqidd 2737 . . . . . . . . . . . 12 ((𝜑𝑘𝐴) → (𝑊𝑘) = (𝑊𝑘))
5955, 56, 1, 1, 48, 57, 58ofval 7606 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝐹f𝑐𝑊)‘𝑘) = ((𝐹𝑘)↑𝑐(𝑊𝑘)))
6059fveq2d 6829 . . . . . . . . . 10 ((𝜑𝑘𝐴) → (log‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
6154, 60eqtrd 2776 . . . . . . . . 9 ((𝜑𝑘𝐴) → ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘)) = (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))
6261mpteq2dva 5192 . . . . . . . 8 (𝜑 → (𝑘𝐴 ↦ ((log ↾ ℝ+)‘((𝐹f𝑐𝑊)‘𝑘))) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
6351, 62eqtrd 2776 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)) = (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘)))))
6463oveq2d 7353 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = (ℂfld Σg (𝑘𝐴 ↦ (log‘((𝐹𝑘)↑𝑐(𝑊𝑘))))))
6528, 39, 643eqtr4d 2786 . . . . 5 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))))
66 amgmwlem.0 . . . . . . . . . . . . 13 𝑀 = (mulGrp‘ℂfld)
6766oveq1i 7347 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = ((mulGrp‘ℂfld) ↾s (ℂ ∖ {0}))
6867rpmsubg 20768 . . . . . . . . . . 11 + ∈ (SubGrp‘(𝑀s (ℂ ∖ {0})))
69 subgsubm 18873 . . . . . . . . . . 11 (ℝ+ ∈ (SubGrp‘(𝑀s (ℂ ∖ {0}))) → ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))))
7068, 69ax-mp 5 . . . . . . . . . 10 + ∈ (SubMnd‘(𝑀s (ℂ ∖ {0})))
71 cnring 20726 . . . . . . . . . . 11 fld ∈ Ring
72 cnfldbas 20707 . . . . . . . . . . . . 13 ℂ = (Base‘ℂfld)
73 cnfld0 20728 . . . . . . . . . . . . 13 0 = (0g‘ℂfld)
74 cndrng 20733 . . . . . . . . . . . . 13 fld ∈ DivRing
7572, 73, 74drngui 20099 . . . . . . . . . . . 12 (ℂ ∖ {0}) = (Unit‘ℂfld)
7675, 66unitsubm 20007 . . . . . . . . . . 11 (ℂfld ∈ Ring → (ℂ ∖ {0}) ∈ (SubMnd‘𝑀))
77 eqid 2736 . . . . . . . . . . . 12 (𝑀s (ℂ ∖ {0})) = (𝑀s (ℂ ∖ {0}))
7877subsubm 18552 . . . . . . . . . . 11 ((ℂ ∖ {0}) ∈ (SubMnd‘𝑀) → (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))))
7971, 76, 78mp2b 10 . . . . . . . . . 10 (ℝ+ ∈ (SubMnd‘(𝑀s (ℂ ∖ {0}))) ↔ (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0})))
8070, 79mpbi 229 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) ∧ ℝ+ ⊆ (ℂ ∖ {0}))
8180simpli 484 . . . . . . . 8 + ∈ (SubMnd‘𝑀)
82 eqid 2736 . . . . . . . . 9 (𝑀s+) = (𝑀s+)
8382submbas 18550 . . . . . . . 8 (ℝ+ ∈ (SubMnd‘𝑀) → ℝ+ = (Base‘(𝑀s+)))
8481, 83ax-mp 5 . . . . . . 7 + = (Base‘(𝑀s+))
85 cnfld1 20729 . . . . . . . . 9 1 = (1r‘ℂfld)
8666, 85ringidval 19834 . . . . . . . 8 1 = (0g𝑀)
87 eqid 2736 . . . . . . . . . 10 (0g𝑀) = (0g𝑀)
8882, 87subm0 18551 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (0g𝑀) = (0g‘(𝑀s+)))
8981, 88ax-mp 5 . . . . . . . 8 (0g𝑀) = (0g‘(𝑀s+))
9086, 89eqtri 2764 . . . . . . 7 1 = (0g‘(𝑀s+))
91 cncrng 20725 . . . . . . . . 9 fld ∈ CRing
9266crngmgp 19886 . . . . . . . . 9 (ℂfld ∈ CRing → 𝑀 ∈ CMnd)
9391, 92mp1i 13 . . . . . . . 8 (𝜑𝑀 ∈ CMnd)
9482submmnd 18549 . . . . . . . . 9 (ℝ+ ∈ (SubMnd‘𝑀) → (𝑀s+) ∈ Mnd)
9581, 94mp1i 13 . . . . . . . 8 (𝜑 → (𝑀s+) ∈ Mnd)
9682subcmn 19533 . . . . . . . 8 ((𝑀 ∈ CMnd ∧ (𝑀s+) ∈ Mnd) → (𝑀s+) ∈ CMnd)
9793, 95, 96syl2anc 584 . . . . . . 7 (𝜑 → (𝑀s+) ∈ CMnd)
98 resubdrg 20919 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) ∧ ℝfld ∈ DivRing)
9998simpli 484 . . . . . . . . 9 ℝ ∈ (SubRing‘ℂfld)
100 df-refld 20916 . . . . . . . . . 10 fld = (ℂflds ℝ)
101100subrgring 20132 . . . . . . . . 9 (ℝ ∈ (SubRing‘ℂfld) → ℝfld ∈ Ring)
10299, 101ax-mp 5 . . . . . . . 8 fld ∈ Ring
103 ringmnd 19888 . . . . . . . 8 (ℝfld ∈ Ring → ℝfld ∈ Mnd)
104102, 103mp1i 13 . . . . . . 7 (𝜑 → ℝfld ∈ Mnd)
10566oveq1i 7347 . . . . . . . . . 10 (𝑀s+) = ((mulGrp‘ℂfld) ↾s+)
106105reloggim 25860 . . . . . . . . 9 (log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld)
107 gimghm 18976 . . . . . . . . 9 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpIso ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld))
108106, 107ax-mp 5 . . . . . . . 8 (log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld)
109 ghmmhm 18940 . . . . . . . 8 ((log ↾ ℝ+) ∈ ((𝑀s+) GrpHom ℝfld) → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
110108, 109mp1i 13 . . . . . . 7 (𝜑 → (log ↾ ℝ+) ∈ ((𝑀s+) MndHom ℝfld))
111 1red 11077 . . . . . . . 8 (𝜑 → 1 ∈ ℝ)
11249, 1, 111fdmfifsupp 9236 . . . . . . 7 (𝜑 → (𝐹f𝑐𝑊) finSupp 1)
11384, 90, 97, 104, 1, 110, 49, 112gsummhm 19634 . . . . . 6 (𝜑 → (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹f𝑐𝑊))))
114 subrgsubg 20135 . . . . . . . . . 10 (ℝ ∈ (SubRing‘ℂfld) → ℝ ∈ (SubGrp‘ℂfld))
11599, 114ax-mp 5 . . . . . . . . 9 ℝ ∈ (SubGrp‘ℂfld)
116 subgsubm 18873 . . . . . . . . 9 (ℝ ∈ (SubGrp‘ℂfld) → ℝ ∈ (SubMnd‘ℂfld))
117115, 116ax-mp 5 . . . . . . . 8 ℝ ∈ (SubMnd‘ℂfld)
118117a1i 11 . . . . . . 7 (𝜑 → ℝ ∈ (SubMnd‘ℂfld))
11940, 41mp1i 13 . . . . . . . 8 (𝜑 → (log ↾ ℝ+):ℝ+⟶ℝ)
120 fco 6675 . . . . . . . 8 (((log ↾ ℝ+):ℝ+⟶ℝ ∧ (𝐹f𝑐𝑊):𝐴⟶ℝ+) → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)):𝐴⟶ℝ)
121119, 49, 120syl2anc 584 . . . . . . 7 (𝜑 → ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊)):𝐴⟶ℝ)
1221, 118, 121, 100gsumsubm 18570 . . . . . 6 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = (ℝfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))))
12381a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ∈ (SubMnd‘𝑀))
1241, 123, 49, 82gsumsubm 18570 . . . . . . 7 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) = ((𝑀s+) Σg (𝐹f𝑐𝑊)))
125124fveq2d 6829 . . . . . 6 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘((𝑀s+) Σg (𝐹f𝑐𝑊))))
126113, 122, 1253eqtr4d 2786 . . . . 5 (𝜑 → (ℂfld Σg ((log ↾ ℝ+) ∘ (𝐹f𝑐𝑊))) = ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))))
12786, 93, 1, 123, 49, 112gsumsubmcl 19615 . . . . . 6 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) ∈ ℝ+)
128 fvres 6844 . . . . . 6 ((𝑀 Σg (𝐹f𝑐𝑊)) ∈ ℝ+ → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
129127, 128syl 17 . . . . 5 (𝜑 → ((log ↾ ℝ+)‘(𝑀 Σg (𝐹f𝑐𝑊))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
13065, 126, 1293eqtrd 2780 . . . 4 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) = (log‘(𝑀 Σg (𝐹f𝑐𝑊))))
131 simprl 768 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℝ+)
132131rpcnd 12875 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑥 ∈ ℂ)
133 simprr 770 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
134133rpcnd 12875 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → 𝑦 ∈ ℂ)
135132, 134mulcomd 11097 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+)) → (𝑥 · 𝑦) = (𝑦 · 𝑥))
1361, 4, 2, 135caofcom 7630 . . . . . . . 8 (𝜑 → (𝑊f · 𝐹) = (𝐹f · 𝑊))
137136oveq2d 7353 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = (ℂfld Σg (𝐹f · 𝑊)))
1382feqmptd 6893 . . . . . . . . . . 11 (𝜑𝐹 = (𝑘𝐴 ↦ (𝐹𝑘)))
1391, 5, 3, 31, 138offval2 7615 . . . . . . . . . 10 (𝜑 → (𝑊f · 𝐹) = (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘))))
140139oveq2d 7353 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))))
1415, 3rpmulcld 12889 . . . . . . . . . . 11 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
142141rpcnd 12875 . . . . . . . . . 10 ((𝜑𝑘𝐴) → ((𝑊𝑘) · (𝐹𝑘)) ∈ ℂ)
1431, 142gsumfsum 20771 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑘𝐴 ↦ ((𝑊𝑘) · (𝐹𝑘)))) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
144140, 143eqtrd 2776 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) = Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)))
145 amgmwlem.2 . . . . . . . . 9 (𝜑𝐴 ≠ ∅)
1461, 145, 141fsumrpcl 15548 . . . . . . . 8 (𝜑 → Σ𝑘𝐴 ((𝑊𝑘) · (𝐹𝑘)) ∈ ℝ+)
147144, 146eqeltrd 2837 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) ∈ ℝ+)
148137, 147eqeltrrd 2838 . . . . . 6 (𝜑 → (ℂfld Σg (𝐹f · 𝑊)) ∈ ℝ+)
149148relogcld 25884 . . . . 5 (𝜑 → (log‘(ℂfld Σg (𝐹f · 𝑊))) ∈ ℝ)
150 ringcmn 19915 . . . . . . 7 (ℂfld ∈ Ring → ℂfld ∈ CMnd)
15171, 150mp1i 13 . . . . . 6 (𝜑 → ℂfld ∈ CMnd)
152 remulcl 11057 . . . . . . . 8 ((𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ) → (𝑥 · 𝑦) ∈ ℝ)
153152adantl 482 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ)) → (𝑥 · 𝑦) ∈ ℝ)
154 rpssre 12838 . . . . . . . 8 + ⊆ ℝ
155 fss 6668 . . . . . . . 8 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ ℝ) → 𝑊:𝐴⟶ℝ)
1564, 154, 155sylancl 586 . . . . . . 7 (𝜑𝑊:𝐴⟶ℝ)
15721renegcld 11503 . . . . . . . 8 ((𝜑𝑘𝐴) → -(log‘(𝐹𝑘)) ∈ ℝ)
158157fmpttd 7045 . . . . . . 7 (𝜑 → (𝑘𝐴 ↦ -(log‘(𝐹𝑘))):𝐴⟶ℝ)
159153, 156, 158, 1, 1, 48off 7613 . . . . . 6 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))):𝐴⟶ℝ)
160 0red 11079 . . . . . . 7 (𝜑 → 0 ∈ ℝ)
161159, 1, 160fdmfifsupp 9236 . . . . . 6 (𝜑 → (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))) finSupp 0)
16273, 151, 1, 118, 159, 161gsumsubmcl 19615 . . . . 5 (𝜑 → (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ∈ ℝ)
163154a1i 11 . . . . . . . 8 (𝜑 → ℝ+ ⊆ ℝ)
164 simpr 485 . . . . . . . . . . 11 ((𝜑𝑤 ∈ ℝ+) → 𝑤 ∈ ℝ+)
165164relogcld 25884 . . . . . . . . . 10 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℝ)
166165renegcld 11503 . . . . . . . . 9 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℝ)
167166fmpttd 7045 . . . . . . . 8 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℝ)
168 simpl 483 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ ℝ+)
169 ioorp 13258 . . . . . . . . . . . 12 (0(,)+∞) = ℝ+
170168, 169eleqtrrdi 2848 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑎 ∈ (0(,)+∞))
171 simpr 485 . . . . . . . . . . . 12 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ ℝ+)
172171, 169eleqtrrdi 2848 . . . . . . . . . . 11 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → 𝑏 ∈ (0(,)+∞))
173 iccssioo2 13253 . . . . . . . . . . 11 ((𝑎 ∈ (0(,)+∞) ∧ 𝑏 ∈ (0(,)+∞)) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
174170, 172, 173syl2anc 584 . . . . . . . . . 10 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ (0(,)+∞))
175174, 169sseqtrdi 3982 . . . . . . . . 9 ((𝑎 ∈ ℝ+𝑏 ∈ ℝ+) → (𝑎[,]𝑏) ⊆ ℝ+)
176175adantl 482 . . . . . . . 8 ((𝜑 ∧ (𝑎 ∈ ℝ+𝑏 ∈ ℝ+)) → (𝑎[,]𝑏) ⊆ ℝ+)
177 ioossico 13271 . . . . . . . . . 10 (0(,)+∞) ⊆ (0[,)+∞)
178169, 177eqsstrri 3967 . . . . . . . . 9 + ⊆ (0[,)+∞)
179 fss 6668 . . . . . . . . 9 ((𝑊:𝐴⟶ℝ+ ∧ ℝ+ ⊆ (0[,)+∞)) → 𝑊:𝐴⟶(0[,)+∞))
1804, 178, 179sylancl 586 . . . . . . . 8 (𝜑𝑊:𝐴⟶(0[,)+∞))
181 0lt1 11598 . . . . . . . . 9 0 < 1
182 amgmwlem.5 . . . . . . . . 9 (𝜑 → (ℂfld Σg 𝑊) = 1)
183181, 182breqtrrid 5130 . . . . . . . 8 (𝜑 → 0 < (ℂfld Σg 𝑊))
184 logccv 25924 . . . . . . . . . . . 12 (((𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
1851843adant1 1129 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
186 elioore 13210 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ)
1871863ad2ant3 1134 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ)
188 simp21 1205 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑥 ∈ ℝ+)
189188relogcld 25884 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℝ)
190187, 189remulcld 11106 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℝ)
191 1red 11077 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 1 ∈ ℝ)
192191, 186resubcld 11504 . . . . . . . . . . . . . . 15 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ)
1931923ad2ant3 1134 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ)
194 simp22 1206 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑦 ∈ ℝ+)
195194relogcld 25884 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℝ)
196193, 195remulcld 11106 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℝ)
197190, 196readdcld 11105 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) ∈ ℝ)
198 eliooord 13239 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → (0 < 𝑡𝑡 < 1))
199198simpld 495 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < 𝑡)
200186, 199elrpd 12870 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → 𝑡 ∈ ℝ+)
2012003ad2ant3 1134 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℝ+)
202201, 188rpmulcld 12889 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · 𝑥) ∈ ℝ+)
203 0red 11079 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 0 ∈ ℝ)
204198simprd 496 . . . . . . . . . . . . . . . . . . 19 (𝑡 ∈ (0(,)1) → 𝑡 < 1)
205 1m0e1 12195 . . . . . . . . . . . . . . . . . . 19 (1 − 0) = 1
206204, 205breqtrrdi 5134 . . . . . . . . . . . . . . . . . 18 (𝑡 ∈ (0(,)1) → 𝑡 < (1 − 0))
207186, 191, 203, 206ltsub13d 11682 . . . . . . . . . . . . . . . . 17 (𝑡 ∈ (0(,)1) → 0 < (1 − 𝑡))
208192, 207elrpd 12870 . . . . . . . . . . . . . . . 16 (𝑡 ∈ (0(,)1) → (1 − 𝑡) ∈ ℝ+)
2092083ad2ant3 1134 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℝ+)
210209, 194rpmulcld 12889 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · 𝑦) ∈ ℝ+)
211 rpaddcl 12853 . . . . . . . . . . . . . 14 (((𝑡 · 𝑥) ∈ ℝ+ ∧ ((1 − 𝑡) · 𝑦) ∈ ℝ+) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
212202, 210, 211syl2anc 584 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ ℝ+)
213212relogcld 25884 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ ℝ)
214197, 213ltnegd 11654 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) < (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ↔ -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦)))))
215185, 214mpbid 231 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
216 eqidd 2737 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
217 fveq2 6825 . . . . . . . . . . . . 13 (𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
218217adantl 482 . . . . . . . . . . . 12 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → (log‘𝑤) = (log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
219218negeqd 11316 . . . . . . . . . . 11 (((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) ∧ 𝑤 = ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) → -(log‘𝑤) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
220 negex 11320 . . . . . . . . . . . 12 -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V
221220a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) ∈ V)
222216, 219, 212, 221fvmptd 6938 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) = -(log‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))))
223 fveq2 6825 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑥 → (log‘𝑤) = (log‘𝑥))
224223negeqd 11316 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑥 → -(log‘𝑤) = -(log‘𝑥))
225 eqid 2736 . . . . . . . . . . . . . . . 16 (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤))
226 negex 11320 . . . . . . . . . . . . . . . 16 -(log‘𝑤) ∈ V
227224, 225, 226fvmpt3i 6936 . . . . . . . . . . . . . . 15 (𝑥 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
228188, 227syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥) = -(log‘𝑥))
229228oveq2d 7353 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = (𝑡 · -(log‘𝑥)))
230187recnd 11104 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → 𝑡 ∈ ℂ)
231189recnd 11104 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑥) ∈ ℂ)
232230, 231mulneg2d 11530 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · -(log‘𝑥)) = -(𝑡 · (log‘𝑥)))
233229, 232eqtrd 2776 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) = -(𝑡 · (log‘𝑥)))
234 fveq2 6825 . . . . . . . . . . . . . . . . 17 (𝑤 = 𝑦 → (log‘𝑤) = (log‘𝑦))
235234negeqd 11316 . . . . . . . . . . . . . . . 16 (𝑤 = 𝑦 → -(log‘𝑤) = -(log‘𝑦))
236235, 225, 226fvmpt3i 6936 . . . . . . . . . . . . . . 15 (𝑦 ∈ ℝ+ → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
237194, 236syl 17 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦) = -(log‘𝑦))
238237oveq2d 7353 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = ((1 − 𝑡) · -(log‘𝑦)))
239209rpcnd 12875 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (1 − 𝑡) ∈ ℂ)
240195recnd 11104 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (log‘𝑦) ∈ ℂ)
241239, 240mulneg2d 11530 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · -(log‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
242238, 241eqtrd 2776 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦)) = -((1 − 𝑡) · (log‘𝑦)))
243233, 242oveq12d 7355 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
244190recnd 11104 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → (𝑡 · (log‘𝑥)) ∈ ℂ)
245196recnd 11104 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((1 − 𝑡) · (log‘𝑦)) ∈ ℂ)
246244, 245negdid 11446 . . . . . . . . . . 11 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))) = (-(𝑡 · (log‘𝑥)) + -((1 − 𝑡) · (log‘𝑦))))
247243, 246eqtr4d 2779 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))) = -((𝑡 · (log‘𝑥)) + ((1 − 𝑡) · (log‘𝑦))))
248215, 222, 2473brtr4d 5124 . . . . . . . . 9 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑦 ∈ ℝ+𝑥 < 𝑦) ∧ 𝑡 ∈ (0(,)1)) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦))) < ((𝑡 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑥)) + ((1 − 𝑡) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑦))))
249163, 167, 176, 248scvxcvx 26241 . . . . . . . 8 ((𝜑 ∧ (𝑢 ∈ ℝ+𝑣 ∈ ℝ+𝑠 ∈ (0[,]1))) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((𝑠 · 𝑢) + ((1 − 𝑠) · 𝑣))) ≤ ((𝑠 · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑢)) + ((1 − 𝑠) · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘𝑣))))
250163, 167, 176, 1, 180, 2, 183, 249jensen 26244 . . . . . . 7 (𝜑 → (((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊)) ∈ ℝ+ ∧ ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊))))
251250simprd 496 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) ≤ ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)))
252182oveq2d 7353 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊f · 𝐹)) / 1))
253252fveq2d 6829 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / 1)))
254147rpcnd 12875 . . . . . . . . 9 (𝜑 → (ℂfld Σg (𝑊f · 𝐹)) ∈ ℂ)
255254div1d 11844 . . . . . . . 8 (𝜑 → ((ℂfld Σg (𝑊f · 𝐹)) / 1) = (ℂfld Σg (𝑊f · 𝐹)))
256255fveq2d 6829 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / 1)) = ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))))
257 fveq2 6825 . . . . . . . . . . 11 (𝑤 = (ℂfld Σg (𝑊f · 𝐹)) → (log‘𝑤) = (log‘(ℂfld Σg (𝑊f · 𝐹))))
258257negeqd 11316 . . . . . . . . . 10 (𝑤 = (ℂfld Σg (𝑊f · 𝐹)) → -(log‘𝑤) = -(log‘(ℂfld Σg (𝑊f · 𝐹))))
259258, 225, 226fvmpt3i 6936 . . . . . . . . 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 6829 . . . . . . . . 9 (𝜑 → (log‘(ℂfld Σg (𝑊f · 𝐹))) = (log‘(ℂfld Σg (𝐹f · 𝑊))))
262261negeqd 11316 . . . . . . . 8 (𝜑 → -(log‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
263260, 262eqtrd 2776 . . . . . . 7 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘(ℂfld Σg (𝑊f · 𝐹))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
264253, 256, 2633eqtrd 2780 . . . . . 6 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤))‘((ℂfld Σg (𝑊f · 𝐹)) / (ℂfld Σg 𝑊))) = -(log‘(ℂfld Σg (𝐹f · 𝑊))))
265182oveq2d 7353 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1))
266 ringmnd 19888 . . . . . . . . . . 11 (ℂfld ∈ Ring → ℂfld ∈ Mnd)
26771, 266ax-mp 5 . . . . . . . . . 10 fld ∈ Mnd
26872submid 18546 . . . . . . . . . 10 (ℂfld ∈ Mnd → ℂ ∈ (SubMnd‘ℂfld))
269267, 268mp1i 13 . . . . . . . . 9 (𝜑 → ℂ ∈ (SubMnd‘ℂfld))
270 mulcl 11056 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ) → (𝑥 · 𝑦) ∈ ℂ)
271270adantl 482 . . . . . . . . . 10 ((𝜑 ∧ (𝑥 ∈ ℂ ∧ 𝑦 ∈ ℂ)) → (𝑥 · 𝑦) ∈ ℂ)
272 rpcn 12841 . . . . . . . . . . . . 13 (𝑥 ∈ ℝ+𝑥 ∈ ℂ)
273272ssriv 3936 . . . . . . . . . . . 12 + ⊆ ℂ
274273a1i 11 . . . . . . . . . . 11 (𝜑 → ℝ+ ⊆ ℂ)
2754, 274fssd 6669 . . . . . . . . . 10 (𝜑𝑊:𝐴⟶ℂ)
276165recnd 11104 . . . . . . . . . . . . 13 ((𝜑𝑤 ∈ ℝ+) → (log‘𝑤) ∈ ℂ)
277276negcld 11420 . . . . . . . . . . . 12 ((𝜑𝑤 ∈ ℝ+) → -(log‘𝑤) ∈ ℂ)
278277fmpttd 7045 . . . . . . . . . . 11 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ)
279 fco 6675 . . . . . . . . . . 11 (((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)):ℝ+⟶ℂ ∧ 𝐹:𝐴⟶ℝ+) → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
280278, 2, 279syl2anc 584 . . . . . . . . . 10 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹):𝐴⟶ℂ)
281271, 275, 280, 1, 1, 48off 7613 . . . . . . . . 9 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)):𝐴⟶ℂ)
282281, 1, 160fdmfifsupp 9236 . . . . . . . . 9 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) finSupp 0)
28373, 151, 1, 269, 281, 282gsumsubmcl 19615 . . . . . . . 8 (𝜑 → (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) ∈ ℂ)
284283div1d 11844 . . . . . . 7 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / 1) = (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))))
285 eqidd 2737 . . . . . . . . . 10 (𝜑 → (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) = (𝑤 ∈ ℝ+ ↦ -(log‘𝑤)))
286 fveq2 6825 . . . . . . . . . . 11 (𝑤 = (𝐹𝑘) → (log‘𝑤) = (log‘(𝐹𝑘)))
287286negeqd 11316 . . . . . . . . . 10 (𝑤 = (𝐹𝑘) → -(log‘𝑤) = -(log‘(𝐹𝑘)))
2883, 138, 285, 287fmptco 7057 . . . . . . . . 9 (𝜑 → ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹) = (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))
289288oveq2d 7353 . . . . . . . 8 (𝜑 → (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹)) = (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘)))))
290289oveq2d 7353 . . . . . . 7 (𝜑 → (ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) = (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
291265, 284, 2903eqtrd 2780 . . . . . 6 (𝜑 → ((ℂfld Σg (𝑊f · ((𝑤 ∈ ℝ+ ↦ -(log‘𝑤)) ∘ 𝐹))) / (ℂfld Σg 𝑊)) = (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
292251, 264, 2913brtr3d 5123 . . . . 5 (𝜑 → -(log‘(ℂfld Σg (𝐹f · 𝑊))) ≤ (ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))))
293149, 162, 292lenegcon1d 11658 . . . 4 (𝜑 → -(ℂfld Σg (𝑊f · (𝑘𝐴 ↦ -(log‘(𝐹𝑘))))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))))
294130, 293eqbrtrrd 5116 . . 3 (𝜑 → (log‘(𝑀 Σg (𝐹f𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))))
295127relogcld 25884 . . . 4 (𝜑 → (log‘(𝑀 Σg (𝐹f𝑐𝑊))) ∈ ℝ)
296 efle 15926 . . . 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 584 . . 3 (𝜑 → ((log‘(𝑀 Σg (𝐹f𝑐𝑊))) ≤ (log‘(ℂfld Σg (𝐹f · 𝑊))) ↔ (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊))))))
298294, 297mpbid 231 . 2 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) ≤ (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))))
299127reeflogd 25885 . . 3 (𝜑 → (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))) = (𝑀 Σg (𝐹f𝑐𝑊)))
300299eqcomd 2742 . 2 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) = (exp‘(log‘(𝑀 Σg (𝐹f𝑐𝑊)))))
301148reeflogd 25885 . . 3 (𝜑 → (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))) = (ℂfld Σg (𝐹f · 𝑊)))
302301eqcomd 2742 . 2 (𝜑 → (ℂfld Σg (𝐹f · 𝑊)) = (exp‘(log‘(ℂfld Σg (𝐹f · 𝑊)))))
303298, 300, 3023brtr4d 5124 1 (𝜑 → (𝑀 Σg (𝐹f𝑐𝑊)) ≤ (ℂfld Σg (𝐹f · 𝑊)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1540  wcel 2105  wne 2940  Vcvv 3441  cdif 3895  wss 3898  c0 4269  {csn 4573   class class class wbr 5092  cmpt 5175  cres 5622  ccom 5624  wf 6475  1-1-ontowf1o 6478  cfv 6479  (class class class)co 7337  f cof 7593  Fincfn 8804  cc 10970  cr 10971  0cc0 10972  1c1 10973   + caddc 10975   · cmul 10977  +∞cpnf 11107   < clt 11110  cle 11111  cmin 11306  -cneg 11307   / cdiv 11733  +crp 12831  (,)cioo 13180  [,)cico 13182  [,]cicc 13183  Σcsu 15496  expce 15870  Basecbs 17009  s cress 17038  0gc0g 17247   Σg cgsu 17248  Mndcmnd 18482   MndHom cmhm 18525  SubMndcsubmnd 18526  SubGrpcsubg 18845   GrpHom cghm 18927   GrpIso cgim 18969  CMndccmn 19481  mulGrpcmgp 19815  Ringcrg 19878  CRingccrg 19879  DivRingcdr 20093  SubRingcsubrg 20125  fldccnfld 20703  fldcrefld 20915  logclog 25816  𝑐ccxp 25817
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2707  ax-rep 5229  ax-sep 5243  ax-nul 5250  ax-pow 5308  ax-pr 5372  ax-un 7650  ax-inf2 9498  ax-cnex 11028  ax-resscn 11029  ax-1cn 11030  ax-icn 11031  ax-addcl 11032  ax-addrcl 11033  ax-mulcl 11034  ax-mulrcl 11035  ax-mulcom 11036  ax-addass 11037  ax-mulass 11038  ax-distr 11039  ax-i2m1 11040  ax-1ne0 11041  ax-1rid 11042  ax-rnegex 11043  ax-rrecex 11044  ax-cnre 11045  ax-pre-lttri 11046  ax-pre-lttrn 11047  ax-pre-ltadd 11048  ax-pre-mulgt0 11049  ax-pre-sup 11050  ax-addf 11051  ax-mulf 11052
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3349  df-reu 3350  df-rab 3404  df-v 3443  df-sbc 3728  df-csb 3844  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3917  df-nul 4270  df-if 4474  df-pw 4549  df-sn 4574  df-pr 4576  df-tp 4578  df-op 4580  df-uni 4853  df-int 4895  df-iun 4943  df-iin 4944  df-br 5093  df-opab 5155  df-mpt 5176  df-tr 5210  df-id 5518  df-eprel 5524  df-po 5532  df-so 5533  df-fr 5575  df-se 5576  df-we 5577  df-xp 5626  df-rel 5627  df-cnv 5628  df-co 5629  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633  df-pred 6238  df-ord 6305  df-on 6306  df-lim 6307  df-suc 6308  df-iota 6431  df-fun 6481  df-fn 6482  df-f 6483  df-f1 6484  df-fo 6485  df-f1o 6486  df-fv 6487  df-isom 6488  df-riota 7293  df-ov 7340  df-oprab 7341  df-mpo 7342  df-of 7595  df-om 7781  df-1st 7899  df-2nd 7900  df-supp 8048  df-tpos 8112  df-frecs 8167  df-wrecs 8198  df-recs 8272  df-rdg 8311  df-1o 8367  df-2o 8368  df-er 8569  df-map 8688  df-pm 8689  df-ixp 8757  df-en 8805  df-dom 8806  df-sdom 8807  df-fin 8808  df-fsupp 9227  df-fi 9268  df-sup 9299  df-inf 9300  df-oi 9367  df-card 9796  df-pnf 11112  df-mnf 11113  df-xr 11114  df-ltxr 11115  df-le 11116  df-sub 11308  df-neg 11309  df-div 11734  df-nn 12075  df-2 12137  df-3 12138  df-4 12139  df-5 12140  df-6 12141  df-7 12142  df-8 12143  df-9 12144  df-n0 12335  df-z 12421  df-dec 12539  df-uz 12684  df-q 12790  df-rp 12832  df-xneg 12949  df-xadd 12950  df-xmul 12951  df-ioo 13184  df-ioc 13185  df-ico 13186  df-icc 13187  df-fz 13341  df-fzo 13484  df-fl 13613  df-mod 13691  df-seq 13823  df-exp 13884  df-fac 14089  df-bc 14118  df-hash 14146  df-shft 14877  df-cj 14909  df-re 14910  df-im 14911  df-sqrt 15045  df-abs 15046  df-limsup 15279  df-clim 15296  df-rlim 15297  df-sum 15497  df-ef 15876  df-sin 15878  df-cos 15879  df-pi 15881  df-struct 16945  df-sets 16962  df-slot 16980  df-ndx 16992  df-base 17010  df-ress 17039  df-plusg 17072  df-mulr 17073  df-starv 17074  df-sca 17075  df-vsca 17076  df-ip 17077  df-tset 17078  df-ple 17079  df-ds 17081  df-unif 17082  df-hom 17083  df-cco 17084  df-rest 17230  df-topn 17231  df-0g 17249  df-gsum 17250  df-topgen 17251  df-pt 17252  df-prds 17255  df-xrs 17310  df-qtop 17315  df-imas 17316  df-xps 17318  df-mre 17392  df-mrc 17393  df-acs 17395  df-mgm 18423  df-sgrp 18472  df-mnd 18483  df-mhm 18527  df-submnd 18528  df-grp 18676  df-minusg 18677  df-mulg 18797  df-subg 18848  df-ghm 18928  df-gim 18971  df-cntz 19019  df-cmn 19483  df-abl 19484  df-mgp 19816  df-ur 19833  df-ring 19880  df-cring 19881  df-oppr 19957  df-dvdsr 19978  df-unit 19979  df-invr 20009  df-dvr 20020  df-drng 20095  df-subrg 20127  df-psmet 20695  df-xmet 20696  df-met 20697  df-bl 20698  df-mopn 20699  df-fbas 20700  df-fg 20701  df-cnfld 20704  df-refld 20916  df-top 22149  df-topon 22166  df-topsp 22188  df-bases 22202  df-cld 22276  df-ntr 22277  df-cls 22278  df-nei 22355  df-lp 22393  df-perf 22394  df-cn 22484  df-cnp 22485  df-haus 22572  df-cmp 22644  df-tx 22819  df-hmeo 23012  df-fil 23103  df-fm 23195  df-flim 23196  df-flf 23197  df-xms 23579  df-ms 23580  df-tms 23581  df-cncf 24147  df-limc 25136  df-dv 25137  df-log 25818  df-cxp 25819
This theorem is referenced by:  amgmlemALT  46866  amgmw2d  46867
  Copyright terms: Public domain W3C validator