Metamath Proof Explorer

Theorem jensen

Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015) (Proof shortened by AV, 27-Jul-2019)

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 ) ) ) )
Assertion jensen 
|- ( ph -> ( ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) e. D /\ ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) ) )

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 5 ffnd 
 |-  ( ph -> T Fn A )
10 fnresdm 
 |-  ( T Fn A -> ( T |` A ) = T )
11 9 10 syl 
 |-  ( ph -> ( T |` A ) = T )
12 11 oveq2d 
 |-  ( ph -> ( CCfld gsum ( T |` A ) ) = ( CCfld gsum T ) )
13 7 12 breqtrrd 
 |-  ( ph -> 0 < ( CCfld gsum ( T |` A ) ) )
14 ssid 
 |-  A C_ A
15 13 14 jctil 
 |-  ( ph -> ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) )
16 sseq1 
 |-  ( a = (/) -> ( a C_ A <-> (/) C_ A ) )
17 reseq2 
 |-  ( a = (/) -> ( T |` a ) = ( T |` (/) ) )
18 res0 
 |-  ( T |` (/) ) = (/)
19 17 18 eqtrdi 
 |-  ( a = (/) -> ( T |` a ) = (/) )
20 19 oveq2d 
 |-  ( a = (/) -> ( CCfld gsum ( T |` a ) ) = ( CCfld gsum (/) ) )
21 cnfld0 
 |-  0 = ( 0g ` CCfld )
22 21 gsum0 
 |-  ( CCfld gsum (/) ) = 0
23 20 22 eqtrdi 
 |-  ( a = (/) -> ( CCfld gsum ( T |` a ) ) = 0 )
24 23 breq2d 
 |-  ( a = (/) -> ( 0 < ( CCfld gsum ( T |` a ) ) <-> 0 < 0 ) )
25 16 24 anbi12d 
 |-  ( a = (/) -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) <-> ( (/) C_ A /\ 0 < 0 ) ) )
26 reseq2 
 |-  ( a = (/) -> ( ( T oF x. X ) |` a ) = ( ( T oF x. X ) |` (/) ) )
27 26 oveq2d 
 |-  ( a = (/) -> ( CCfld gsum ( ( T oF x. X ) |` a ) ) = ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) )
28 27 23 oveq12d 
 |-  ( a = (/) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) )
29 reseq2 
 |-  ( a = (/) -> ( ( T oF x. ( F o. X ) ) |` a ) = ( ( T oF x. ( F o. X ) ) |` (/) ) )
30 29 oveq2d 
 |-  ( a = (/) -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) = ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) )
31 30 23 oveq12d 
 |-  ( a = (/) -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) )
32 31 breq2d 
 |-  ( a = (/) -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) <-> ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) ) )
33 32 rabbidv 
 |-  ( a = (/) -> { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } = { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } )
34 28 33 eleq12d 
 |-  ( a = (/) -> ( ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } <-> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } ) )
35 25 34 imbi12d 
 |-  ( a = (/) -> ( ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) <-> ( ( (/) C_ A /\ 0 < 0 ) -> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } ) ) )
36 35 imbi2d 
 |-  ( a = (/) -> ( ( ph -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) ) <-> ( ph -> ( ( (/) C_ A /\ 0 < 0 ) -> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } ) ) ) )
37 sseq1 
 |-  ( a = k -> ( a C_ A <-> k C_ A ) )
38 reseq2 
 |-  ( a = k -> ( T |` a ) = ( T |` k ) )
39 38 oveq2d 
 |-  ( a = k -> ( CCfld gsum ( T |` a ) ) = ( CCfld gsum ( T |` k ) ) )
40 39 breq2d 
 |-  ( a = k -> ( 0 < ( CCfld gsum ( T |` a ) ) <-> 0 < ( CCfld gsum ( T |` k ) ) ) )
41 37 40 anbi12d 
 |-  ( a = k -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) <-> ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) ) )
42 reseq2 
 |-  ( a = k -> ( ( T oF x. X ) |` a ) = ( ( T oF x. X ) |` k ) )
43 42 oveq2d 
 |-  ( a = k -> ( CCfld gsum ( ( T oF x. X ) |` a ) ) = ( CCfld gsum ( ( T oF x. X ) |` k ) ) )
44 43 39 oveq12d 
 |-  ( a = k -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) )
45 reseq2 
 |-  ( a = k -> ( ( T oF x. ( F o. X ) ) |` a ) = ( ( T oF x. ( F o. X ) ) |` k ) )
46 45 oveq2d 
 |-  ( a = k -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) = ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) )
47 46 39 oveq12d 
 |-  ( a = k -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) )
48 47 breq2d 
 |-  ( a = k -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) <-> ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) )
49 48 rabbidv 
 |-  ( a = k -> { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } = { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } )
50 44 49 eleq12d 
 |-  ( a = k -> ( ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } <-> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) )
51 41 50 imbi12d 
 |-  ( a = k -> ( ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) <-> ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) )
52 51 imbi2d 
 |-  ( a = k -> ( ( ph -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) ) <-> ( ph -> ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) ) )
53 sseq1 
 |-  ( a = ( k u. { c } ) -> ( a C_ A <-> ( k u. { c } ) C_ A ) )
54 reseq2 
 |-  ( a = ( k u. { c } ) -> ( T |` a ) = ( T |` ( k u. { c } ) ) )
55 54 oveq2d 
 |-  ( a = ( k u. { c } ) -> ( CCfld gsum ( T |` a ) ) = ( CCfld gsum ( T |` ( k u. { c } ) ) ) )
56 55 breq2d 
 |-  ( a = ( k u. { c } ) -> ( 0 < ( CCfld gsum ( T |` a ) ) <-> 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) )
