MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jensen Unicode version

Theorem jensen 20299
Description: Jensen's inequality, a finite extension of the definition of convexity (the last hypothesis). (Contributed by Mario Carneiro, 21-Jun-2015.)
Hypotheses
Ref Expression
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  <  (fld  gsumg  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
Ref Expression
jensen  |-  ( ph  ->  ( ( (fld  gsumg  ( T  o F  x.  X ) )  /  (fld 
gsumg  T ) )  e.  D  /\  ( F `
 ( (fld  gsumg  ( T  o F  x.  X ) )  /  (fld 
gsumg  T ) ) )  <_  ( (fld  gsumg  ( T  o F  x.  ( F  o.  X ) ) )  /  (fld 
gsumg  T ) ) ) )
Distinct variable groups:    a, b,
t, x, y, A    D, a, b, t, x, y    ph, a, b, t, x, y    F, a, b, t, x, y    T, a, b, t, x, y    X, a, b, t, x, y

Proof of Theorem jensen
Dummy variables  c 
k  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 remulcl 8838 . . . . . . . . 9  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  x.  y
)  e.  RR )
21adantl 452 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  x.  y
)  e.  RR )
3 jensen.5 . . . . . . . . 9  |-  ( ph  ->  T : A --> ( 0 [,)  +oo ) )
4 elrege0 10762 . . . . . . . . . . 11  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
54simplbi 446 . . . . . . . . . 10  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  RR )
65ssriv 3197 . . . . . . . . 9  |-  ( 0 [,)  +oo )  C_  RR
7 fss 5413 . . . . . . . . 9  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  T : A
--> RR )
83, 6, 7sylancl 643 . . . . . . . 8  |-  ( ph  ->  T : A --> RR )
9 jensen.6 . . . . . . . . 9  |-  ( ph  ->  X : A --> D )
10 jensen.1 . . . . . . . . 9  |-  ( ph  ->  D  C_  RR )
11 fss 5413 . . . . . . . . 9  |-  ( ( X : A --> D  /\  D  C_  RR )  ->  X : A --> RR )
129, 10, 11syl2anc 642 . . . . . . . 8  |-  ( ph  ->  X : A --> RR )
13 jensen.4 . . . . . . . 8  |-  ( ph  ->  A  e.  Fin )
14 inidm 3391 . . . . . . . 8  |-  ( A  i^i  A )  =  A
152, 8, 12, 13, 13, 14off 6109 . . . . . . 7  |-  ( ph  ->  ( T  o F  x.  X ) : A --> RR )
16 ffn 5405 . . . . . . 7  |-  ( ( T  o F  x.  X ) : A --> RR  ->  ( T  o F  x.  X )  Fn  A )
1715, 16syl 15 . . . . . 6  |-  ( ph  ->  ( T  o F  x.  X )  Fn  A )
18 fnresdm 5369 . . . . . 6  |-  ( ( T  o F  x.  X )  Fn  A  ->  ( ( T  o F  x.  X )  |`  A )  =  ( T  o F  x.  X ) )
1917, 18syl 15 . . . . 5  |-  ( ph  ->  ( ( T  o F  x.  X )  |`  A )  =  ( T  o F  x.  X ) )
2019oveq2d 5890 . . . 4  |-  ( ph  ->  (fld 
gsumg  ( ( T  o F  x.  X )  |`  A ) )  =  (fld 
gsumg  ( T  o F  x.  X ) ) )
21 ffn 5405 . . . . . . 7  |-  ( T : A --> ( 0 [,)  +oo )  ->  T  Fn  A )
223, 21syl 15 . . . . . 6  |-  ( ph  ->  T  Fn  A )
23 fnresdm 5369 . . . . . 6  |-  ( T  Fn  A  ->  ( T  |`  A )  =  T )
2422, 23syl 15 . . . . 5  |-  ( ph  ->  ( T  |`  A )  =  T )
2524oveq2d 5890 . . . 4  |-  ( ph  ->  (fld 
gsumg  ( T  |`  A ) )  =  (fld  gsumg  T ) )
2620, 25oveq12d 5892 . . 3  |-  ( ph  ->  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  =  ( (fld 
gsumg  ( T  o F  x.  X ) )  / 
(fld  gsumg  T ) ) )
27 jensen.7 . . . . . . 7  |-  ( ph  ->  0  <  (fld  gsumg  T ) )
2827, 25breqtrrd 4065 . . . . . 6  |-  ( ph  ->  0  <  (fld  gsumg  ( T  |`  A ) ) )
29 ssid 3210 . . . . . 6  |-  A  C_  A
3028, 29jctil 523 . . . . 5  |-  ( ph  ->  ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
31 sseq1 3212 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( a 
C_  A  <->  (/)  C_  A
) )
32 reseq2 4966 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( T  |`  a )  =  ( T  |`  (/) ) )
33 res0 4975 . . . . . . . . . . . . . 14  |-  ( T  |`  (/) )  =  (/)
3432, 33syl6eq 2344 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( T  |`  a )  =  (/) )
3534oveq2d 5890 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  (/) ) )
36 cnfld0 16414 . . . . . . . . . . . . 13  |-  0  =  ( 0g ` fld )
3736gsum0 14473 . . . . . . . . . . . 12  |-  (fld  gsumg  (/) )  =  0
3835, 37syl6eq 2344 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  0 )
3938breq2d 4051 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( 0  <  (fld 
gsumg  ( T  |`  a ) )  <->  0  <  0
) )
4031, 39anbi12d 691 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  <->  ( (/)  C_  A  /\  0  <  0
) ) )
41 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( ( T  o F  x.  X )  |`  a
)  =  ( ( T  o F  x.  X )  |`  (/) ) )
4241oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  (/) ) ) )
4342, 38oveq12d 5892 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  =  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
) )
44 reseq2 4966 . . . . . . . . . . . . . 14  |-  ( a  =  (/)  ->  ( ( T  o F  x.  ( F  o.  X
) )  |`  a
)  =  ( ( T  o F  x.  ( F  o.  X
) )  |`  (/) ) )
4544oveq2d 5890 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) ) )
4645, 38oveq12d 5892 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X
) )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  =  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) )
4746breq2d 4051 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  ( ( F `  w )  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) ) )
4847rabbidv 2793 . . . . . . . . . 10  |-  ( a  =  (/)  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
4943, 48eleq12d 2364 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) )
5040, 49imbi12d 311 . . . . . . . 8  |-  ( a  =  (/)  ->  ( ( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( (/)  C_  A  /\  0  <  0
)  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) ) )
5150imbi2d 307 . . . . . . 7  |-  ( a  =  (/)  ->  ( (
ph  ->  ( ( a 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( (/)  C_  A  /\  0  <  0 )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) ) ) )
52 sseq1 3212 . . . . . . . . . 10  |-  ( a  =  k  ->  (
a  C_  A  <->  k  C_  A ) )
53 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  k  ->  ( T  |`  a )  =  ( T  |`  k
) )
5453oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  k  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  k ) ) )
5554breq2d 4051 . . . . . . . . . 10  |-  ( a  =  k  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  k ) ) ) )
5652, 55anbi12d 691 . . . . . . . . 9  |-  ( a  =  k  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( k  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  k )
) ) ) )
57 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  k  ->  (
( T  o F  x.  X )  |`  a )  =  ( ( T  o F  x.  X )  |`  k ) )
5857oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) ) )
5958, 54oveq12d 5892 . . . . . . . . . 10  |-  ( a  =  k  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
60 reseq2 4966 . . . . . . . . . . . . . 14  |-  ( a  =  k  ->  (
( T  o F  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )
6160oveq2d 5890 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) ) )
6261, 54oveq12d 5892 . . . . . . . . . . . 12  |-  ( a  =  k  ->  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
6362breq2d 4051 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
6463rabbidv 2793 . . . . . . . . . 10  |-  ( a  =  k  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )
6559, 64eleq12d 2364 . . . . . . . . 9  |-  ( a  =  k  ->  (
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )
6656, 65imbi12d 311 . . . . . . . 8  |-  ( a  =  k  ->  (
( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) )
6766imbi2d 307 . . . . . . 7  |-  ( a  =  k  ->  (
( ph  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) ) )
68 sseq1 3212 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  ( a  C_  A 
<->  ( k  u.  {
c } )  C_  A ) )
69 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  ( k  u. 
{ c } )  ->  ( T  |`  a )  =  ( T  |`  ( k  u.  { c } ) ) )
7069oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( T  |`  a ) )  =  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )
7170breq2d 4051 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  ( 0  < 
(fld  gsumg  ( T  |`  a )
)  <->  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
7268, 71anbi12d 691 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( a 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  <->  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
73 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  o F  x.  X
)  |`  a )  =  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )
7473oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) ) )
7574, 70oveq12d 5892 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
76 reseq2 4966 . . . . . . . . . . . . . 14  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  o F  x.  ( F  o.  X )
)  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )
7776oveq2d 5890 . . . . . . . . . . . . 13  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) ) )
7877, 70oveq12d 5892 . . . . . . . . . . . 12  |-  ( a  =  ( k  u. 
{ c } )  ->  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
7978breq2d 4051 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( F `
 w )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
8079rabbidv 2793 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  { w  e.  D  |  ( F `
 w )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } )
