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

Theorem jensen 20696
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 jensen.7 . . . . . 6  |-  ( ph  ->  0  <  (fld  gsumg  T ) )
2 jensen.5 . . . . . . . . 9  |-  ( ph  ->  T : A --> ( 0 [,)  +oo ) )
3 ffn 5533 . . . . . . . . 9  |-  ( T : A --> ( 0 [,)  +oo )  ->  T  Fn  A )
42, 3syl 16 . . . . . . . 8  |-  ( ph  ->  T  Fn  A )
5 fnresdm 5496 . . . . . . . 8  |-  ( T  Fn  A  ->  ( T  |`  A )  =  T )
64, 5syl 16 . . . . . . 7  |-  ( ph  ->  ( T  |`  A )  =  T )
76oveq2d 6038 . . . . . 6  |-  ( ph  ->  (fld 
gsumg  ( T  |`  A ) )  =  (fld  gsumg  T ) )
81, 7breqtrrd 4181 . . . . 5  |-  ( ph  ->  0  <  (fld  gsumg  ( T  |`  A ) ) )
9 ssid 3312 . . . . 5  |-  A  C_  A
108, 9jctil 524 . . . 4  |-  ( ph  ->  ( A  C_  A  /\  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
11 jensen.4 . . . . 5  |-  ( ph  ->  A  e.  Fin )
12 sseq1 3314 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( a 
C_  A  <->  (/)  C_  A
) )
13 reseq2 5083 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( T  |`  a )  =  ( T  |`  (/) ) )
14 res0 5092 . . . . . . . . . . . . 13  |-  ( T  |`  (/) )  =  (/)
1513, 14syl6eq 2437 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  ( T  |`  a )  =  (/) )
1615oveq2d 6038 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  (/) ) )
17 cnfld0 16650 . . . . . . . . . . . 12  |-  0  =  ( 0g ` fld )
1817gsum0 14709 . . . . . . . . . . 11  |-  (fld  gsumg  (/) )  =  0
1916, 18syl6eq 2437 . . . . . . . . . 10  |-  ( a  =  (/)  ->  (fld  gsumg  ( T  |`  a
) )  =  0 )
2019breq2d 4167 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( 0  <  (fld 
gsumg  ( T  |`  a ) )  <->  0  <  0
) )
2112, 20anbi12d 692 . . . . . . . 8  |-  ( a  =  (/)  ->  ( ( a  C_  A  /\  0  <  (fld 
gsumg  ( T  |`  a ) ) )  <->  ( (/)  C_  A  /\  0  <  0
) ) )
22 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  (/)  ->  ( ( T  o F  x.  X )  |`  a
)  =  ( ( T  o F  x.  X )  |`  (/) ) )
2322oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  (/) ) ) )
2423, 19oveq12d 6040 . . . . . . . . 9  |-  ( a  =  (/)  ->  ( (fld  gsumg  ( ( T  o F  x.  X )  |`  a
) )  /  (fld  gsumg  ( T  |`  a
) ) )  =  ( (fld 
gsumg  ( ( T  o F  x.  X )  |`  (/) ) )  /  0
) )
25 reseq2 5083 . . . . . . . . . . . . 13  |-  ( a  =  (/)  ->  ( ( T  o F  x.  ( F  o.  X
) )  |`  a
)  =  ( ( T  o F  x.  ( F  o.  X
) )  |`  (/) ) )
2625oveq2d 6038 . . . . . . . . . . . 12  |-  ( a  =  (/)  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  (/) ) ) )
2726, 19oveq12d 6040 . . . . . . . . . . 11  |-  ( 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
) )
2827breq2d 4167 . . . . . . . . . 10  |-  ( 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
) ) )
2928rabbidv 2893 . . . . . . . . 9  |-  ( 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
) } )
3024, 29eleq12d 2457 . . . . . . . 8  |-  ( 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
) } ) )
3121, 30imbi12d 312 . . . . . . 7  |-  ( 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
) } ) ) )
3231imbi2d 308 . . . . . 6  |-  ( 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
) } ) ) ) )
33 sseq1 3314 . . . . . . . . 9  |-  ( a  =  k  ->  (
a  C_  A  <->  k  C_  A ) )
34 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  k  ->  ( T  |`  a )  =  ( T  |`  k
) )
3534oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  k  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  k ) ) )
3635breq2d 4167 . . . . . . . . 9  |-  ( a  =  k  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  k ) ) ) )
3733, 36anbi12d 692 . . . . . . . 8  |-  ( a  =  k  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( k  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  k )
) ) ) )
38 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  k  ->  (
( T  o F  x.  X )  |`  a )  =  ( ( T  o F  x.  X )  |`  k ) )
3938oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  k ) ) )
4039, 35oveq12d 6040 . . . . . . . . 9  |-  ( 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 )
) ) )
41 reseq2 5083 . . . . . . . . . . . . 13  |-  ( a  =  k  ->  (
( T  o F  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) )
4241oveq2d 6038 . . . . . . . . . . . 12  |-  ( a  =  k  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  k ) ) )
4342, 35oveq12d 6040 . . . . . . . . . . 11  |-  ( 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 )
) ) )
4443breq2d 4167 . . . . . . . . . 10  |-  ( 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 )
) ) ) )
4544rabbidv 2893 . . . . . . . . 9  |-  ( 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 )
) ) } )
4640, 45eleq12d 2457 . . . . . . . 8  |-  ( 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 )
) ) } ) )
4737, 46imbi12d 312 . . . . . . 7  |-  ( 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 )
) ) } ) ) )
4847imbi2d 308 . . . . . 6  |-  ( 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 )
) ) } ) ) ) )
49 sseq1 3314 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( a  C_  A 
<->  ( k  u.  {
c } )  C_  A ) )
50 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( T  |`  a )  =  ( T  |`  ( k  u.  { c } ) ) )
5150oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( T  |`  a ) )  =  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )
5251breq2d 4167 . . . . . . . . 9  |-  ( a  =  ( k  u. 
{ c } )  ->  ( 0  < 
(fld  gsumg  ( T  |`  a )
)  <->  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )
5349, 52anbi12d 692 . . . . . . . 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 5083 . . . . . . . . . . 11  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  o F  x.  X
)  |`  a )  =  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) )
5554oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  ( k  u. 
{ c } )  ->  (fld 
gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  ( k  u.  {
c } ) ) ) )
5655, 51oveq12d 6040 . . . . . . . . 9  |-  ( 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 } ) ) ) ) )
57 reseq2 5083 . . . . . . . . . . . . 13  |-  ( a  =  ( k  u. 
{ c } )  ->  ( ( T  o F  x.  ( F  o.  X )
)  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  ( k  u.  {
c } ) ) )
5857oveq2d 6038 . . . . . . . . . . . 12  |-  ( 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 } ) ) ) )
5958, 51oveq12d 6040 . . . . . . . . . . 11  |-  ( 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 } ) ) ) ) )
6059breq2d 4167 . . . . . . . . . 10  |-  ( 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 } ) ) ) ) ) )
6160rabbidv 2893 . . . . . . . . 9  |-  ( 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 } ) ) ) ) } )
6256, 61eleq12d 2457 . . . . . . . 8  |-  ( 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 } ) ) ) ) } ) )
6353, 62imbi12d 312 . . . . . . 7  |-  ( 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 } ) ) ) ) } ) ) )
6463imbi2d 308 . . . . . 6  |-  ( 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 } ) ) ) ) } ) ) ) )
65 sseq1 3314 . . . . . . . . 9  |-  ( a  =  A  ->  (
a  C_  A  <->  A  C_  A
) )
66 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  A  ->  ( T  |`  a )  =  ( T  |`  A ) )
6766oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  A  ->  (fld  gsumg  ( T  |`  a
) )  =  (fld  gsumg  ( T  |`  A ) ) )
6867breq2d 4167 . . . . . . . . 9  |-  ( a  =  A  ->  (
0  <  (fld  gsumg  ( T  |`  a
) )  <->  0  <  (fld  gsumg  ( T  |`  A ) ) ) )
6965, 68anbi12d 692 . . . . . . . 8  |-  ( a  =  A  ->  (
( a  C_  A  /\  0  <  (fld  gsumg  ( T  |`  a
) ) )  <->  ( A  C_  A  /\  0  < 
(fld  gsumg  ( T  |`  A )
) ) ) )
70 reseq2 5083 . . . . . . . . . . 11  |-  ( a  =  A  ->  (
( T  o F  x.  X )  |`  a )  =  ( ( T  o F  x.  X )  |`  A ) )
7170oveq2d 6038 . . . . . . . . . 10  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  o F  x.  X )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  X )  |`  A ) ) )
7271, 67oveq12d 6040 . . . . . . . . 9  |-  ( 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 )
) ) )
73 reseq2 5083 . . . . . . . . . . . . 13  |-  ( a  =  A  ->  (
( T  o F  x.  ( F  o.  X ) )  |`  a )  =  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) )
7473oveq2d 6038 . . . . . . . . . . . 12  |-  ( a  =  A  ->  (fld  gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  a ) )  =  (fld 
gsumg  ( ( T  o F  x.  ( F  o.  X ) )  |`  A ) ) )
7574, 67oveq12d 6040 . . . . . . . . . . 11  |-  ( 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 )
) ) )
7675breq2d 4167 . . . . . . . . . 10  |-  ( 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 )
) ) ) )
7776rabbidv 2893 . . . . . . . . 9  |-  ( 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 )
) ) } )
7872, 77eleq12d 2457 . . . . . . . 8  |-  ( 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 )
) ) } ) )
7969, 78imbi12d 312 . . . . . . 7  |-  ( 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 )
) ) } ) ) )
8079imbi2d 308 . . . . . 6  |-  ( 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 )
) ) } ) ) ) )
81 0re 9026 . . . . . . . . . 10  |-  0  e.  RR
8281ltnri 9117 . . . . . . . . 9  |-  -.  0  <  0
8382pm2.21i 125 . . . . . . . 8  |-  ( 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
) } )
8483adantl 453 . . . . . . 7  |-  ( (
(/)  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
) } )
8584a1i 11 . . . . . 6  |-  ( 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
) } ) )
86 impexp 434 . . . . . . . . . . . 12  |-  ( ( ( 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 )
) ) } ) ) )
87 simprl 733 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } ) 
C_  A )
8887unssad 3469 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  C_  A )
89 simpr 448 . . . . . . . . . . . . . . 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 711 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  D  C_  RR )
92 jensen.2 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  F : D --> RR )
9392ad3antrrr 711 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  F : D
--> RR )
94 simplll 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 )
) ) } ) )  ->  ph )
95 jensen.3 . . . . . . . . . . . . . . . . . . 19  |-  ( (
ph  /\  ( a  e.  D  /\  b  e.  D ) )  -> 
( a [,] b
)  C_  D )
9694, 95sylan 458 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  /\  ( 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  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 )
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  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 ) )
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  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 )
1011ad3antrrr 711 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  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 458 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  /\  ( 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 736 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  -.  c  e.  k )
10587adantr 452 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  ( k  u.  { c } ) 
C_  A )
106 eqid 2389 . . . . . . . . . . . . . . . . . 18  |-  (fld  gsumg  ( T  |`  k
) )  =  (fld  gsumg  ( T  |`  k ) )
107 eqid 2389 . . . . . . . . . . . . . . . . . 18  |-  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) )  =  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) )
108 cnrng 16648 . . . . . . . . . . . . . . . . . . . . . . 23  |-fld  e.  Ring
109 rngcmn 15623 . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  A  e.  Fin )
112 ssfi 7267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  Fin  /\  k  C_  A )  -> 
k  e.  Fin )
113111, 88, 112syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  k  e.  Fin )
114 rege0subm 16680 . . . . . . . . . . . . . . . . . . . . . . 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 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  T : A
--> ( 0 [,)  +oo ) )
117 fssres 5552 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  k  C_  A )  ->  ( T  |`  k ) : k --> ( 0 [,) 
+oo ) )
118116, 88, 117syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( T  |`  k ) : k --> ( 0 [,)  +oo ) )
119113, 118fisuppfi 14702 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( `' ( T  |`  k )
" ( _V  \  { 0 } ) )  e.  Fin )
12017, 110, 113, 115, 118, 119gsumsubmcl 15453 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  ( 0 [,)  +oo )
)
121 elrege0 10941 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,)  +oo ) 
<->  ( (fld 
gsumg  ( T  |`  k ) )  e.  RR  /\  0  <_  (fld 
gsumg  ( T  |`  k ) ) ) )
122121simplbi 447 . . . . . . . . . . . . . . . . . . . . 21  |-  ( (fld  gsumg  ( T  |`  k ) )  e.  ( 0 [,)  +oo )  ->  (fld 
gsumg  ( T  |`  k ) )  e.  RR )
123120, 122syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  (fld  gsumg  ( T  |`  k
) )  e.  RR )
124123adantr 452 . . . . . . . . . . . . . . . . . . 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 )
125 simprl 733 . . . . . . . . . . . . . . . . . . 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  |`  k ) ) )
126124, 125elrpd 10580 . . . . . . . . . . . . . . . . . 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  |`  k
) )  e.  RR+ )
127 simprr 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 )
) ) } ) )  ->  ( (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 )
) ) } )
128 fveq2 5670 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( 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 )
) ) ) )
129128breq1d 4165 . . . . . . . . . . . . . . . . . . . . 21  |-  ( 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 )
) ) ) )
130129elrab 3037 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( (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 )
) ) ) )
131127, 130sylib 189 . . . . . . . . . . . . . . . . . . 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  /\  ( 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 )
) ) ) )
132131simpld 446 . . . . . . . . . . . . . . . . . 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 ) )  / 
(fld  gsumg  ( T  |`  k )
) )  e.  D
)
133131simprd 450 . . . . . . . . . . . . . . . . . 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 )
) ) } ) )  ->  ( 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 )
) ) )
13491, 93, 96, 97, 98, 100, 101, 103, 104, 105, 106, 107, 126, 132, 133jensenlem2 20695 . . . . . . . . . . . . . . . . 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.  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 } ) ) ) ) ) )
135 fveq2 5670 . . . . . . . . . . . . . . . . . . 19  |-  ( 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 } ) ) ) ) ) )
136135breq1d 4165 . . . . . . . . . . . . . . . . . 18  |-  ( 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 } ) ) ) ) ) )
137136elrab 3037 . . . . . . . . . . . . . . . . 17  |-  ( ( (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 } ) ) ) ) ) )
138134, 137sylibr 204 . . . . . . . . . . . . . . . 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 } ) ) ) ) } )
139138expr 599 . . . . . . . . . . . . . . 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  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 } ) ) ) ) } ) )
14089, 139embantd 52 . . . . . . . . . . . . . 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  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 } ) ) ) ) } ) )
141 cnfldbas 16632 . . . . . . . . . . . . . . . . . . . . 21  |-  CC  =  ( Base ` fld )
142 rngmnd 15602 . . . . . . . . . . . . . . . . . . . . . 22  |-  (fld  e.  Ring  ->fld  e.  Mnd )
143108, 142mp1i 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 )
144 ssfi 7267 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( A  e.  Fin  /\  ( k  u.  {
c } )  C_  A )  ->  (
k  u.  { c } )  e.  Fin )
145111, 87, 144syl2anc 643 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  -.  c  e.  k )  /\  ( ( k  u. 
{ c } ) 
C_  A  /\  0  <  (fld 
gsumg  ( T  |`  ( k  u.  { c } ) ) ) ) )  ->  ( k  u.  { c } )  e.  Fin )
146145adantr 452 . . . . . . . . . . . . . . . . . . . . 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 )
147 ssun2 3456 . . . . . . . . . . . . . . . . . . . . . . 23  |-  { c }  C_  ( k  u.  { c } )
148 vex 2904 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  c  e. 
_V
149148snid 3786 . . . . . . . . . . . . . . . . . . . . . . 23  |-  c  e. 
{ c }
150147, 149sselii 3290 . . . . . . . . . . . . . . . . . . . . . 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 9010 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( x  e.  RR  /\  y  e.  RR )  ->  ( x  x.  y
)  e.  RR )
153152adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( (
ph  /\  ( x  e.  RR  /\  y  e.  RR ) )  -> 
( x  x.  y
)  e.  RR )
154 elrege0 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( x  e.  ( 0 [,) 
+oo )  <->  ( x  e.  RR  /\  0  <_  x ) )
155154simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( 0 [,) 
+oo )  ->  x  e.  RR )
156155ssriv 3297 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 [,)  +oo )  C_  RR
157 fss 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  RR )  ->  T : A
--> RR )
1582, 156, 157sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  T : A --> RR )
159 fss 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( X : A --> D  /\  D  C_  RR )  ->  X : A --> RR )
16099, 90, 159syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ph  ->  X : A --> RR )
161 inidm 3495 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( A  i^i  A )  =  A
162153, 158, 160, 11, 11, 161off 6261 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ph  ->  ( T  o F  x.  X ) : A --> RR )
163 ax-resscn 8982 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  RR  C_  CC
164 fss 5541 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( T  o F  x.  X ) : A --> RR  /\  RR  C_  CC )  ->  ( T  o F  x.  X
) : A --> CC )
165162, 163, 164sylancl 644 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ph  ->  ( T  o F  x.  X ) : A --> CC )
166165ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . 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
) : A --> CC )
16787adantr 452 . . . . . . . . . . . . . . . . . . . . . 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
)
168 fssres 5552 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( T  o F  x.  X ) : A --> CC  /\  (
k  u.  { c } )  C_  A
)  ->  ( ( T  o F  x.  X
)  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
169166, 167, 168syl2anc 643 . . . . . . . . . . . . . . . . . . . . 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 } ) ) : ( k  u. 
{ c } ) --> CC )
1702ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( 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 ) )
171111adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  A  e.  Fin )
172 fex 5910 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  A  e.  Fin )  ->  T  e.  _V )
173170, 171, 172syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  T  e.  _V )
17499ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X : A --> D )
175 fex 5910 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( X : A --> D  /\  A  e.  Fin )  ->  X  e.  _V )
176174, 171, 175syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  -.  c  e.  k
)  /\  ( (
k  u.  { c } )  C_  A  /\  0  <  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) ) )  /\  0  =  (fld 
gsumg  ( T  |`  k ) ) )  ->  X  e.  _V )
177 offres 6260 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( 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 } ) ) ) )
178173, 176, 177syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
179178cnveqd 4990 . . . . . . . . . . . . . . . . . . . . . . 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 } ) )  =  `' ( ( T  |`  ( k  u.  { c } ) )  o F  x.  ( X  |`  ( k  u.  { c } ) ) ) )
180179imaeq1d 5144 . . . . . . . . . . . . . . . . . . . . . 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 } ) )  =  ( `' ( ( T  |`  ( k  u.  {
c } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) " ( _V  \  { 0 } ) ) )
181156, 163sstri 3302 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( 0 [,)  +oo )  C_  CC
182 fss 5541 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( T : A --> ( 0 [,)  +oo )  /\  (
0 [,)  +oo )  C_  CC )  ->  T : A
--> CC )
183170, 181, 182sylancl 644 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
184 fssres 5552 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( T : A --> CC  /\  ( k  u.  {
c } )  C_  A )  ->  ( T  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
185183, 167, 184syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 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 )
186 eldifi 3414 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  ( k  u.  {
c } ) )
187186adantl 453 . . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
188 fvres 5687 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 x )  =  ( T `  x
) )
189187, 188syl 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 ) )
190 difun2 3652 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( k  u.  { c } )  \  {
c } )  =  ( k  \  {
c } )
191 difss 3419 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( k 
\  { c } )  C_  k
192190, 191eqsstri 3323 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( k  u.  { c } )  \  {
c } )  C_  k
193192sseli 3289 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( x  e.  ( ( k  u.  { c } )  \  { c } )  ->  x  e.  k )
194 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
19588adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
196170, 195feqresmpt 5721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) ) )
197196oveq2d 6038 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) )
198113adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
199195sselda 3293 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
200170ffvelrnda 5811 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
201199, 200syldan 457 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
202181, 201sseldi 3291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
203198, 202gsumfsum 16691 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
204194, 197, 2033eqtrrd 2426 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
205 elrege0 10941 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31  |-  ( ( T `  x )  e.  ( 0 [,) 
+oo )  <->  ( ( T `  x )  e.  RR  /\  0  <_ 
( T `  x
) ) )
206201, 205sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) )
207206simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
208206simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 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
) )
209198, 207, 208fsum00 12506 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 ) )
210204, 209mpbid 202 . . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
211210r19.21bi 2749 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
212193, 211sylan2 461 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
213189, 212eqtrd 2421 . . . . . . . . . . . . . . . . . . . . . . . 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 )
214185, 213suppss 5804 . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
" ( _V  \  { 0 } ) )  C_  { c } )
215 mul02 9178 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( x  e.  CC  ->  (
0  x.  x )  =  0 )
216215adantl 453 . . . . . . . . . . . . . . . . . . . . . . 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 )
21790ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . . 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 )
218217, 163syl6ss 3305 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
219 fss 5541 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( X : A --> D  /\  D  C_  CC )  ->  X : A --> CC )
220174, 218, 219syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . 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 )
221 fssres 5552 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( X : A --> CC  /\  ( k  u.  {
c } )  C_  A )  ->  ( X  |`  ( k  u. 
{ c } ) ) : ( k  u.  { c } ) --> CC )
222220, 167, 221syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . 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 )
223214, 216, 185, 222, 146suppssof1 6287 . . . . . . . . . . . . . . . . . . . . . 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 } ) )  o F  x.  ( X  |`  ( k  u. 
{ c } ) ) ) " ( _V  \  { 0 } ) )  C_  { c } )
224180, 223eqsstrd 3327 . . . . . . . . . . . . . . . . . . . . 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 } ) ) " ( _V 
\  { 0 } ) )  C_  { c } )
225141, 17, 143, 146, 151, 169, 224gsumpt 15474 . . . . . . . . . . . . . . . . . . . 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  o F  x.  X )  |`  ( k  u.  {
c } ) ) `
 c ) )