57 53 56 anbi12d 
 |-  ( a = ( k u. { c } ) -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) <-> ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
58 reseq2 
 |-  ( a = ( k u. { c } ) -> ( ( T oF x. X ) |` a ) = ( ( T oF x. X ) |` ( k u. { c } ) ) )
59 58 oveq2d 
 |-  ( a = ( k u. { c } ) -> ( CCfld gsum ( ( T oF x. X ) |` a ) ) = ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) )
60 59 55 oveq12d 
 |-  ( a = ( k u. { c } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) )
61 reseq2 
 |-  ( a = ( k u. { c } ) -> ( ( T oF x. ( F o. X ) ) |` a ) = ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) )
62 61 oveq2d 
 |-  ( a = ( k u. { c } ) -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) = ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) )
63 62 55 oveq12d 
 |-  ( a = ( k u. { c } ) -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) )
64 63 breq2d 
 |-  ( a = ( k u. { c } ) -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) <-> ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
65 64 rabbidv 
 |-  ( a = ( k u. { c } ) -> { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } = { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } )
66 60 65 eleq12d 
 |-  ( a = ( k u. { c } ) -> ( ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } <-> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
67 57 66 imbi12d 
 |-  ( a = ( k u. { c } ) -> ( ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) <-> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) )
68 67 imbi2d 
 |-  ( a = ( k u. { c } ) -> ( ( ph -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) ) <-> ( ph -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) ) )
69 sseq1 
 |-  ( a = A -> ( a C_ A <-> A C_ A ) )
70 reseq2 
 |-  ( a = A -> ( T |` a ) = ( T |` A ) )
71 70 oveq2d 
 |-  ( a = A -> ( CCfld gsum ( T |` a ) ) = ( CCfld gsum ( T |` A ) ) )
72 71 breq2d 
 |-  ( a = A -> ( 0 < ( CCfld gsum ( T |` a ) ) <-> 0 < ( CCfld gsum ( T |` A ) ) ) )
73 69 72 anbi12d 
 |-  ( a = A -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) <-> ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) ) )
74 reseq2 
 |-  ( a = A -> ( ( T oF x. X ) |` a ) = ( ( T oF x. X ) |` A ) )