8175, 80eleq12d 2364 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( (fld  gsumg  ( ( T  o F  x.  X )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  e. 
{ w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
8272, 81imbi12d 311 . . . . . . . 8  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( ( k  u.  { c } )  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) ) )
8382imbi2d 307 . . . . . . 7  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( ph  ->  ( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) ) ) )
84 sseq1 3212 . . . . . . . . . 10  |-  ( a  =  A  ->  (
a  C_  A  <->  A  C_  A
) )
85 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  A  ->  ( T  |`  a )  =  ( T  |`  A ) )
8685oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  A  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  A ) ) )
8786breq2d 4051 . . . . . . . . . 10  |-  ( a  =  A  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
8884, 87anbi12d 691 . . . . . . . . 9  |-  ( a  =  A  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( A  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  A )
) ) ) )
89 reseq2 4966 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (
( T  o F  x.  X )  |`  a )  =  ( ( T  o F  x.  X )  |`  A ) )
9089oveq2d 5890 . . . . . . . . . . 11  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  A ) ) )
9190, 86oveq12d 5892 . . . . . . . . . 10  |-  ( a  =  A  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) )
92 reseq2 4966 . . . . . . . . . . . . . 14  |-  ( a  =  A  ->  (
( T  o F  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )
9392oveq2d 5890 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) ) )
9493, 86oveq12d 5892 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) )
9594breq2d 4051 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) ) )
9695rabbidv 2793 . . . . . . . . . 10  |-  ( a  =  A  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } )
9791, 96eleq12d 2364 . . . . . . . . 9  |-  ( a  =  A  ->  (
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) )
9888, 97imbi12d 311 . . . . . . . 8  |-  ( a  =  A  ->  (
( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) ) )
9998imbi2d 307 . . . . . . 7  |-  ( a  =  A  ->  (
( ph  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) ) ) )
100 0re 8854 . . . . . . . . . . 11  |-  0  e.  RR
101100ltnri 8945 . . . . . . . . . 10  |-  -.  0  <  0
102101pm2.21i 123 . . . . . . . . 9  |-  ( 0  <  0  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
103102adantl 452 . . . . . . . 8  |-  ( (
(/)  C_  A  /\  0  <  0 )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
104103a1i 10 . . . . . . 7  |-  ( ph  ->  ( ( (/)  C_  A  /\  0  <  0
)  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) )
105 impexp 433 . . . . . . . . . . . . 13  |-  ( ( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )  <-> 
( k  C_  A  ->  ( 0  <  (fld  gsumg  ( T  |`  k
) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) )
106 ssun1 3351 . . . . . . . . . . . . . . 15  |-  k  C_  ( k  u.  {
c } )
107 simprl 732 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } ) 
C_  A )
108106, 107syl5ss 3203 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  C_  A )
109 simpr 447 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  <  (fld 
gsumg  ( T  |`  k ) ) )  ->  0  <  (fld 
gsumg  ( T  |`  k ) ) )
11010ad3antrrr 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  D  C_  RR )
111 jensen.2 . . . . . . . . . . . . . . . . . . . 20  |-  ( ph  ->  F : D --> RR )
112111ad3antrrr 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  F : D
--> RR )
113 simplll 734 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ph )
114 jensen.3 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
ph  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
115113, 114sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
116113, 13syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  A  e.  Fin )
117113, 3syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  T : A
--> ( 0 [,)  +oo ) )
118113, 9syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  X : A
--> D )
11927ad3antrrr 710 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  0  <  (fld  gsumg  T ) )
120 jensen.8 . . . . . . . . . . . . . . . . . . . 20  |-  ( (
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
) ) ) )
121113, 120sylan 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( 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
) ) ) )
122 simpllr 735 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  -.  c  e.  k )
123107adantr 451 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( k  u.  { c } ) 
C_  A )
124 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  (fld  gsumg  ( T  |`  k
) )  =  (fld  gsumg  ( T  |`  k ) )
125 eqid 2296 . . . . . . . . . . . . . . . . . . 19  |-  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) )  =  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) )
126 cnrng 16412 . . . . . . . . . . . . . . . . . . . . . . . 24  |-fld  e.  Ring
127 rngcmn 15387 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  (fld  e.  Ring  ->fld  e. CMnd )
128126, 127mp1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->fld  e. CMnd )
12913ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  A  e.  Fin )
130 ssfi 7099 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  Fin  /\  k  C_  A )  -> 
k  e.  Fin )
131129, 108, 130syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  e.  Fin )
132 rege0subm 16444 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( 0 [,)  +oo )  e.  (SubMnd ` fld )
133132a1i 10 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( 0 [,)  +oo )  e.  (SubMnd ` fld ) )
1343ad2antrr 706 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  T : A
--> ( 0 [,)  +oo ) )
135 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  k  C_  A )  ->  ( T  |`  k ) : k --> ( 0 [,) 
+oo ) )
136134, 108, 135syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( T  |`  k ) : k --> ( 0 [,)  +oo ) )
137131, 136fisuppfi 14466 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( `' ( T  |`  k )
" ( _V  \  { 0 } ) )  e.  Fin )
13836, 128, 131, 133, 136, 137gsumsubmcl 15217 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  ( 0 [,)  +oo )
)
139 elrege0 10762 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,)  +oo ) 
<->  ( (fld 
gsumg  ( T  |`  k ) )  e.  RR  /\  0  <_  (fld 
gsumg  ( T  |`  k ) ) ) )
140139simplbi 446 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,)  +oo )  ->  (fld 
gsumg  ( T  |`  k ) )  e.  RR )
141138, 140syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR )
142141adantr 451 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR )
143 simprl 732 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  0  <  (fld  gsumg  ( T  |`  k ) ) )
144142, 143elrpd 10404 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR+ )
145 simprr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )
146 fveq2 5541 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( w  =  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  ->  ( F `  w )  =  ( F `  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
147146breq1d 4049 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  <->  ( F `  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
148147elrab 2936 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) }  <->  ( (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D  /\  ( F `  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
149145, 148sylib 188 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D  /\  ( F `  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
150149simpld 445 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D
)
151149simprd 449 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( F `  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
152110, 112, 115, 116, 117, 118, 119, 121, 122, 123, 124, 125, 144, 150, 151jensenlem2 20298 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (
(fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  D  /\  ( F `  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
153 fveq2 5541 . . . . . . . . . . . . . . . . . . . 20  |-  ( w  =  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  ->  ( F `  w )  =  ( F `  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) ) )
154153breq1d 4049 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  ->  ( ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  <->  ( F `  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  <_  (
(fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
155154elrab 2936 . . . . . . . . . . . . . . . . . 18  |-  ( ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) }  <->  ( (
(fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  D  /\  ( F `  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
156152, 155sylibr 203 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  (
0  <  (fld  gsumg  ( T  |`  k
) )  /\  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } )
157156expr 598 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  <  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) }  ->  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
158109, 157embantd 50 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  <  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( 0  <  (fld  gsumg  ( T  |`  k
) )  ->  (
(fld  gsumg  ( ( T  o F  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
159 cnfldbas 16399 . . . . . . . . . . . . . . . . . . . . . 22  |-  CC  =  ( Base ` fld )
160 rngmnd 15366 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (fld  e.  Ring  ->fld  e.  Mnd )
161126, 160mp1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->fld  e.  Mnd )
162 ssfi 7099 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( A  e.  Fin  /\  ( k  u.  {
c } )  C_  A )  ->  (
k  u.  { c } )  e.  Fin )
163129, 107, 162syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } )  e.  Fin )
164163adantr 451 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
k  u.  { c } )  e.  Fin )
165 ssun2 3352 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  { c }  C_  ( k  u.  { c } )
166 vex 2804 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  c  e. 
_V
167166snid 3680 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  c  e. 
{ c }
168165, 167sselii 3190 . . . . . . . . . . . . . . . . . . . . . . 23  |-  c  e.  ( k  u.  {
c } )
169168a1i 10 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  c  e.  ( k  u.  {
c } ) )
170 ax-resscn 8810 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  RR  C_  CC
171 fss 5413 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( T  o F  x.  X ) : A --> RR  /\  RR  C_  CC )  ->  ( T  o F  x.  X
) : A --> CC )
17215, 170, 171sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( T  o F  x.  X ) : A --> CC )
173172ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T  o F  x.  X
) : A --> CC )
174107adantr 451 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
k  u.  { c } )  C_  A
)
175 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( T  o F  x.  X ) : A --> CC  /\  (
k  u.  { c } )  C_  A
)  ->  ( ( T  o F  x.  X
)  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
176173, 174, 175syl2anc 642 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) : ( k  u. 
{ c } ) --> CC )
1773ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T : A --> ( 0 [,) 
+oo ) )
178129adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  A  e.  Fin )
179 fex 5765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  A  e.  Fin )  ->  T  e.  _V )
180177, 178, 179syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T  e.  _V )
1819ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X : A --> D )
182 fex 5765 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( X : A --> D  /\  A  e.  Fin )  ->  X  e.  _V )
183181, 178, 182syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X  e.  _V )
184 offres 6108 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T  e.  _V  /\  X  e.  _V )  ->  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) )  =  ( ( T  |`  ( k  u.  {
c } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) )
185180, 183, 184syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  o F  x.  X )  |`  ( k  u.  {
c } ) )  =  ( ( T  |`  ( k  u.  {
c } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) )
186185cnveqd 4873 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  `' ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) )  =  `' ( ( T  |`  ( k  u.  { c } ) )  o F  x.  ( X  |`  ( k  u.  { c } ) ) ) )
187186imaeq1d 5027 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( `' ( ( T  o F  x.  X
)  |`  ( k  u. 
{ c } ) ) " ( _V 
\  { 0 } ) )  =  ( `' ( ( T  |`  ( k  u.  {
c } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) " ( _V  \  { 0 } ) ) )
1886, 170sstri 3201 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 0 [,)  +oo )  C_  CC
189 fss 5413 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  CC )  ->  T : A
--> CC )
190177, 188, 189sylancl 643 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T : A --> CC )
191 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> CC  /\  ( k  u.  {
c } )  C_  A )  ->  ( T  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
192190, 174, 191syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
193 eldifi 3311 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  ( k  u.  {
c } ) )
194193adantl 452 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  ( ( k  u. 
{ c } ) 
\  { c } ) )  ->  x  e.  ( k  u.  {
c } ) )
195 fvres 5558 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 x )  =  ( T `  x
) )
196194, 195syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  ( ( k  u. 
{ c } ) 
\  { c } ) )  ->  (
( T  |`  (
k  u.  { c } ) ) `  x )  =  ( T `  x ) )
197 difun2 3546 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( k  u.  { c } )  \  {
c } )  =  ( k  \  {
c } )
198 difss 3316 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( k 
\  { c } )  C_  k
199197, 198eqsstri 3221 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  u.  { c } )  \  {
c } )  C_  k
200199sseli 3189 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  k )
201 simpr 447 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  0  =  (fld 
gsumg  ( T  |`  k ) ) )
202108adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  k  C_  A )
203177, 202feqresmpt 5592 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T  |`  k )  =  ( x  e.  k 
|->  ( T `  x
) ) )
204203oveq2d 5890 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  =  (fld  gsumg  ( x  e.  k  |->  ( T `
 x ) ) ) )
