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 syl6eq 
 |-  ( 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 syl6eq 
 |-  ( 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 fex 
 |-  ( ( T : A --> ( 0 [,) +oo ) /\ A e. Fin ) -> T e. _V )
166 163 164 165 syl2anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> T e. _V )
167 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 )
168 fex 
 |-  ( ( X : A --> D /\ A e. Fin ) -> X e. _V )
169 167 164 168 syl2anc 
 |-  ( ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) /\ 0 = ( CCfld gsum ( T |` k ) ) ) -> X e. _V )
170 offres 
 |-  ( ( T e. _V /\ X e. _V ) -> ( ( T oF x. X ) |` ( k u. { c } ) ) = ( ( T |` ( k u. { c } ) ) oF x. ( X |` ( k u. { c } ) ) ) )
171 166 169 170 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 } ) ) ) )
172 171 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 ) )
173 151 157 sstri 
 |-  ( 0 [,) +oo ) C_ CC
174 fss 
 |-  ( ( T : A --> ( 0 [,) +oo ) /\ ( 0 [,) +oo ) C_ CC ) -> T : A --> CC )
175 163 173 174 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 )
176 175 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 )
177 eldifi 
 |-  ( x e. ( ( k u. { c } ) \ { c } ) -> x e. ( k u. { c } ) )
178 177 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 } ) )
179 178 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 ) )
180 difun2 
 |-  ( ( k u. { c } ) \ { c } ) = ( k \ { c } )
181 difss 
 |-  ( k \ { c } ) C_ k
182 180 181 eqsstri 
 |-  ( ( k u. { c } ) \ { c } ) C_ k
183 182 sseli 
 |-  ( x e. ( ( k u. { c } ) \ { c } ) -> x e. k )
184 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 ) ) )
185 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 )
186 163 185 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 ) ) )
187 186 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 ) ) ) )
188 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 )
189 185 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 )
190 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 ) )
191 189 190 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 ) )
192 173 191 sseldi 
 |-  ( ( ( ( ( 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 )
193 188 192 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 ) )
194 184 187 193 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 )
195 elrege0 
 |-  ( ( T ` x ) e. ( 0 [,) +oo ) <-> ( ( T ` x ) e. RR /\ 0 <_ ( T ` x ) ) )
196 191 195 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 ) ) )
197 196 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 )
198 196 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 ) )
199 188 197 198 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 ) )
200 194 199 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 )
201 200 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 )
202 183 201 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 )
203 179 202 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 )
204 176 203 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 } )
205 mul02 
 |-  ( x e. CC -> ( 0 x. x ) = 0 )
206 205 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 )
207 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 )
208 207 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 )
209 167 208 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 )
210 209 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 )
211 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 )
212 204 206 176 210 144 211 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 } )
213 172 212 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 } )
214 140 21 142 144 148 162 213 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 ) )
215 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 ) )
216 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 )
217 167 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 )
218 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 )
219 fnfvof 
 |-  ( ( ( T Fn A /\ X Fn A ) /\ ( A e. Fin /\ c e. A ) ) -> ( ( T oF x. X ) ` c ) = ( ( T ` c ) x. ( X ` c ) ) )
220 216 217 164 218 219 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 ) ) )
221 214 215 220 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 ) ) )
222 140 21 142 144 148 176 204 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 ) )
223 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 ) )
224 222 223 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 ) )
225 221 224 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 ) ) )
226 209 218 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 )
227 175 218 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 )
228 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 } ) ) ) )
229 228 224 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 ) )
230 229 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 )
231 226 227 230 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 ) )
232 225 231 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 ) )
233 167 218 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 )
234 232 233 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 )
235 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 )
236 235 233 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 )
237 236 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 ) ) )
238 232 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 ) ) )
239 fco 
 |-  ( ( F : D --> RR /\ X : A --> D ) -> ( F o. X ) : A --> RR )
240 2 6 239 syl2anc 
 |-  ( ph -> ( F o. X ) : A --> RR )
241 150 153 240 4 4 155 off 
 |-  ( ph -> ( T oF x. ( F o. X ) ) : A --> RR )
242 fss 
 |-  ( ( ( T oF x. ( F o. X ) ) : A --> RR /\ RR C_ CC ) -> ( T oF x. ( F o. X ) ) : A --> CC )
243 241 157 242 sylancl 
 |-  ( ph -> ( T oF x. ( F o. X ) ) : A --> CC )
244 243 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 )
245 244 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 )
246 240 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 )
247 fex 
 |-  ( ( ( F o. X ) : A --> RR /\ A e. Fin ) -> ( F o. X ) e. _V )