75 74 oveq2d 
 |-  ( a = A -> ( CCfld gsum ( ( T oF x. X ) |` a ) ) = ( CCfld gsum ( ( T oF x. X ) |` A ) ) )
76 75 71 oveq12d 
 |-  ( a = A -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) )
77 reseq2 
 |-  ( a = A -> ( ( T oF x. ( F o. X ) ) |` a ) = ( ( T oF x. ( F o. X ) ) |` A ) )
78 77 oveq2d 
 |-  ( a = A -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) = ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) )
79 78 71 oveq12d 
 |-  ( a = A -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) = ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) )
80 79 breq2d 
 |-  ( a = A -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) <-> ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) ) )
81 80 rabbidv 
 |-  ( a = A -> { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } = { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } )
82 76 81 eleq12d 
 |-  ( a = A -> ( ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } <-> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } ) )
83 73 82 imbi12d 
 |-  ( a = A -> ( ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) <-> ( ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } ) ) )
84 83 imbi2d 
 |-  ( a = A -> ( ( ph -> ( ( a C_ A /\ 0 < ( CCfld gsum ( T |` a ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` a ) ) / ( CCfld gsum ( T |` a ) ) ) } ) ) <-> ( ph -> ( ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } ) ) ) )
85 0re 
 |-  0 e. RR
86 85 ltnri 
 |-  -. 0 < 0
87 86 pm2.21i 
 |-  ( 0 < 0 -> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } )
88 87 adantl 
 |-  ( ( (/) C_ A /\ 0 < 0 ) -> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } )
89 88 a1i 
 |-  ( ph -> ( ( (/) C_ A /\ 0 < 0 ) -> ( ( CCfld gsum ( ( T oF x. X ) |` (/) ) ) / 0 ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` (/) ) ) / 0 ) } ) )
90 impexp 
 |-  ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) <-> ( k C_ A -> ( 0 < ( CCfld gsum ( T |` k ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) )
91 simprl 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( k u. { c } ) C_ A )
92 91 unssad 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> k C_ A )
93 simpr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> 0 < ( CCfld gsum ( T |` k ) ) )
94 1 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> D C_ RR )
95 2 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> F : D --> RR )
96 simplll 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ph )
97 96 3 sylan 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) /\ ( a e. D /\ b e. D ) ) -> ( a [,] b ) C_ D )
98 96 4 syl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> A e. Fin )
99 96 5 syl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> T : A --> ( 0 [,) +oo ) )
100 96 6 syl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> X : A --> D )
101 7 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> 0 < ( CCfld gsum T ) )
102 96 8 sylan 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) /\ ( 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 ) ) ) )
103 simpllr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> -. c e. k )
104 91 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( k u. { c } ) C_ A )
105 eqid 
 |-  ( CCfld gsum ( T |` k ) ) = ( CCfld gsum ( T |` k ) )
106 eqid 
 |-  ( CCfld gsum ( T |` ( k u. { c } ) ) ) = ( CCfld gsum ( T |` ( k u. { c } ) ) )
107 cnring 
 |-  CCfld e. Ring
108 ringcmn 
 |-  ( CCfld e. Ring -> CCfld e. CMnd )
109 107 108 mp1i 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> CCfld e. CMnd )
110 4 ad2antrr 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> A e. Fin )
111 110 92 ssfid 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> k e. Fin )
112 rege0subm 
 |-  ( 0 [,) +oo ) e. ( SubMnd ` CCfld )
113 112 a1i 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( 0 [,) +oo ) e. ( SubMnd ` CCfld ) )
114 5 ad2antrr 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> T : A --> ( 0 [,) +oo ) )
115 114 92 fssresd 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( T |` k ) : k --> ( 0 [,) +oo ) )
116 c0ex 
 |-  0 e. _V
117 116 a1i 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> 0 e. _V )
118 115 111 117 fdmfifsupp 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( T |` k ) finSupp 0 )
119 21 109 111 113 115 118 gsumsubmcl 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( CCfld gsum ( T |` k ) ) e. ( 0 [,) +oo ) )
120 elrege0 
 |-  ( ( CCfld gsum ( T |` k ) ) e. ( 0 [,) +oo ) <-> ( ( CCfld gsum ( T |` k ) ) e. RR /\ 0 <_ ( CCfld gsum ( T |` k ) ) ) )
121 120 simplbi 
 |-  ( ( CCfld gsum ( T |` k ) ) e. ( 0 [,) +oo ) -> ( CCfld gsum ( T |` k ) ) e. RR )
122 119 121 syl 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( CCfld gsum ( T |` k ) ) e. RR )
123 122 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( CCfld gsum ( T |` k ) ) e. RR )
124 simprl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> 0 < ( CCfld gsum ( T |` k ) ) )
125 123 124 elrpd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( CCfld gsum ( T |` k ) ) e. RR+ )
126 simprr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } )
127 fveq2 
 |-  ( w = ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) -> ( F ` w ) = ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) )