205131adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  k  e.  Fin )
206202sselda 3193 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  x  e.  A )
207 ffvelrn 5679 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  x  e.  A )  ->  ( T `  x )  e.  ( 0 [,)  +oo ) )
208177, 207sylan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  A )  ->  ( T `  x )  e.  ( 0 [,)  +oo ) )
209206, 208syldan 456 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  ( T `  x )  e.  ( 0 [,)  +oo ) )
210188, 209sseldi 3191 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  ( T `  x )  e.  CC )
211205, 210gsumfsum 16455 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( x  e.  k 
|->  ( T `  x
) ) )  = 
sum_ x  e.  k 
( T `  x
) )
212201, 204, 2113eqtrrd 2333 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  sum_ x  e.  k  ( T `  x )  =  0 )
213 elrege0 10762 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( T `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( T `  x )  e.  RR  /\  0  <_ 
( T `  x
) ) )
214209, 213sylib 188 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  (
( T `  x
)  e.  RR  /\  0  <_  ( T `  x ) ) )
215214simpld 445 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  ( T `  x )  e.  RR )
216214simprd 449 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  0  <_  ( T `  x
) )
217205, 215, 216fsum00 12272 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( sum_ x  e.  k  ( T `  x )  =  0  <->  A. x  e.  k  ( T `  x )  =  0 ) )
218212, 217mpbid 201 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  A. x  e.  k  ( T `  x )  =  0 )
219218r19.21bi 2654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  k )  ->  ( T `  x )  =  0 )
220200, 219sylan2 460 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  ( ( k  u. 
{ c } ) 
\  { c } ) )  ->  ( T `  x )  =  0 )
221196, 220eqtrd 2328 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  ( ( k  u. 
{ c } ) 
\  { c } ) )  ->  (
( T  |`  (
k  u.  { c } ) ) `  x )  =  0 )
222192, 221suppss 5674 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( `' ( T  |`  ( k  u.  {
c } ) )
" ( _V  \  { 0 } ) )  C_  { c } )
223 mul02 9006 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
224223adantl 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\ 
-.  c  e.  k )  /\  ( ( k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  /\  x  e.  CC )  ->  (
0  x.  x )  =  0 )
22510ad3antrrr 710 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  D  C_  RR )
226225, 170syl6ss 3204 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  D  C_  CC )
227 fss 5413 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( X : A --> D  /\  D  C_  CC )  ->  X : A --> CC )
228181, 226, 227syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X : A --> CC )
229 fssres 5424 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X : A --> CC  /\  ( k  u.  {
c } )  C_  A )  ->  ( X  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
230228, 174, 229syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( X  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
231222, 224, 192, 230, 164suppssof1 6135 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( `' ( ( T  |`  ( k  u.  {
c } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) " ( _V  \  { 0 } ) )  C_  { c } )
232187, 231eqsstrd 3225 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( `' ( ( T  o F  x.  X
)  |`  ( k  u. 
{ c } ) ) " ( _V 
\  { 0 } ) )  C_  { c } )
233159, 36, 161, 164, 169, 176, 232gsumpt 15238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  =  ( ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) `
 c ) )
234 fvres 5558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( ( T  o F  x.  X )  |`  (
k  u.  { c } ) ) `  c )  =  ( ( T  o F  x.  X ) `  c ) )
235169, 234syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) `
 c )  =  ( ( T  o F  x.  X ) `  c ) )
