Metamath Proof Explorer

Theorem jensenlem1

Description: Lemma for jensen . (Contributed by Mario Carneiro, 4-Jun-2016)

Ref Expression
Hypotheses jensen.1 
|- ( ph -> D C_ RR )
jensen.2 
|- ( ph -> F : D --> RR )
jensen.3 
|- ( ( ph /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
jensen.4 
|- ( ph -> A e. Fin )
jensen.5 
|- ( ph -> T : A --> ( 0 [,) +oo ) )
jensen.6 
|- ( ph -> X : A --> D )
jensen.7 
|- ( ph -> 0 < ( CCfld gsum T ) )
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 ) ) ) )
jensenlem.1 
|- ( ph -> -. z e. B )
jensenlem.2 
|- ( ph -> ( B u. { z } ) C_ A )
jensenlem.s 
|- S = ( CCfld gsum ( T |` B ) )
jensenlem.l 
|- L = ( CCfld gsum ( T |` ( B u. { z } ) ) )
Assertion jensenlem1 
|- ( ph -> L = ( S + ( T ` z ) ) )

Proof

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 ffvelcdmda 
 |-  ( ( 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 ffvelcdmd 
 |-  ( 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 ) ) )