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

Theorem jensen 23519
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.)
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  oF  x.  X ) )  /  (fld 
gsumg  T ) )  e.  D  /\  ( F `
 ( (fld  gsumg  ( T  oF  x.  X ) )  /  (fld 
gsumg  T ) ) )  <_  ( (fld  gsumg  ( T  oF  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 jensen.7 . . . . . 6  |-  ( ph  ->  0  <  (fld  gsumg  T ) )
2 jensen.5 . . . . . . . . 9  |-  ( ph  ->  T : A --> ( 0 [,) +oo ) )
3 ffn 5713 . . . . . . . . 9  |-  ( T : A --> ( 0 [,) +oo )  ->  T  Fn  A )
42, 3syl 16 . . . . . . . 8  |-  ( ph  ->  T  Fn  A )
5 fnresdm 5672 . . . . . . . 8  |-  ( T  Fn  A  ->  ( T  |`  A )  =  T )
64, 5syl 16 . . . . . . 7  |-  ( ph  ->  ( T  |`  A )  =  T )
76oveq2d 6286 . . . . . 6  |-  ( ph  ->  (fld 
gsumg  ( T  |`  A ) )  =  (fld  gsumg  T ) )
81, 7breqtrrd 4465 . . . . 5  |-  ( ph  ->  0  <  (fld  gsumg  ( T  |`  A ) ) )
9 ssid 3508 . . . . 5  |-  A  C_  A
108, 9jctil 535 . . . 4  |-  ( ph  ->  ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
11 jensen.4 . . . . 5  |-  ( ph  ->  A  e.  Fin )
12 sseq1 3510 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( a 
C_  A  <->  (/)  C_  A
) )
13 reseq2 5257 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( T  |`  a )  =  ( T  |`  (/) ) )
14 res0 5266 . . . . . . . . . . . . 13  |-  ( T  |`  (/) )  =  (/)
1513, 14syl6eq 2511 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( T  |`  a )  =  (/) )
1615oveq2d 6286 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  (/) ) )
17 cnfld0 18640 . . . . . . . . . . . 12  |-  0  =  ( 0g ` fld )
1817gsum0 16107 . . . . . . . . . . 11  |-  (fld  gsumg  (/) )  =  0
1916, 18syl6eq 2511 . . . . . . . . . 10  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  0 )
2019breq2d 4451 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( 0  <  (fld 
gsumg  ( T  |`  a ) )  <->  0  <  0
) )
2112, 20anbi12d 708 . . . . . . . 8  |-  ( a  =  (/)  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  <->  ( (/)  C_  A  /\  0  <  0
) ) )
22 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  ( ( T  oF  x.  X )  |`  a
)  =  ( ( T  oF  x.  X )  |`  (/) ) )
2322oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  X )  |`  (/) ) ) )
2423, 19oveq12d 6288 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  =  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
) )
25 reseq2 5257 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( ( T  oF  x.  ( F  o.  X
) )  |`  a
)  =  ( ( T  oF  x.  ( F  o.  X
) )  |`  (/) ) )
2625oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) ) )
2726, 19oveq12d 6288 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X
) )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  =  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) )
2827breq2d 4451 . . . . . . . . . 10  |-  ( a  =  (/)  ->  ( ( F `  w )  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) ) )
2928rabbidv 3098 . . . . . . . . 9  |-  ( a  =  (/)  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
3024, 29eleq12d 2536 . . . . . . . 8  |-  ( a  =  (/)  ->  ( ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) )
3121, 30imbi12d 318 . . . . . . 7  |-  ( a  =  (/)  ->  ( ( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( (/)  C_  A  /\  0  <  0
)  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) ) )
3231imbi2d 314 . . . . . 6  |-  ( a  =  (/)  ->  ( (
ph  ->  ( ( a 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( (/)  C_  A  /\  0  <  0 )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) ) ) )
33 sseq1 3510 . . . . . . . . 9  |-  ( a  =  k  ->  (
a  C_  A  <->  k  C_  A ) )
34 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  k  ->  ( T  |`  a )  =  ( T  |`  k
) )
3534oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  k  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  k ) ) )
3635breq2d 4451 . . . . . . . . 9  |-  ( a  =  k  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  k ) ) ) )
3733, 36anbi12d 708 . . . . . . . 8  |-  ( a  =  k  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( k  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  k )
) ) ) )
38 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( T  oF  x.  X )  |`  a )  =  ( ( T  oF  x.  X )  |`  k ) )
3938oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) ) )
4039, 35oveq12d 6288 . . . . . . . . 9  |-  ( a  =  k  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
41 reseq2 5257 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( T  oF  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )
4241oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) ) )
4342, 35oveq12d 6288 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
4443breq2d 4451 . . . . . . . . . 10  |-  ( a  =  k  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
4544rabbidv 3098 . . . . . . . . 9  |-  ( a  =  k  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )
4640, 45eleq12d 2536 . . . . . . . 8  |-  ( a  =  k  ->  (
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )
4737, 46imbi12d 318 . . . . . . 7  |-  ( a  =  k  ->  (
( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) )
4847imbi2d 314 . . . . . 6  |-  ( a  =  k  ->  (
( ph  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) ) )
49 sseq1 3510 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( a  C_  A 
<->  ( k  u.  {
c } )  C_  A ) )
50 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( T  |`  a )  =  ( T  |`  ( k  u.  { c } ) ) )
5150oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( T  |`  a ) )  =  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )
5251breq2d 4451 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( 0  < 
(fld  gsumg  ( T  |`  a )
)  <->  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
5349, 52anbi12d 708 . . . . . . . 8  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( a 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  <->  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
54 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  oF  x.  X
)  |`  a )  =  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )
5554oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) ) )
5655, 51oveq12d 6288 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
57 reseq2 5257 . . . . . . . . . . . . 13  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  oF  x.  ( F  o.  X )
)  |`  a )  =  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )
5857oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) ) )
5958, 51oveq12d 6288 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
6059breq2d 4451 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( F `
 w )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
