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 ffvelcdmda 
 |-  ( ( ph /\ k e. A ) -> ( F ` k ) e. RR+ )
8 5 ffvelcdmda 
 |-  ( ( 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 ffvelcdmda 
 |-  ( ( 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 ) ) )