128 127 breq1d 
 |-  ( w = ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) <-> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) )
129 128 elrab 
 |-  ( ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } <-> ( ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. D /\ ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) )
130 126 129 sylib 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. D /\ ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) )
131 130 simpld 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. D )
132 130 simprd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) )
133 94 95 97 98 99 100 101 102 103 104 105 106 125 131 132 jensenlem2 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. D /\ ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
134 fveq2 
 |-  ( w = ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( F ` w ) = ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
135 134 breq1d 
 |-  ( w = ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) <-> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
136 135 elrab 
 |-  ( ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } <-> ( ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. D /\ ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) )
137 133 136 sylibr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ ( 0 < ( CCfld gsum ( T |` k ) ) /\ ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } )
138 137 expr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
139 93 138 embantd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( 0 < ( CCfld gsum ( T |` k ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
140 cnfldbas 
 |-  CC = ( Base ` CCfld )
141 ringmnd 
 |-  ( CCfld e. Ring -> CCfld e. Mnd )
142 107 141 mp1i 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> CCfld e. Mnd )
143 110 91 ssfid 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( k u. { c } ) e. Fin )
144 143 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( k u. { c } ) e. Fin )
145 ssun2 
 |-  { c } C_ ( k u. { c } )
146 vsnid 
 |-  c e. { c }
147 145 146 sselii 
 |-  c e. ( k u. { c } )
148 147 a1i 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> c e. ( k u. { c } ) )
149 remulcl 
 |-  ( ( x e. RR /\ y e. RR ) -> ( x x. y ) e. RR )
150 149 adantl 
 |-  ( ( ph /\ ( x e. RR /\ y e. RR ) ) -> ( x x. y ) e. RR )
151 rge0ssre 
 |-  ( 0 [,) +oo ) C_ RR
152 fss 
 |-  ( ( T : A --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ RR ) -> T : A --> RR )
153 5 151 152 sylancl 
 |-  ( ph -> T : A --> RR )
154 6 1 fssd 
 |-  ( ph -> X : A --> RR )
155 inidm 
 |-  ( A i^i A ) = A
156 150 153 154 4 4 155 off 
 |-  ( ph -> ( T oF x. X ) : A --> RR )
157 ax-resscn 
 |-  RR C_ CC
158 fss 
 |-  ( ( ( T oF x. X ) : A --> RR /\ RR C_ CC ) -> ( T oF x. X ) : A --> CC )
159 156 157 158 sylancl 
 |-  ( ph -> ( T oF x. X ) : A --> CC )
160 159 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T oF x. X ) : A --> CC )
161 91 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( k u. { c } ) C_ A )
162 160 161 fssresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. X ) |` ( k u. { c } ) ) : ( k u. { c } ) --> CC )
163 5 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> T : A --> ( 0 [,) +oo ) )
164 110 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> A e. Fin )
165 163 164 fexd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> T e. _V )
166 6 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> X : A --> D )
167 166 164 fexd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> X e. _V )
168 offres 
 |-  ( ( T e. _V /\ X e. _V ) -> ( ( T oF x. X ) |` ( k u. { c } ) ) = ( ( T |` ( k u. { c } ) ) oF x. ( X |` ( k u. { c } ) ) ) )