6160rabbidv 3098 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  { w  e.  D  |  ( F `
 w )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } )
6256, 61eleq12d 2536 . . . . . . . 8  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( (fld  gsumg  ( ( T  oF  x.  X )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  e. 
{ w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
6353, 62imbi12d 318 . . . . . . 7  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( ( k  u.  { c } )  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) ) )
6463imbi2d 314 . . . . . 6  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( ph  ->  ( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  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  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) ) ) )
65 sseq1 3510 . . . . . . . . 9  |-  ( a  =  A  ->  (
a  C_  A  <->  A  C_  A
) )
66 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( T  |`  a )  =  ( T  |`  A ) )
6766oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  A  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  A ) ) )
6867breq2d 4451 . . . . . . . . 9  |-  ( a  =  A  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
6965, 68anbi12d 708 . . . . . . . 8  |-  ( a  =  A  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( A  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  A )
) ) ) )
70 reseq2 5257 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
( T  oF  x.  X )  |`  a )  =  ( ( T  oF  x.  X )  |`  A ) )
7170oveq2d 6286 . . . . . . . . . 10  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  X )  |`  A ) ) )
7271, 67oveq12d 6288 . . . . . . . . 9  |-  ( a  =  A  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) )
73 reseq2 5257 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  (
( T  oF  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )
7473oveq2d 6286 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) ) )
7574, 67oveq12d 6288 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  =  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) )
7675breq2d 4451 . . . . . . . . . 10  |-  ( a  =  A  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  <->  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) ) )
7776rabbidv 3098 . . . . . . . . 9  |-  ( a  =  A  ->  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  =  { w  e.  D  |  ( F `  w )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } )
7872, 77eleq12d 2536 . . . . . . . 8  |-  ( a  =  A  ->  (
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) }  <->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) )
7969, 78imbi12d 318 . . . . . . 7  |-  ( a  =  A  ->  (
( ( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } )  <-> 
( ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) ) )
8079imbi2d 314 . . . . . 6  |-  ( a  =  A  ->  (
( ph  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  a ) )  / 
(fld  gsumg  ( T  |`  a )
) ) } ) )  <->  ( ph  ->  ( ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  A ) )  / 
(fld  gsumg  ( T  |`  A )
) ) } ) ) ) )
81 0re 9585 . . . . . . . . . 10  |-  0  e.  RR
8281ltnri 9682 . . . . . . . . 9  |-  -.  0  <  0
8382pm2.21i 131 . . . . . . . 8  |-  ( 0  <  0  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
8483adantl 464 . . . . . . 7  |-  ( (
(/)  C_  A  /\  0  <  0 )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } )
8584a1i 11 . . . . . 6  |-  ( ph  ->  ( ( (/)  C_  A  /\  0  <  0
)  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (/) ) )  /  0
)  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  (/) ) )  /  0
) } ) )
86 impexp 444 . . . . . . . . . . . 12  |-  ( ( ( k  C_  A  /\  0  <  (fld  gsumg  ( T  |`  k
) ) )  -> 
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )  <-> 
( k  C_  A  ->  ( 0  <  (fld  gsumg  ( T  |`  k
) )  ->  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) ) )
87 simprl 754 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } ) 
C_  A )
8887unssad 3667 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  C_  A )
89 simpr 459 . . . . . . . . . . . . . . 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 ) ) )
90 jensen.1 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  D  C_  RR )
9190ad3antrrr 727 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  D  C_  RR )
92 jensen.2 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : D --> RR )
9392ad3antrrr 727 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  F : D
--> RR )
94 simplll 757 . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ph )
95 jensen.3 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
9694, 95sylan 469 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
9794, 11syl 16 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  A  e.  Fin )
9894, 2syl 16 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  T : A
--> ( 0 [,) +oo ) )
99 jensen.6 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X : A --> D )
10094, 99syl 16 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  X : A
--> D )
1011ad3antrrr 727 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  0  <  (fld  gsumg  T ) )
102 jensen.8 . . . . . . . . . . . . . . . . . . 19  |-  ( (
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
) ) ) )
10394, 102sylan 469 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  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
) ) ) )
104 simpllr 758 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  -.  c  e.  k )
10587adantr 463 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( k  u.  { c } ) 
C_  A )
106 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  (fld  gsumg  ( T  |`  k
) )  =  (fld  gsumg  ( T  |`  k ) )
107 eqid 2454 . . . . . . . . . . . . . . . . . 18  |-  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) )  =  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) )
108 cnring 18638 . . . . . . . . . . . . . . . . . . . . . . 23  |-fld  e.  Ring
109 ringcmn 17427 . . . . . . . . . . . . . . . . . . . . . . 23  |-  (fld  e.  Ring  ->fld  e. CMnd )
110108, 109mp1i 12 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->fld  e. CMnd )
11111ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  A  e.  Fin )
112 ssfi 7733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  Fin  /\  k  C_  A )  -> 
k  e.  Fin )
113111, 88, 112syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  e.  Fin )
114 rege0subm 18672 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( 0 [,) +oo )  e.  (SubMnd ` fld )
115114a1i 11 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( 0 [,) +oo )  e.  (SubMnd ` fld ) )
1162ad2antrr 723 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  T : A
--> ( 0 [,) +oo ) )
117116, 88fssresd 5734 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( T  |`  k ) : k --> ( 0 [,) +oo ) )
118 c0ex 9579 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  0  e.  _V
119118a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  0  e.  _V )
120117, 113, 119fdmfifsupp 7831 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( T  |`  k ) finSupp  0 )
12117, 110, 113, 115, 117, 120gsumsubmcl 17132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  ( 0 [,) +oo )
)
122 elrege0 11630 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,) +oo ) 
<->  ( (fld 
gsumg  ( T  |`  k ) )  e.  RR  /\  0  <_  (fld 
gsumg  ( T  |`  k ) ) ) )
123122simplbi 458 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,) +oo )  ->  (fld 
gsumg  ( T  |`  k ) )  e.  RR )
124121, 123syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR )
125124adantr 463 . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR )
126 simprl 754 . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  0  <  (fld  gsumg  ( T  |`  k ) ) )
127125, 126elrpd 11256 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR+ )
128 simprr 755 . . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )
129 fveq2 5848 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( w  =  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  ->  ( F `  w )  =  ( F `  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
130129breq1d 4449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( w  =  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  ->  (
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  <->  ( F `  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
131130elrab 3254 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) }  <->  ( (
(fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D  /\  ( F `  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
132128, 131sylib 196 . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (
(fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D  /\  ( F `  (
(fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) ) )
133132simpld 457 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D
)
134132simprd 461 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( F `  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )  <_ 
( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) )
13591, 93, 96, 97, 98, 100, 101, 103, 104, 105, 106, 107, 127, 133, 134jensenlem2 23518 . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (
(fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  D  /\  ( F `  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
136 fveq2 5848 . . . . . . . . . . . . . . . . . . 19  |-  ( w  =  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  ->  ( F `  w )  =  ( F `  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) ) )
137136breq1d 4449 . . . . . . . . . . . . . . . . . 18  |-  ( w  =  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  ->  ( ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  <->  ( F `  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  <_  (
(fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
138137elrab 3254 . . . . . . . . . . . . . . . . 17  |-  ( ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) }  <->  ( (
(fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  D  /\  ( F `  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  (
k  u.  { c } ) ) )  /  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) ) )
139135, 138sylibr 212 . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } ) )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } )
140139expr 613 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  <  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( (fld 
gsumg  ( ( T  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) }  ->  ( (fld 
gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
14189, 140embantd 54 . . . . . . . . . . . . . 14  |-  ( ( ( ( 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  oF  x.  X )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  {
w  e.  D  | 
( F `  w
)  <_  ( (fld  gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  k ) )  / 
(fld  gsumg  ( T  |`  k )
) ) } )  ->  ( (fld  gsumg  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  e.  { w  e.  D  |  ( F `  w )  <_  ( (fld 
gsumg  ( ( T  oF  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) } ) )
142 cnfldbas 18622 . . . . . . . . . . . . . . . . . . . . 21  |-  CC  =  ( Base ` fld )
143 ringmnd 17405 . . . . . . . . . . . . . . . . . . . . . 22  |-  (fld  e.  Ring  ->fld  e.  Mnd )
144108, 143mp1i 12 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->fld  e.  Mnd )
145 ssfi 7733 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  Fin  /\  ( k  u.  {
c } )  C_  A )  ->  (
k  u.  { c } )  e.  Fin )
146111, 87, 145syl2anc 659 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } )  e.  Fin )
147146adantr 463 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 )
148 ssun2 3654 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { c }  C_  ( k  u.  { c } )
149 ssnid 4045 . . . . . . . . . . . . . . . . . . . . . . 23  |-  c  e. 
{ c }
150148, 149sselii 3486 . . . . . . . . . . . . . . . . . . . . . 22  |-  c  e.  ( k  u.  {
c } )
151150a1i 11 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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 } ) )
152 remulcl 9566 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  x.  y
)  e.  RR )
153152adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  x.  y
)  e.  RR )
154 rge0ssre 11631 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 [,) +oo )  C_  RR
155 fss 5721 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  RR )  ->  T : A --> RR )
1562, 154, 155sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  T : A --> RR )
15799, 90fssd 5722 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  X : A --> RR )
158 inidm 3693 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  A )  =  A
159153, 156, 157, 11, 11, 158off 6527 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( T  oF  x.  X ) : A --> RR )
160 ax-resscn 9538 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  RR  C_  CC
161 fss 5721 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( T  oF  x.  X ) : A --> RR  /\  RR  C_  CC )  ->  ( T  oF  x.  X
) : A --> CC )
162159, 160, 161sylancl 660 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( T  oF  x.  X ) : A --> CC )
163162ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T  oF  x.  X
) : A --> CC )
16487adantr 463 . . . . . . . . . . . . . . . . . . . . . 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 } )  C_  A
)
165163, 164fssresd 5734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) : ( k  u. 
{ c } ) --> CC )
1662ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( 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 ) )
167111adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  A  e.  Fin )
168 fex 6120 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T : A --> ( 0 [,) +oo )  /\  A  e.  Fin )  ->  T  e.  _V )
169166, 167, 168syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T  e.  _V )
17099ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X : A --> D )
171 fex 6120 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X : A --> D  /\  A  e.  Fin )  ->  X  e.  _V )
172170, 167, 171syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X  e.  _V )
173 offres 6768 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( T  e.  _V  /\  X  e.  _V )  ->  ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) )  =  ( ( T  |`  ( k  u.  {
c } ) )  oF  x.  ( X  |`  ( k  u. 
{ c } ) ) ) )
174169, 172, 173syl2anc 659 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  oF  x.  X )  |`  ( k  u.  {
c } ) )  =  ( ( T  |`  ( k  u.  {
c } ) )  oF  x.  ( X  |`  ( k  u. 
{ c } ) ) ) )
175174oveq1d 6285 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) supp  0 )  =  ( ( ( T  |`  ( k  u.  {
c } ) )  oF  x.  ( X  |`  ( k  u. 
{ c } ) ) ) supp  0 ) )
176154, 160sstri 3498 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 [,) +oo )  C_  CC
177 fss 5721 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> ( 0 [,) +oo )  /\  ( 0 [,) +oo )  C_  CC )  ->  T : A --> CC )
178166, 176, 177sylancl 660 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T : A --> CC )
179178, 164fssresd 5734 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) : ( k  u.  { c } ) --> CC )
180 eldifi 3612 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  ( k  u.  {
c } ) )
181180adantl 464 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )  ->  x  e.  ( k  u.  {
c } ) )
182 fvres 5862 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 x )  =  ( T `  x
) )
183181, 182syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 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 )  =  ( T `  x ) )
184 difun2 3895 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  u.  { c } )  \  {
c } )  =  ( k  \  {
c } )
185 difss 3617 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k 
\  { c } )  C_  k
186184, 185eqsstri 3519 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  u.  { c } )  \  {
c } )  C_  k
187186sseli 3485 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  k )
188 simpr 459 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) ) )
18988adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  k  C_  A )
190166, 189feqresmpt 5902 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( 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
) ) )
191190oveq2d 6286 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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 ) ) ) )
192113adantr 463 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  k  e.  Fin )
193189sselda 3489 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  x  e.  A )
194166ffvelrnda 6007 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ( 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 ) )
195193, 194syldan 468 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  ( 0 [,) +oo ) )
196176, 195sseldi 3487 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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.  CC )
197192, 196gsumfsum 18682 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( 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
) )
198188, 191, 1973eqtrrd 2500 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 )
199 elrege0 11630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( T `  x )  e.  ( 0 [,) +oo )  <->  ( ( T `
 x )  e.  RR  /\  0  <_ 
( T `  x
) ) )
200195, 199sylib 196 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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  /\  0  <_  ( T `  x ) ) )
201200simpld 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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 )
202200simprd 461 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ( 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
) )
203192, 201, 202fsum00 13697 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( 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 ) )
204198, 203mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( 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 )
205204r19.21bi 2823 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )  ->  ( T `  x )  =  0 )
206187, 205sylan2 472 . . . . . . . . . . . . . . . . . . . . . . . . 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 `  x )  =  0 )
207183, 206eqtrd 2495 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( 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 )
208179, 207suppss 6922 . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) supp  0
)  C_  { c } )
209 mul02 9747 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
210209adantl 464 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( 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 )
21190ad3antrrr 727 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  D  C_  RR )
212211, 160syl6ss 3501 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  D  C_  CC )
213170, 212fssd 5722 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X : A --> CC )
214213, 164fssresd 5734 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( 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 )
215118a1i 11 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  0  e.  _V )
216208, 210, 179, 214, 147, 215suppssof1 6925 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( 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 } ) )  oF  x.  ( X  |`  ( k  u. 
{ c } ) ) ) supp  0 ) 
C_  { c } )
217175, 216eqsstrd 3523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) supp  0 )  C_  { c } )
218142, 17, 144, 147, 151, 165, 217gsumpt 17187 . . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  =  ( ( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) `
 c ) )
219 fvres 5862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( ( T  oF  x.  X )  |`  (
k  u.  { c } ) ) `  c )  =  ( ( T  oF  x.  X ) `  c ) )
220151, 219syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( ( T  oF  x.  X )  |`  ( k  u.  {
c } ) ) `
 c )  =  ( ( T  oF  x.  X ) `  c ) )
221166, 3syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T  Fn  A )
222 ffn 5713 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X : A --> D  ->  X  Fn  A )
223170, 222syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X  Fn  A )
224164, 151sseldd 3490 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  c  e.  A )
225 fnfvof 6526 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T  Fn  A  /\  X  Fn  A
)  /\  ( A  e.  Fin  /\  c  e.  A ) )  -> 
( ( T  oF  x.  X ) `  c )  =  ( ( T `  c
)  x.  ( X `
 c ) ) )