248 246 164 247 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 ) e. _V )
249 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 } ) ) ) )
250 166 248 249 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 } ) ) ) )
251 250 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 ) )
252 fss 
 |-  ( ( ( F o. X ) : A --> RR /\ RR C_ CC ) -> ( F o. X ) : A --> CC )
253 246 157 252 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 )
254 253 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 )
255 204 206 176 254 144 211 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 } )
256 251 255 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 } )
257 140 21 142 144 148 245 256 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 ) )
258 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 ) )
259 2 ffnd 
 |-  ( ph -> F Fn D )
260 fnfco 
 |-  ( ( F Fn D /\ X : A --> D ) -> ( F o. X ) Fn A )
261 259 6 260 syl2anc 
 |-  ( ph -> ( F o. X ) Fn A )
262 261 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 )
263 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 ) ) )
264 216 262 164 218 263 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 ) ) )
265 fvco3 
 |-  ( ( X : A --> D /\ c e. A ) -> ( ( F o. X ) ` c ) = ( F ` ( X ` c ) ) )
266 167 218 265 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 ) ) )
267 266 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 ) ) ) )
268 264 267 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 ) ) ) )
269 257 258 268 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 ) ) ) )
270 269 224 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 ) ) )
271 236 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 )
272 271 227 230 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 ) ) )
273 270 272 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 ) ) )
274 237 238 273 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 } ) ) ) ) )
275 135 234 274 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 } ) ) ) ) } )
276 275 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 } ) ) ) ) } ) )
277 120 simprbi 
 |-  ( ( CCfld gsum ( T |` k ) ) e. ( 0 [,) +oo ) -> 0 <_ ( CCfld gsum ( T |` k ) ) )
278 119 277 syl 
 |-  ( ( ( ph /\ -. c e. k ) /\ ( ( k u. { c } ) C_ A /\ 0 < ( CCfld gsum ( T |` ( k u. { c } ) ) ) ) ) -> 0 <_ ( CCfld gsum ( T |` k ) ) )
279 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 ) ) ) ) )
280 85 122 279 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 ) ) ) ) )
281 278 280 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 ) ) ) )
282 139 276 281 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 } ) ) ) ) } ) )
283 92 282 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 } ) ) ) ) } ) )
284 90 283 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 } ) ) ) ) } ) )
285 284 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 } ) ) ) ) } ) ) )
286 285 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 } ) ) ) ) } ) ) )
287 286 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 } ) ) ) ) } ) ) ) )
288 287 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 } ) ) ) ) } ) ) ) )
289 288 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 } ) ) ) ) } ) ) ) )
290 36 52 68 84 89 289 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 ) ) ) } ) ) )
291 4 290 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 ) ) ) } ) )
292 15 291 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 ) ) ) } )
293 156 ffnd 
 |-  ( ph -> ( T oF x. X ) Fn A )
294 fnresdm 
 |-  ( ( T oF x. X ) Fn A -> ( ( T oF x. X ) |` A ) = ( T oF x. X ) )
295 293 294 syl 
 |-  ( ph -> ( ( T oF x. X ) |` A ) = ( T oF x. X ) )
296 295 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( T oF x. X ) |` A ) ) = ( CCfld gsum ( T oF x. X ) ) )
297 296 12 oveq12d 
 |-  ( ph -> ( ( CCfld gsum ( ( T oF x. X ) |` A ) ) / ( CCfld gsum ( T |` A ) ) ) = ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) )
298 9 261 4 4 155 offn 
 |-  ( ph -> ( T oF x. ( F o. X ) ) Fn A )
299 fnresdm 
 |-  ( ( T oF x. ( F o. X ) ) Fn A -> ( ( T oF x. ( F o. X ) ) |` A ) = ( T oF x. ( F o. X ) ) )
300 298 299 syl 
 |-  ( ph -> ( ( T oF x. ( F o. X ) ) |` A ) = ( T oF x. ( F o. X ) ) )
301 300 oveq2d 
 |-  ( ph -> ( CCfld gsum ( ( T oF x. ( F o. X ) ) |` A ) ) = ( CCfld gsum ( T oF x. ( F o. X ) ) ) )
302 301 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 ) ) )
303 302 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 ) ) ) )
304 303 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 ) ) } )
305 292 297 304 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 ) ) } )
306 fveq2 
 |-  ( w = ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) -> ( F ` w ) = ( F ` ( ( CCfld gsum ( T oF x. X ) ) / ( CCfld gsum T ) ) ) )
307 306 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 ) ) ) )
308 307 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 ) ) ) )
309 305 308 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 ) ) ) )