169 165 167 168 syl2anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. X ) |` ( k u. { c } ) ) = ( ( T |` ( k u. { c } ) ) oF x. ( X |` ( k u. { c } ) ) ) )
170 169 oveq1d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. X ) |` ( k u. { c } ) ) supp 0 ) = ( ( ( T |` ( k u. { c } ) ) oF x. ( X |` ( k u. { c } ) ) ) supp 0 ) )
171 151 157 sstri 
 |-  ( 0 [,) +oo ) C_ CC
172 fss 
 |-  ( ( T : A --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> T : A --> CC )
173 163 171 172 sylancl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> T : A --> CC )
174 173 161 fssresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T |` ( k u. { c } ) ) : ( k u. { c } ) --> CC )
175 eldifi 
 |-  ( x e. ( ( k u. { c } ) \ { c } ) -> x e. ( k u. { c } ) )
176 175 adantl 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. ( ( k u. { c } ) \ { c } ) ) -> x e. ( k u. { c } ) )
177 176 fvresd 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. ( ( k u. { c } ) \ { c } ) ) -> ( ( T |` ( k u. { c } ) ) ` x ) = ( T ` x ) )
178 difun2 
 |-  ( ( k u. { c } ) \ { c } ) = ( k \ { c } )
179 difss 
 |-  ( k \ { c } ) C_ k
180 178 179 eqsstri 
 |-  ( ( k u. { c } ) \ { c } ) C_ k
181 180 sseli 
 |-  ( x e. ( ( k u. { c } ) \ { c } ) -> x e. k )
182 simpr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> 0 = ( CCfld gsum ( T |` k ) ) )
183 92 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> k C_ A )
184 163 183 feqresmpt 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T |` k ) = ( x e. k |-> ( T ` x ) ) )
185 184 oveq2d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( T |` k ) ) = ( CCfld gsum ( x e. k |-> ( T ` x ) ) ) )
186 111 adantr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> k e. Fin )
187 183 sselda 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> x e. A )
188 163 ffvelrnda 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. A ) -> ( T ` x ) e. ( 0 [,) +oo ) )
189 187 188 syldan 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> ( T ` x ) e. ( 0 [,) +oo ) )
190 171 189 sselid 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> ( T ` x ) e. CC )
191 186 190 gsumfsum 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( x e. k |-> ( T ` x ) ) ) = sum_ x e. k ( T ` x ) )
192 182 185 191 3eqtrrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> sum_ x e. k ( T ` x ) = 0 )
193 elrege0 
 |-  ( ( T ` x ) e. ( 0 [,) +oo ) <-> ( ( T ` x ) e. RR /\ 0 <_ ( T ` x ) ) )
194 189 193 sylib 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> ( ( T ` x ) e. RR /\ 0 <_ ( T ` x ) ) )
195 194 simpld 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> ( T ` x ) e. RR )
196 194 simprd 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> 0 <_ ( T ` x ) )
197 186 195 196 fsum00 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( sum_ x e. k ( T ` x ) = 0 <-> A. x e. k ( T ` x ) = 0 ) )
198 192 197 mpbid 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> A. x e. k ( T ` x ) = 0 )
199 198 r19.21bi 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. k ) -> ( T ` x ) = 0 )
200 181 199 sylan2 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. ( ( k u. { c } ) \ { c } ) ) -> ( T ` x ) = 0 )
201 177 200 eqtrd 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. ( ( k u. { c } ) \ { c } ) ) -> ( ( T |` ( k u. { c } ) ) ` x ) = 0 )
202 174 201 suppss 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T |` ( k u. { c } ) ) supp 0 ) C_ { c } )
203 mul02 
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
204 203 adantl 
 |-  ( ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) /\ x e. CC ) -> ( 0 x. x ) = 0 )