226221, 223, 167, 224, 225syl22anc 1227 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( T  oF  x.  X ) `  c )  =  ( ( T `  c
)  x.  ( X `
 c ) ) )
227218, 220, 2263eqtrd 2499 . . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  =  ( ( T `  c )  x.  ( X `  c ) ) )
228142, 17, 144, 147, 151, 179, 208gsumpt 17187 . . . . . . . . . . . . . . . . . . . 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  |`  ( k  u.  {
c } ) ) `
 c ) )
229 fvres 5862 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 c )  =  ( T `  c
) )
230151, 229syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
231228, 230eqtrd 2495 . . . . . . . . . . . . . . . . . . 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  |`  (
k  u.  { c } ) ) )  =  ( T `  c ) )
232227, 231oveq12d 6288 . . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  =  ( ( ( T `  c
)  x.  ( X `
 c ) )  /  ( T `  c ) ) )
233213, 224ffvelrnd 6008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( X `  c )  e.  CC )
234178, 224ffvelrnd 6008 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T `  c )  e.  CC )
235 simplrr 760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( 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  u.  { c } ) ) ) )
236235, 231breqtrd 4463 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  0  <  ( T `  c
) )
237236gt0ne0d 10113 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  ( T `  c )  =/=  0 )
238233, 234, 237divcan3d 10321 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  (
( ( T `  c )  x.  ( X `  c )
)  /  ( T `
 c ) )  =  ( X `  c ) )
239232, 238eqtrd 2495 . . . . . . . . . . . . . . . . 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  oF  x.  X )  |`  ( k  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  =  ( X `
 c ) )
240170, 224ffvelrnd 6008 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  -.