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 ) ) ) |