205 1 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> D C_ RR )
206 205 157 sstrdi 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> D C_ CC )
207 166 206 fssd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> X : A --> CC )
208 207 161 fssresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( X |` ( k u. { c } ) ) : ( k u. { c } ) --> CC )
209 116 a1i 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> 0 e. _V )
210 202 204 174 208 144 209 suppssof1 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T |` ( k u. { c } ) ) oF x. ( X |` ( k u. { c } ) ) ) supp 0 ) C_ { c } )
211 170 210 eqsstrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. X ) |` ( k u. { c } ) ) supp 0 ) C_ { c } )
212 140 21 142 144 148 162 211 gsumpt 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) = ( ( ( T oF x. X ) |` ( k u. { c } ) ) ` c ) )
213 148 fvresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. X ) |` ( k u. { c } ) ) ` c ) = ( ( T oF x. X ) ` c ) )
214 163 ffnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> T Fn A )
215 166 ffnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> X Fn A )
216 161 148 sseldd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> c e. A )
217 fnfvof 
 |-  ( ( ( T Fn A /\ X Fn A ) /\ ( A e. Fin /\ c e. A ) ) -> ( ( T oF x. X ) ` c ) = ( ( T ` c ) x. ( X ` c ) ) )
218 214 215 164 216 217 syl22anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. X ) ` c ) = ( ( T ` c ) x. ( X ` c ) ) )
219 212 213 218 3eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) = ( ( T ` c ) x. ( X ` c ) ) )
220 140 21 142 144 148 174 202 gsumpt 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( T |` ( k u. { c } ) ) ) = ( ( T |` ( k u. { c } ) ) ` c ) )
221 148 fvresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T |` ( k u. { c } ) ) ` c ) = ( T ` c ) )
222 220 221 eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( T |` ( k u. { c } ) ) ) = ( T ` c ) )
223 219 222 oveq12d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) = ( ( ( T ` c ) x. ( X ` c ) ) / ( T ` c ) ) )
224 207 216 ffvelrnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( X ` c ) e. CC )
225 173 216 ffvelrnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T ` c ) e. CC )
226 simplrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) )
227 226 222 breqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> 0 < ( T ` c ) )
228 227 gt0ne0d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T ` c ) =/= 0 )
229 224 225 228 divcan3d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T ` c ) x. ( X ` c ) ) / ( T ` c ) ) = ( X ` c ) )
230 223 229 eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) = ( X ` c ) )
231 166 216 ffvelrnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( X ` c ) e. D )
232 230 231 eqeltrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. D )
233 2 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> F : D --> RR )
234 233 231 ffvelrnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F ` ( X ` c ) ) e. RR )
235 234 leidd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F ` ( X ` c ) ) <_ ( F ` ( X ` c ) ) )
236 230 fveq2d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) = ( F ` ( X ` c ) ) )
237 fco 
 |-  ( ( F : D --> RR /\ X : A --> D ) -> ( F o. X ) : A --> RR )
238 2 6 237 syl2anc 
 |-  ( ph -> ( F o. X ) : A --> RR )
239 150 153 238 4 4 155 off 
 |-  ( ph -> ( T oF x. ( F o. X ) ) : A --> RR )
240 fss 
 |-  ( ( ( T oF x. ( F o. X ) ) : A --> RR /\ RR C_ CC ) -> ( T oF x. ( F o. X ) ) : A --> CC )
241 239 157 240 sylancl 
 |-  ( ph -> ( T oF x. ( F o. X ) ) : A --> CC )
242 241 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( T oF x. ( F o. X ) ) : A --> CC )
243 242 161 fssresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) : ( k u. { c } ) --> CC )
244 238 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F o. X ) : A --> RR )
245 244 164 fexd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F o. X ) e. _V )
246 offres 
 |-  ( ( T e. _V /\ ( F o. X ) e. _V ) -> ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) = ( ( T |` ( k u. { c } ) ) oF x. ( ( F o. X ) |` ( k u. { c } ) ) ) )
