Step |
Hyp |
Ref |
Expression |
1 |
|
jensen.1 |
|- ( ph -> D C_ RR ) |
2 |
|
jensen.2 |
|- ( ph -> F : D --> RR ) |
3 |
|
jensen.3 |
|- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D ) |
4 |
|
jensen.4 |
|- ( ph -> A e. Fin ) |
5 |
|
jensen.5 |
|- ( ph -> T : A --> ( 0 [,) +oo ) ) |
6 |
|
jensen.6 |
|- ( ph -> X : A --> D ) |
7 |
|
jensen.7 |
|- ( ph -> 0 < ( CCfld gsum T ) ) |
8 |
|
jensen.8 |
|- ( ( ph /\ ( x e. D /\ y e. D /\ t e. ( 0 [,] 1 ) ) ) -> ( F ` ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) <_ ( ( t x. ( F ` x ) ) + ( ( 1 - t ) x. ( F ` y ) ) ) ) |
9 |
|
jensenlem.1 |
|- ( ph -> -. z e. B ) |
10 |
|
jensenlem.2 |
|- ( ph -> ( B u. { z } ) C_ A ) |
11 |
|
jensenlem.s |
|- S = ( CCfld gsum ( T |` B ) ) |
12 |
|
jensenlem.l |
|- L = ( CCfld gsum ( T |` ( B u. { z } ) ) ) |
13 |
|
cnfldbas |
|- CC = ( Base ` CCfld ) |
14 |
|
cnfldadd |
|- + = ( +g ` CCfld ) |
15 |
|
cnring |
|- CCfld e. Ring |
16 |
|
ringcmn |
|- ( CCfld e. Ring -> CCfld e. CMnd ) |
17 |
15 16
|
mp1i |
|- ( ph -> CCfld e. CMnd ) |
18 |
10
|
unssad |
|- ( ph -> B C_ A ) |
19 |
4 18
|
ssfid |
|- ( ph -> B e. Fin ) |
20 |
|
rge0ssre |
|- ( 0 [,) +oo ) C_ RR |
21 |
|
ax-resscn |
|- RR C_ CC |
22 |
20 21
|
sstri |
|- ( 0 [,) +oo ) C_ CC |
23 |
18
|
sselda |
|- ( ( ph /\ x e. B ) -> x e. A ) |
24 |
5
|
ffvelrnda |
|- ( ( ph /\ x e. A ) -> ( T ` x ) e. ( 0 [,) +oo ) ) |
25 |
23 24
|
syldan |
|- ( ( ph /\ x e. B ) -> ( T ` x ) e. ( 0 [,) +oo ) ) |
26 |
22 25
|
sselid |
|- ( ( ph /\ x e. B ) -> ( T ` x ) e. CC ) |
27 |
10
|
unssbd |
|- ( ph -> { z } C_ A ) |
28 |
|
vex |
|- z e. _V |
29 |
28
|
snss |
|- ( z e. A <-> { z } C_ A ) |
30 |
27 29
|
sylibr |
|- ( ph -> z e. A ) |
31 |
5 30
|
ffvelrnd |
|- ( ph -> ( T ` z ) e. ( 0 [,) +oo ) ) |
32 |
22 31
|
sselid |
|- ( ph -> ( T ` z ) e. CC ) |
33 |
|
fveq2 |
|- ( x = z -> ( T ` x ) = ( T ` z ) ) |
34 |
13 14 17 19 26 30 9 32 33
|
gsumunsn |
|- ( ph -> ( CCfld gsum ( x e. ( B u. { z } ) |-> ( T ` x ) ) ) = ( ( CCfld gsum ( x e. B |-> ( T ` x ) ) ) + ( T ` z ) ) ) |
35 |
5 10
|
feqresmpt |
|- ( ph -> ( T |` ( B u. { z } ) ) = ( x e. ( B u. { z } ) |-> ( T ` x ) ) ) |
36 |
35
|
oveq2d |
|- ( ph -> ( CCfld gsum ( T |` ( B u. { z } ) ) ) = ( CCfld gsum ( x e. ( B u. { z } ) |-> ( T ` x ) ) ) ) |
37 |
5 18
|
feqresmpt |
|- ( ph -> ( T |` B ) = ( x e. B |-> ( T ` x ) ) ) |
38 |
37
|
oveq2d |
|- ( ph -> ( CCfld gsum ( T |` B ) ) = ( CCfld gsum ( x e. B |-> ( T ` x ) ) ) ) |
39 |
38
|
oveq1d |
|- ( ph -> ( ( CCfld gsum ( T |` B ) ) + ( T ` z ) ) = ( ( CCfld gsum ( x e. B |-> ( T ` x ) ) ) + ( T ` z ) ) ) |
40 |
34 36 39
|
3eqtr4d |
|- ( ph -> ( CCfld gsum ( T |` ( B u. { z } ) ) ) = ( ( CCfld gsum ( T |` B ) ) + ( T ` z ) ) ) |
41 |
11
|
oveq1i |
|- ( S + ( T ` z ) ) = ( ( CCfld gsum ( T |` B ) ) + ( T ` z ) ) |
42 |
40 12 41
|
3eqtr4g |
|- ( ph -> L = ( S + ( T ` z ) ) ) |