236177, 21syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T  Fn  A )
237 ffn 5405 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( X : A --> D  ->  X  Fn  A )
238181, 237syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X  Fn  A )
239174, 169sseldd 3194 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  c  e.  A )
240 fnfvof 6106 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T  Fn  A  /\  X  Fn  A
)  /\  ( A  e.  Fin  /\  c  e.  A ) )  -> 
( ( T  o F  x.  X ) `  c )  =  ( ( T `  c
)  x.  ( X `
 c ) ) )
241236, 238, 178, 239, 240syl22anc 1183 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  o F  x.  X ) `  c )  =  ( ( T `  c
)  x.  ( X `
 c ) ) )
242233, 235, 2413eqtrd 2332 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )  =  ( ( T `  c )  x.  ( X `  c ) ) )
243159, 36, 161, 164, 169, 192, 222gsumpt 15238 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) )  =  ( ( T  |`  ( k  u.  {
c } ) ) `
 c ) )
244 fvres 5558 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 c )  =  ( T `  c
) )
245169, 244syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  |`  (
k  u.  { c } ) ) `  c )  =  ( T `  c ) )
246243, 245eqtrd 2328 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) )  =  ( T `  c ) )
247242, 246oveq12d 5892 . . . . . . . . . . . . . . . . . . 19  |-  (