247 165 245 246 syl2anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) = ( ( T |` ( k u. { c } ) ) oF x. ( ( F o. X ) |` ( k u. { c } ) ) ) )
248 247 oveq1d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) supp 0 ) = ( ( ( T |` ( k u. { c } ) ) oF x. ( ( F o. X ) |` ( k u. { c } ) ) ) supp 0 ) )
249 fss 
 |-  ( ( ( F o. X ) : A --> RR /\ RR C_ CC ) -> ( F o. X ) : A --> CC )
250 244 157 249 sylancl 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F o. X ) : A --> CC )
251 250 161 fssresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( F o. X ) |` ( k u. { c } ) ) : ( k u. { c } ) --> CC )
252 202 204 174 251 144 209 suppssof1 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T |` ( k u. { c } ) ) oF x. ( ( F o. X ) |` ( k u. { c } ) ) ) supp 0 ) C_ { c } )
253 248 252 eqsstrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) supp 0 ) C_ { c } )
254 140 21 142 144 148 243 253 gsumpt 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) = ( ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ` c ) )
255 148 fvresd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ` c ) = ( ( T oF x. ( F o. X ) ) ` c ) )
256 2 ffnd 
 |-  ( ph -> F Fn D )
257 fnfco 
 |-  ( ( F Fn D /\ X : A --> D ) -> ( F o. X ) Fn A )
258 256 6 257 syl2anc 
 |-  ( ph -> ( F o. X ) Fn A )
259 258 ad3antrrr 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F o. X ) Fn A )
260 fnfvof 
 |-  ( ( ( T Fn A /\ ( F o. X ) Fn A ) /\ ( A e. Fin /\ c e. A ) ) -> ( ( T oF x. ( F o. X ) ) ` c ) = ( ( T ` c ) x. ( ( F o. X ) ` c ) ) )
261 214 259 164 216 260 syl22anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. ( F o. X ) ) ` c ) = ( ( T ` c ) x. ( ( F o. X ) ` c ) ) )
262 fvco3 
 |-  ( ( X : A --> D /\ c e. A ) -> ( ( F o. X ) ` c ) = ( F ` ( X ` c ) ) )
263 166 216 262 syl2anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( F o. X ) ` c ) = ( F ` ( X ` c ) ) )
264 263 oveq2d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T ` c ) x. ( ( F o. X ) ` c ) ) = ( ( T ` c ) x. ( F ` ( X ` c ) ) ) )
265 261 264 eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( T oF x. ( F o. X ) ) ` c ) = ( ( T ` c ) x. ( F ` ( X ` c ) ) ) )
266 254 255 265 3eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) = ( ( T ` c ) x. ( F ` ( X ` c ) ) ) )
267 266 222 oveq12d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) = ( ( ( T ` c ) x. ( F ` ( X ` c ) ) ) / ( T ` c ) ) )
268 234 recnd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F ` ( X ` c ) ) e. CC )
269 268 225 228 divcan3d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( ( T ` c ) x. ( F ` ( X ` c ) ) ) / ( T ` c ) ) = ( F ` ( X ` c ) ) )
270 267 269 eqtrd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) = ( F ` ( X ` c ) ) )
271 235 236 270 3brtr4d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( F ` ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) )
272 135 232 271 elrabd 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } )
273 272 a1d 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> ( ( 0 < ( CCfld gsum ( T |` k ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
274 120 simprbi 
 |-  ( ( CCfld gsum ( T |` k ) ) e. ( 0 [,) +oo ) -> 0 <_ ( CCfld gsum ( T |` k ) ) )
275 119 274 syl 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> 0 <_ ( CCfld gsum ( T |` k ) ) )
276 leloe 
 |-  ( ( 0 e. RR /\ ( CCfld gsum ( T |` k ) ) e. RR ) -> ( 0 <_ ( CCfld gsum ( T |` k ) ) <-> ( 0 < ( CCfld gsum ( T |` k ) ) \/ 0 = ( CCfld gsum ( T |` k ) ) ) ) )
277 85 122 276 sylancr 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( 0 <_ ( CCfld gsum ( T |` k ) ) <-> ( 0 < ( CCfld gsum ( T |` k ) ) \/ 0 = ( CCfld gsum ( T |` k ) ) ) ) )
278 275 277 mpbid 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( 0 < ( CCfld gsum ( T |` k ) ) \/ 0 = ( CCfld gsum ( T |` k ) ) ) )
279 139 273 278 mpjaodan 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( ( 0 < ( CCfld gsum ( T |` k ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
280 92 279 embantd 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( ( k C_ A -> ( 0 < ( CCfld gsum ( T |` k ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
281 90 280 syl5bi 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) )
282 281 ex 
 |-  ( ( ph /\ -. c e. k ) -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) )
283 282 com23 
 |-  ( ( ph /\ -. c e. k ) -> ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) )
