Metamath Proof Explorer


Theorem amgmwlem

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

Ref Expression
Hypotheses amgmwlem.0
|- M = ( mulGrp ` CCfld )
amgmwlem.1
|- ( ph -> A e. Fin )
amgmwlem.2
|- ( ph -> A =/= (/) )
amgmwlem.3
|- ( ph -> F : A --> RR+ )
amgmwlem.4
|- ( ph -> W : A --> RR+ )
amgmwlem.5
|- ( ph -> ( CCfld gsum W ) = 1 )
Assertion amgmwlem
|- ( ph -> ( M gsum ( F oF ^c W ) ) <_ ( CCfld gsum ( F oF x. W ) ) )

Proof

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