226 fvres 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( ( T  o F  x.  X )  |`  (
k  u.  { c } ) ) `  c )  =  ( ( T  o F  x.  X ) `  c ) )
227151, 226syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) )
228170, 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 )
229 ffn 5533 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( X : A --> D  ->  X  Fn  A )
230174, 229syl 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 )
231167, 151sseldd 3294 . . . . . . . . . . . . . . . . . . . . 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 )
232 fnfvof 6258 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( T  Fn  A  /\  X  Fn  A
)  /\  ( A  e.  Fin  /\  c  e.  A ) )  -> 
( ( T  o F  x.  X ) `  c )  =  ( ( T `  c
)  x.  ( X `
 c ) ) )
233228, 230, 171, 231, 232syl22anc 1185 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( 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 ) ) )
234225, 227, 2333eqtrd 2425 . . . . . . . . . . . . . . . . . . 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  u.  {
c } ) ) )  =  ( ( T `  c )  x.  ( X `  c ) ) )
235141, 17, 143, 146, 151, 185, 214gsumpt 15474 . . . . . . . . . . . . . . . . . . . 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 ) )
236 fvres 5687 . . . . . . . . . . . . . . . . . . . . 21  |-  ( c  e.  ( k  u. 
{ c } )  ->  ( ( T  |`  ( k  u.  {
c } ) ) `
 c )  =  ( T `  c
) )
237151, 236syl 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 ) )
238235, 237eqtrd 2421 . . . . . . . . . . . . . . . . . . 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 ) )
239234, 238oveq12d 6040 . . . . . . . . . . . . . . . . . 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  u.  {
c } ) ) )  /  (fld  gsumg  ( T  |`  (
k  u.  { c } ) ) ) )  =  ( ( ( T `  c
)  x.  ( X `
 c ) )  /  ( T `  c ) ) )
240220, 231ffvelrnd 5812 . . . . . . . . . . . . . . . . . . 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 )
241183, 231ffvelrnd 5812 . . . . . . . . . . . . . . . . . . 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 )
242 simplrr 738 . . . . . . . . . . . . . . . . . . . . 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 } ) ) ) )
243242, 238breqtrd 4179 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\