284 283 expcom 
 |-  ( -. c e. k -> ( ph -> ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) ) )
285 284 adantl 
 |-  ( ( k e. Fin /\ -. c e. k ) -> ( ph -> ( ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) ) )
286 285 a2d 
 |-  ( ( k e. Fin /\ -. c e. k ) -> ( ( ph -> ( ( k C_ A /\ 0 < ( CCfld gsum ( T |` k ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` k ) ) / ( CCfld gsum ( T |` k ) ) ) } ) ) -> ( ph -> ( ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` ( k u. { c } ) ) ) / ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) } ) ) ) )
287 36 52 68 84 89 286 findcard2s 
 |-  ( A e. Fin -> ( ph -> ( ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } ) ) )
288 4 287 mpcom 
 |-  ( ph -> ( ( A C_ A /\ 0 < ( CCfld gsum ( T |` A ) ) ) -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } ) )
289 15 288 mpd 
 |-  ( ph -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } )
290 156 ffnd 
 |-  ( ph -> ( T oF x. X ) Fn A )
291 fnresdm 
 |-  ( ( T oF x. X ) Fn A -> ( ( T oF x. X ) |` A ) = ( T oF x. X ) )
292 290 291 syl 
 |-  ( ph -> ( ( T oF x. X ) |` A ) = ( T oF x. X ) )
293 292 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( T oF x. X ) |` A ) ) = ( CCfld gsum ( T oF x. X ) ) )
294 293 12 oveq12d 
 |-  ( ph -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) = ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) )
295 9 258 4 4 155 offn 
 |-  ( ph -> ( T oF x. ( F o. X ) ) Fn A )
296 fnresdm 
 |-  ( ( T oF x. ( F o. X ) ) Fn A -> ( ( T oF x. ( F o. X ) ) |` A ) = ( T oF x. ( F o. X ) ) )
297 295 296 syl 
 |-  ( ph -> ( ( T oF x. ( F o. X ) ) |` A ) = ( T oF x. ( F o. X ) ) )
298 297 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) = ( CCfld gsum ( T oF x. ( F o. X ) ) ) )
299 298 12 oveq12d 
 |-  ( ph -> ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) = ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) )
300 299 breq2d 
 |-  ( ph -> ( ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) <-> ( F ` w ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) ) )
301 300 rabbidv 
 |-  ( ph -> { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) } = { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) } )
302 289 294 301 3eltr3d 
 |-  ( ph -> ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) } )
303 fveq2 
 |-  ( w = ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) -> ( F ` w ) = ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) )
304 303 breq1d 
 |-  ( w = ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) -> ( ( F ` w ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) <-> ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) ) )
305 304 elrab 
 |-  ( ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) e. { w e. D | ( F ` w ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) } <-> ( ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) e. D /\ ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) ) )
306 302 305 sylib 
 |-  ( ph -> ( ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) e. D /\ ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) <_ ( ( CCfld gsum ( T oF x. ( F o. X ) ) ) / ( CCfld gsum T ) ) ) )