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

Theorem imasdsf1olem 17937
Description: Lemma for imasdsf1o 17938. (Contributed by Mario Carneiro, 21-Aug-2015.)
Hypotheses
Ref Expression
imasdsf1o.u  |-  ( ph  ->  U  =  ( F 
"s  R ) )
imasdsf1o.v  |-  ( ph  ->  V  =  ( Base `  R ) )
imasdsf1o.f  |-  ( ph  ->  F : V -1-1-onto-> B )
imasdsf1o.r  |-  ( ph  ->  R  e.  Z )
imasdsf1o.e  |-  E  =  ( ( dist `  R
)  |`  ( V  X.  V ) )
imasdsf1o.d  |-  D  =  ( dist `  U
)
imasdsf1o.m  |-  ( ph  ->  E  e.  ( * Met `  V ) )
imasdsf1o.x  |-  ( ph  ->  X  e.  V )
imasdsf1o.y  |-  ( ph  ->  Y  e.  V )
imasdsf1o.w  |-  W  =  ( RR* ss  ( RR*  \  {  -oo } ) )
imasdsf1o.s  |-  S  =  { h  e.  ( ( V  X.  V
)  ^m  ( 1 ... n ) )  |  ( ( F `
 ( 1st `  (
h `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( h `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }
imasdsf1o.t  |-  T  = 
U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )
Assertion
Ref Expression
imasdsf1olem  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  ( X E Y ) )
Distinct variable groups:    g, h, i, n, F    ph, g, h, i, n    g, V, h, i, n    g, E, i, n    R, g, h, i, n    S, g    g, X, h, i, n    g, Y, h, i, n
Allowed substitution hints:    B( g, h, i, n)    D( g, h, i, n)    S( h, i, n)    T( g, h, i, n)    U( g, h, i, n)    E( h)    W( g, h, i, n)    Z( g, h, i, n)

Proof of Theorem imasdsf1olem
Dummy variables  f 
j  m  p  x are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 imasdsf1o.u . . . 4  |-  ( ph  ->  U  =  ( F 
"s  R ) )
2 imasdsf1o.v . . . 4  |-  ( ph  ->  V  =  ( Base `  R ) )
3 imasdsf1o.f . . . . 5  |-  ( ph  ->  F : V -1-1-onto-> B )
4 f1ofo 5479 . . . . 5  |-  ( F : V -1-1-onto-> B  ->  F : V -onto-> B )
53, 4syl 15 . . . 4  |-  ( ph  ->  F : V -onto-> B
)
6 imasdsf1o.r . . . 4  |-  ( ph  ->  R  e.  Z )
7 eqid 2283 . . . 4  |-  ( dist `  R )  =  (
dist `  R )
8 imasdsf1o.d . . . 4  |-  D  =  ( dist `  U
)
9 f1of 5472 . . . . . 6  |-  ( F : V -1-1-onto-> B  ->  F : V
--> B )
103, 9syl 15 . . . . 5  |-  ( ph  ->  F : V --> B )
11 imasdsf1o.x . . . . 5  |-  ( ph  ->  X  e.  V )
12 ffvelrn 5663 . . . . 5  |-  ( ( F : V --> B  /\  X  e.  V )  ->  ( F `  X
)  e.  B )
1310, 11, 12syl2anc 642 . . . 4  |-  ( ph  ->  ( F `  X
)  e.  B )
14 imasdsf1o.y . . . . 5  |-  ( ph  ->  Y  e.  V )
15 ffvelrn 5663 . . . . 5  |-  ( ( F : V --> B  /\  Y  e.  V )  ->  ( F `  Y
)  e.  B )
1610, 14, 15syl2anc 642 . . . 4  |-  ( ph  ->  ( F `  Y
)  e.  B )
17 imasdsf1o.s . . . 4  |-  S  =  { h  e.  ( ( V  X.  V
)  ^m  ( 1 ... n ) )  |  ( ( F `
 ( 1st `  (
h `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( h `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }
18 imasdsf1o.e . . . 4  |-  E  =  ( ( dist `  R
)  |`  ( V  X.  V ) )
191, 2, 5, 6, 7, 8, 13, 16, 17, 18imasdsval2 13419 . . 3  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  sup ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) ,  RR* ,  `'  <  ) )
20 imasdsf1o.t . . . 4  |-  T  = 
U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )
2120supeq1i 7200 . . 3  |-  sup ( T ,  RR* ,  `'  <  )  =  sup ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) ,  RR* ,  `'  <  )
2219, 21syl6eqr 2333 . 2  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  sup ( T ,  RR* ,  `'  <  ) )
23 difss 3303 . . . . . . . . . 10  |-  ( RR*  \  {  -oo } ) 
C_  RR*
24 xrsbas 16390 . . . . . . . . . . . 12  |-  RR*  =  ( Base `  RR* s )
25 xrsadd 16391 . . . . . . . . . . . 12  |-  + e  =  ( +g  `  RR* s
)
26 imasdsf1o.w . . . . . . . . . . . 12  |-  W  =  ( RR* ss  ( RR*  \  {  -oo } ) )
27 xrsex 16382 . . . . . . . . . . . . 13  |-  RR* s  e.  _V
2827a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  RR* s  e.  _V )
29 fzfid 11035 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1 ... n )  e. 
Fin )
3023a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*  \  {  -oo }
)  C_  RR* )
31 imasdsf1o.m . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  ( * Met `  V ) )
32 xmetf 17894 . . . . . . . . . . . . . . . 16  |-  ( E  e.  ( * Met `  V )  ->  E : ( V  X.  V ) --> RR* )
33 ffn 5389 . . . . . . . . . . . . . . . 16  |-  ( E : ( V  X.  V ) --> RR*  ->  E  Fn  ( V  X.  V ) )
3431, 32, 333syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  Fn  ( V  X.  V ) )
35 xmetcl 17896 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e. 
RR* )
36 xmetge0 17909 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  0  <_  ( f E g ) )
37 ge0nemnf 10502 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f E g )  e.  RR*  /\  0  <_  ( f E g ) )  ->  (
f E g )  =/=  -oo )
3835, 36, 37syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  =/= 
-oo )
39 eldifsn 3749 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f E g )  e.  ( RR*  \  {  -oo } )  <->  ( (
f E g )  e.  RR*  /\  (
f E g )  =/=  -oo ) )
4035, 38, 39sylanbrc 645 . . . . . . . . . . . . . . . . . 18  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e.  ( RR*  \  {  -oo } ) )
41403expb 1152 . . . . . . . . . . . . . . . . 17  |-  ( ( E  e.  ( * Met `  V )  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  {  -oo } ) )
4231, 41sylan 457 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  {  -oo } ) )
4342ralrimivva 2635 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. f  e.  V  A. g  e.  V  ( f E g )  e.  ( RR*  \  {  -oo } ) )
44 ffnov 5948 . . . . . . . . . . . . . . 15  |-  ( E : ( V  X.  V ) --> ( RR*  \  {  -oo } )  <-> 
( E  Fn  ( V  X.  V )  /\  A. f  e.  V  A. g  e.  V  (
f E g )  e.  ( RR*  \  {  -oo } ) ) )
4534, 43, 44sylanbrc 645 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : ( V  X.  V ) --> (
RR*  \  {  -oo }
) )
4645ad2antrr 706 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> ( RR*  \  {  -oo } ) )
47 ssrab2 3258 . . . . . . . . . . . . . . . . 17  |-  { h  e.  ( ( V  X.  V )  ^m  (
1 ... n ) )  |  ( ( F `
 ( 1st `  (
h `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( h `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  C_  (
( V  X.  V
)  ^m  ( 1 ... n ) )
4817, 47eqsstri 3208 . . . . . . . . . . . . . . . 16  |-  S  C_  ( ( V  X.  V )  ^m  (
1 ... n ) )
4948a1i 10 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  S  C_  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
5049sselda 3180 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
51 elmapi 6792 . . . . . . . . . . . . . 14  |-  ( g  e.  ( ( V  X.  V )  ^m  ( 1 ... n
) )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
5250, 51syl 15 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
53 fco 5398 . . . . . . . . . . . . 13  |-  ( ( E : ( V  X.  V ) --> (
RR*  \  {  -oo }
)  /\  g :
( 1 ... n
) --> ( V  X.  V ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
) )
5446, 52, 53syl2anc 642 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) : ( 1 ... n ) --> ( RR*  \  {  -oo } ) )
55 0re 8838 . . . . . . . . . . . . 13  |-  0  e.  RR
56 rexr 8877 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  e.  RR* )
57 renemnf 8880 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  =/=  -oo )
58 eldifsn 3749 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( RR*  \  {  -oo } )  <->  ( 0  e.  RR*  /\  0  =/=  -oo ) )
5956, 57, 58sylanbrc 645 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  0  e.  ( RR*  \  {  -oo } ) )
6055, 59mp1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  0  e.  ( RR*  \  {  -oo } ) )
61 xaddid2 10567 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( 0 + e x )  =  x )
62 xaddid1 10566 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( x + e 0 )  =  x )
6361, 62jca 518 . . . . . . . . . . . . 13  |-  ( x  e.  RR*  ->  ( ( 0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
6463adantl 452 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  RR* )  ->  ( (
0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
6524, 25, 26, 28, 29, 30, 54, 60, 64gsumress 14454 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  =  ( W  gsumg  ( E  o.  g
) ) )
6626, 24ressbas2 13199 . . . . . . . . . . . . 13  |-  ( (
RR*  \  {  -oo }
)  C_  RR*  ->  ( RR*  \  {  -oo }
)  =  ( Base `  W ) )
6723, 66ax-mp 8 . . . . . . . . . . . 12  |-  ( RR*  \  {  -oo } )  =  ( Base `  W
)
6826xrs10 16410 . . . . . . . . . . . 12  |-  0  =  ( 0g `  W )
6926xrs1cmn 16411 . . . . . . . . . . . . 13  |-  W  e. CMnd
7069a1i 10 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e. CMnd )
7129, 54fisuppfi 14450 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( `' ( E  o.  g ) " ( _V  \  { 0 } ) )  e.  Fin )
7267, 68, 70, 29, 54, 71gsumcl 15198 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( E  o.  g
) )  e.  (
RR*  \  {  -oo }
) )
7365, 72eqeltrd 2357 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  e.  (
RR*  \  {  -oo }
) )
7423, 73sseldi 3178 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  e.  RR* )
75 eqid 2283 . . . . . . . . 9  |-  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  =  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )
7674, 75fmptd 5684 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) : S --> RR* )
77 frn 5395 . . . . . . . 8  |-  ( ( g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) ) : S --> RR*  ->  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7876, 77syl 15 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7978ralrimiva 2626 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )  C_  RR* )
80 iunss 3943 . . . . . 6  |-  ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )  C_  RR*  <->  A. n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  C_  RR* )
8179, 80sylibr 203 . . . . 5  |-  ( ph  ->  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )  C_  RR* )
8220, 81syl5eqss 3222 . . . 4  |-  ( ph  ->  T  C_  RR* )
83 1nn 9757 . . . . . . 7  |-  1  e.  NN
84 1ex 8833 . . . . . . . . . . . 12  |-  1  e.  _V
85 opex 4237 . . . . . . . . . . . 12  |-  <. X ,  Y >.  e.  _V
8684, 85f1osn 5513 . . . . . . . . . . 11  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } -1-1-onto-> { <. X ,  Y >. }
87 f1of 5472 . . . . . . . . . . 11  |-  ( {
<. 1 ,  <. X ,  Y >. >. } : { 1 } -1-1-onto-> { <. X ,  Y >. }  ->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. } )
8886, 87ax-mp 8 . . . . . . . . . 10  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. }
89 opelxpi 4721 . . . . . . . . . . . 12  |-  ( ( X  e.  V  /\  Y  e.  V )  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9011, 14, 89syl2anc 642 . . . . . . . . . . 11  |-  ( ph  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9190snssd 3760 . . . . . . . . . 10  |-  ( ph  ->  { <. X ,  Y >. }  C_  ( V  X.  V ) )
92 fss 5397 . . . . . . . . . 10  |-  ( ( { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> { <. X ,  Y >. }  /\  {
<. X ,  Y >. } 
C_  ( V  X.  V ) )  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9388, 91, 92sylancr 644 . . . . . . . . 9  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
94 fvex 5539 . . . . . . . . . . . 12  |-  ( Base `  R )  e.  _V
952, 94syl6eqel 2371 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  _V )
96 xpexg 4800 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  V  e.  _V )  ->  ( V  X.  V
)  e.  _V )
9795, 95, 96syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( V  X.  V
)  e.  _V )
98 snex 4216 . . . . . . . . . 10  |-  { 1 }  e.  _V
99 elmapg 6785 . . . . . . . . . 10  |-  ( ( ( V  X.  V
)  e.  _V  /\  { 1 }  e.  _V )  ->  ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V
)  ^m  { 1 } )  <->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> ( V  X.  V ) ) )
10097, 98, 99sylancl 643 . . . . . . . . 9  |-  ( ph  ->  ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V
)  ^m  { 1 } )  <->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> ( V  X.  V ) ) )
10193, 100mpbird 223 . . . . . . . 8  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V )  ^m  {
1 } ) )
102 op1stg 6132 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 1st `  <. X ,  Y >. )  =  X )
10311, 14, 102syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  <. X ,  Y >. )  =  X )
104103fveq2d 5529 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X ) )
105 op2ndg 6133 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
10611, 14, 105syl2anc 642 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
107106fveq2d 5529 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) )
108104, 107jca 518 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
10927a1i 10 . . . . . . . . . . 11  |-  ( ph  -> 
RR* s  e.  _V )
110 snfi 6941 . . . . . . . . . . . 12  |-  { 1 }  e.  Fin
111110a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  { 1 }  e.  Fin )
11223a1i 10 . . . . . . . . . . 11  |-  ( ph  ->  ( RR*  \  {  -oo } )  C_  RR* )
113 xmetcl 17896 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  ( X E Y )  e.  RR* )
11431, 11, 14, 113syl3anc 1182 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X E Y )  e.  RR* )
115 xmetge0 17909 . . . . . . . . . . . . . . . 16  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  0  <_  ( X E Y ) )
11631, 11, 14, 115syl3anc 1182 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( X E Y ) )
117 ge0nemnf 10502 . . . . . . . . . . . . . . 15  |-  ( ( ( X E Y )  e.  RR*  /\  0  <_  ( X E Y ) )  ->  ( X E Y )  =/= 
-oo )
118114, 116, 117syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X E Y )  =/=  -oo )
119 eldifsn 3749 . . . . . . . . . . . . . 14  |-  ( ( X E Y )  e.  ( RR*  \  {  -oo } )  <->  ( ( X E Y )  e. 
RR*  /\  ( X E Y )  =/=  -oo ) )
120114, 118, 119sylanbrc 645 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X E Y )  e.  ( RR*  \  {  -oo } ) )
121 fconst6g 5430 . . . . . . . . . . . . 13  |-  ( ( X E Y )  e.  ( RR*  \  {  -oo } )  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  {  -oo } ) )
122120, 121syl 15 . . . . . . . . . . . 12  |-  ( ph  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  {  -oo } ) )
123 fcoconst 5695 . . . . . . . . . . . . . . 15  |-  ( ( E  Fn  ( V  X.  V )  /\  <. X ,  Y >.  e.  ( V  X.  V
) )  ->  ( E  o.  ( {
1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `  <. X ,  Y >. ) } ) )
12434, 90, 123syl2anc 642 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `
 <. X ,  Y >. ) } ) )
12584, 85xpsn 5700 . . . . . . . . . . . . . . 15  |-  ( { 1 }  X.  { <. X ,  Y >. } )  =  { <. 1 ,  <. X ,  Y >. >. }
126125coeq2i 4844 . . . . . . . . . . . . . 14  |-  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )
127 df-ov 5861 . . . . . . . . . . . . . . . . 17  |-  ( X E Y )  =  ( E `  <. X ,  Y >. )
128127eqcomi 2287 . . . . . . . . . . . . . . . 16  |-  ( E `
 <. X ,  Y >. )  =  ( X E Y )
129128sneqi 3652 . . . . . . . . . . . . . . 15  |-  { ( E `  <. X ,  Y >. ) }  =  { ( X E Y ) }
130129xpeq2i 4710 . . . . . . . . . . . . . 14  |-  ( { 1 }  X.  {
( E `  <. X ,  Y >. ) } )  =  ( { 1 }  X.  { ( X E Y ) } )
131124, 126, 1303eqtr3g 2338 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( { 1 }  X.  { ( X E Y ) } ) )
132131feq1d 5379 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  {  -oo } )  <->  ( { 1 }  X.  { ( X E Y ) } ) : {
1 } --> ( RR*  \  {  -oo } ) ) )
133122, 132mpbird 223 . . . . . . . . . . 11  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  {  -oo } ) )
13455, 59mp1i 11 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( RR*  \  {  -oo } ) )
13563adantl 452 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
13624, 25, 26, 109, 111, 112, 133, 134, 135gsumress 14454 . . . . . . . . . 10  |-  ( ph  ->  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
137 fconstmpt 4732 . . . . . . . . . . . 12  |-  ( { 1 }  X.  {
( X E Y ) } )  =  ( j  e.  {
1 }  |->  ( X E Y ) )
138131, 137syl6eq 2331 . . . . . . . . . . 11  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( j  e.  {
1 }  |->  ( X E Y ) ) )
139138oveq2d 5874 . . . . . . . . . 10  |-  ( ph  ->  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
140136, 139eqtrd 2315 . . . . . . . . 9  |-  ( ph  ->  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
141 cmnmnd 15104 . . . . . . . . . . 11  |-  ( W  e. CMnd  ->  W  e.  Mnd )
14269, 141mp1i 11 . . . . . . . . . 10  |-  ( ph  ->  W  e.  Mnd )
14383a1i 10 . . . . . . . . . 10  |-  ( ph  ->  1  e.  NN )
144 eqidd 2284 . . . . . . . . . . 11  |-  ( j  =  1  ->  ( X E Y )  =  ( X E Y ) )
14567, 144gsumsn 15220 . . . . . . . . . 10  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( X E Y )  e.  ( RR*  \  {  -oo } ) )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
146142, 143, 120, 145syl3anc 1182 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
147140, 146eqtr2d 2316 . . . . . . . 8  |-  ( ph  ->  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
148 fveq1 5524 . . . . . . . . . . . . . . 15  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  ( { <. 1 ,  <. X ,  Y >. >. } `  1
) )
14984, 85fvsn 5713 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  <. X ,  Y >. >. } ` 
1 )  =  <. X ,  Y >.
150148, 149syl6eq 2331 . . . . . . . . . . . . . 14  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  <. X ,  Y >. )
151150fveq2d 5529 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 1st `  ( g ` 
1 ) )  =  ( 1st `  <. X ,  Y >. )
)
152151fveq2d 5529 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  ( 1st `  <. X ,  Y >. ) ) )
153152eqeq1d 2291 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  <. X ,  Y >. )
)  =  ( F `
 X ) ) )
154150fveq2d 5529 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 2nd `  ( g ` 
1 ) )  =  ( 2nd `  <. X ,  Y >. )
)
155154fveq2d 5529 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  ( 2nd `  <. X ,  Y >. ) ) )
156155eqeq1d 2291 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 2nd `  ( g ` 
1 ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
157153, 156anbi12d 691 . . . . . . . . . 10  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  <->  ( ( F `  ( 1st ` 
<. X ,  Y >. ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) ) ) )
158 coeq2 4842 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( E  o.  g )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )
159158oveq2d 5874 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( RR* s  gsumg  ( E  o.  g
) )  =  (
RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
160159eqeq2d 2294 . . . . . . . . . 10  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( X E Y )  =  ( RR* s  gsumg  ( E  o.  g
) )  <->  ( X E Y )  =  (
RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) ) )
161157, 160anbi12d 691 . . . . . . . . 9  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 1 ) ) )  =  ( F `
 Y ) )  /\  ( X E Y )  =  (
RR* s  gsumg  ( E  o.  g
) ) )  <->  ( (
( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) ) ) )
162161rspcev 2884 . . . . . . . 8  |-  ( ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V )  ^m  {
1 } )  /\  ( ( ( F `
 ( 1st `  <. X ,  Y >. )
)  =  ( F `
 X )  /\  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) ) )  ->  E. g  e.  ( ( V  X.  V )  ^m  {
1 } ) ( ( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) )
163101, 108, 147, 162syl12anc 1180 . . . . . . 7  |-  ( ph  ->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) )
164 ovex 5883 . . . . . . . . . 10  |-  ( X E Y )  e. 
_V
16575elrnmpt 4926 . . . . . . . . . 10  |-  ( ( X E Y )  e.  _V  ->  (
( X E Y )  e.  ran  (
g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  ( X E Y )  =  (
RR* s  gsumg  ( E  o.  g
) ) ) )
166164, 165ax-mp 8 . . . . . . . . 9  |-  ( ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  ( X E Y )  =  (
RR* s  gsumg  ( E  o.  g
) ) )
16717rexeqi 2741 . . . . . . . . . . 11  |-  ( E. g  e.  S  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) )  <->  E. g  e.  {
h  e.  ( ( V  X.  V )  ^m  ( 1 ... n ) )  |  ( ( F `  ( 1st `  ( h `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( h `
 i ) ) )  =  ( F `
 ( 1st `  (
h `  ( i  +  1 ) ) ) ) ) }  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g
) ) )
168 fveq1 5524 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  1 )  =  ( g ` 
1 ) )
169168fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 1st `  ( h ` 
1 ) )  =  ( 1st `  (
g `  1 )
) )
170169fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  1
) ) )  =  ( F `  ( 1st `  ( g ` 
1 ) ) ) )
171170eqeq1d 2291 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 1st `  ( h ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  (
g `  1 )
) )  =  ( F `  X ) ) )
172 fveq1 5524 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  n )  =  ( g `  n ) )
173172fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 2nd `  ( h `  n ) )  =  ( 2nd `  (
g `  n )
) )
174173fveq2d 5529 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  ( 2nd `  ( g `  n ) ) ) )
175174eqeq1d 2291 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y ) ) )
176 fveq1 5524 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  i )  =  ( g `  i ) )
177176fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 2nd `  ( h `  i ) )  =  ( 2nd `  (
g `  i )
) )
178177fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 2nd `  ( g `  i ) ) ) )
179 fveq1 5524 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  ( i  +  1 ) )  =  ( g `  ( i  +  1 ) ) )
180179fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 1st `  ( h `  ( i  +  1 ) ) )  =  ( 1st `  (
g `  ( i  +  1 ) ) ) )
181180fveq2d 5529 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  (
i  +  1 ) ) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )
182178, 181eqeq12d 2297 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  i ) ) )  =  ( F `  ( 1st `  ( h `
 ( i  +  1 ) ) ) )  <->  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
183182ralbidv 2563 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  ( A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) )  <->  A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) )
184171, 175, 1833anbi123d 1252 . . . . . . . . . . . 12  |-  ( h  =  g  ->  (
( ( F `  ( 1st `  ( h `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( h `
 i ) ) )  =  ( F `
 ( 1st `  (
h `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y )  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) ) )
185184rexrab 2929 . . . . . . . . . . 11  |-  ( E. g  e.  { h  e.  ( ( V  X.  V )  ^m  (
1 ... n ) )  |  ( ( F `
 ( 1st `  (
h `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( h `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) )  <->  E. g  e.  (
( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) )
186167, 185bitri 240 . . . . . . . . . 10  |-  ( E. g  e.  S  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) )
187 oveq2 5866 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
188 1z 10053 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
189 fzsn 10833 . . . . . . . . . . . . . 14  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
190188, 189ax-mp 8 . . . . . . . . . . . . 13  |-  ( 1 ... 1 )  =  { 1 }
191187, 190syl6eq 2331 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
1 ... n )  =  { 1 } )
192191oveq2d 5874 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( V  X.  V
)  ^m  ( 1 ... n ) )  =  ( ( V  X.  V )  ^m  { 1 } ) )
193 df-3an 936 . . . . . . . . . . . . 13  |-  ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) )
194 ral0 3558 . . . . . . . . . . . . . . . 16  |-  A. i  e.  (/)  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) )
195 oveq1 5865 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
196 1m1e0 9814 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  -  1 )  =  0
197195, 196syl6eq 2331 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
198197oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  ( 1 ... 0
) )
199 fz10 10814 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... 0 )  =  (/)
200198, 199syl6eq 2331 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  (/) )
201200raleqdv 2742 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) )  <->  A. i  e.  (/)  ( F `
 ( 2nd `  (
g `  i )
) )  =  ( F `  ( 1st `  ( g `  (
i  +  1 ) ) ) ) ) )
202194, 201mpbiri 224 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )
203202biantrud 493 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  <->  ( (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) ) )
204 fveq2 5525 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
g `  n )  =  ( g ` 
1 ) )
205204fveq2d 5529 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( 2nd `  ( g `  n ) )  =  ( 2nd `  (
g `  1 )
) )
206205fveq2d 5529 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  ( 2nd `  ( g ` 
1 ) ) ) )
207206eqeq1d 2291 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) )
208207anbi2d 684 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
209203, 208bitr3d 246 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y ) )  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
210193, 209syl5bb 248 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
211210anbi1d 685 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) )  <->  ( ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) ) )
212192, 211rexeqbidv 2749 . . . . . . . . . 10  |-  ( n  =  1  ->  ( E. g  e.  (
( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) ) )
213186, 212syl5bb 248 . . . . . . . . 9  |-  ( n  =  1  ->  ( E. g  e.  S  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) ) )
214166, 213syl5bb 248 . . . . . . . 8  |-  ( n  =  1  ->  (
( X E Y )  e.  ran  (
g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  ( ( V  X.  V )  ^m  {
1 } ) ( ( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) ) )
215214rspcev 2884 . . . . . . 7  |-  ( ( 1  e.  NN  /\  E. g  e.  ( ( V  X.  V )  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) )  /\  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  g ) ) ) )  ->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
21683, 163, 215sylancr 644 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) )
217 eliun 3909 . . . . . 6  |-  ( ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  <->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
218216, 217sylibr 203 . . . . 5  |-  ( ph  ->  ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) )
219218, 20syl6eleqr 2374 . . . 4  |-  ( ph  ->  ( X E Y )  e.  T )
220 infmxrlb 10652 . . . 4  |-  ( ( T  C_  RR*  /\  ( X E Y )  e.  T )  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
22182, 219, 220syl2anc 642 . . 3  |-  ( ph  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
22220eleq2i 2347 . . . . . . 7  |-  ( p  e.  T  <->  p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
223 eliun 3909 . . . . . . 7  |-  ( p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
224222, 223bitri 240 . . . . . 6  |-  ( p  e.  T  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
225 vex 2791 . . . . . . . . 9  |-  p  e. 
_V
22675elrnmpt 4926 . . . . . . . . 9  |-  ( p  e.  _V  ->  (
p  e.  ran  (
g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  p  =  ( RR* s  gsumg  ( E  o.  g
) ) ) )
227225, 226ax-mp 8 . . . . . . . 8  |-  ( p  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  p  =  ( RR* s  gsumg  ( E  o.  g
) ) )
228184, 17elrab2 2925 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  S  <->  ( g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) )  /\  ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) ) )
229228simprbi 450 . . . . . . . . . . . . . . . 16  |-  ( g  e.  S  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
230229adantl 452 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
231230simp2d 968 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )
2323ad2antrr 706 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-onto-> B )
233 f1of1 5471 . . . . . . . . . . . . . . . 16  |-  ( F : V -1-1-onto-> B  ->  F : V -1-1-> B )
234232, 233syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-> B )
235 simplr 731 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  NN )
236 elfz1end 10820 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  <->  n  e.  ( 1 ... n
) )
237235, 236sylib 188 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( 1 ... n
) )
238 ffvelrn 5663 . . . . . . . . . . . . . . . . 17  |-  ( ( g : ( 1 ... n ) --> ( V  X.  V )  /\  n  e.  ( 1 ... n ) )  ->  ( g `  n )  e.  ( V  X.  V ) )
23952, 237, 238syl2anc 642 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  n )  e.  ( V  X.  V
) )
240 xp2nd 6150 . . . . . . . . . . . . . . . 16  |-  ( ( g `  n )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  n ) )  e.  V )
241239, 240syl 15 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  e.  V )
24214ad2antrr 706 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  Y  e.  V )
243 f1fveq 5786 . . . . . . . . . . . . . . 15  |-  ( ( F : V -1-1-> B  /\  ( ( 2nd `  (
g `  n )
)  e.  V  /\  Y  e.  V )
)  ->  ( ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  <->  ( 2nd `  (
g `  n )
)  =  Y ) )
244234, 241, 242, 243syl12anc 1180 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( 2nd `  ( g `  n
) )  =  Y ) )
245231, 244mpbid 201 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  =  Y )
246245oveq2d 5874 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  n )
) )  =  ( X E Y ) )
247 eleq1 2343 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  e.  ( 1 ... n )  <->  1  e.  ( 1 ... n
) ) )
248 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
g `  m )  =  ( g ` 
1 ) )
249248fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  1 )
) )
250249oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  1
) ) ) )
251 oveq2 5866 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
252251, 190syl6eq 2331 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
253252reseq2d 4955 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  { 1 } ) )
254253oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
255250, 254breq12d 4036 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
( X E ( 2nd `  ( g `
 m ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... m ) ) )  <-> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) )
256247, 255imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( m  =  1  ->  (
( m  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) )  <->  ( 1  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) ) ) ) )
257256imbi2d 307 . . . . . . . . . . . . . . 15  |-  ( m  =  1  ->  (
( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  ->  ( m  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) ) )  <->  ( (
( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) ) ) )
258 eleq1 2343 . . . . . . . . . . . . . . . . 17  |-  ( m  =  x  ->  (
m  e.  ( 1 ... n )  <->  x  e.  ( 1 ... n
) ) )
259 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
g `  m )  =  ( g `  x ) )
260259fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  x )
) )
261260oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  x
) ) ) )
262 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
1 ... m )  =  ( 1 ... x
) )
263262reseq2d 4955 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... x ) ) )
264263oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) )
265261, 264breq12d 4036 . . . . . . . . . . . . . . . . 17  |-  ( m  =  x  ->  (
( X E ( 2nd `  ( g `
 m ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... m ) ) )  <-> 
( X E ( 2nd `  ( g `
 x ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... x ) ) ) ) )
266258, 265imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( m  =  x  ->  (
( m  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) )  <->  ( x  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  x )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) ) ) )
267266imbi2d 307 . . . . . . . . . . . . . . 15  |-  ( m  =  x  ->  (
( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  ->  ( m  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) ) )  <->  ( (
( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
x  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... x ) ) ) ) ) ) )
268 eleq1 2343 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( x  + 
1 )  ->  (
m  e.  ( 1 ... n )  <->  ( x  +  1 )  e.  ( 1 ... n
) ) )
269 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
g `  m )  =  ( g `  ( x  +  1
) ) )
270269fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  ( x  +  1 ) ) ) )
271270oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) )
272 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
1 ... m )  =  ( 1 ... (
x  +  1 ) ) )
273272reseq2d 4955 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) )
274273oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) ) )
275271, 274breq12d 4036 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( x  + 
1 )  ->  (
( X E ( 2nd `  ( g `
 m ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... m ) ) )  <-> 
( X E ( 2nd `  ( g `
 ( x  + 
1 ) ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... ( x  +  1 ) ) ) ) ) )
276268, 275imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( m  =  ( x  + 
1 )  ->  (
( m  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) )  <->  ( (
x  +  1 )  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  ( x  +  1 ) ) ) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) ) ) ) )
277276imbi2d 307 . . . . . . . . . . . . . . 15  |-  ( m  =  ( x  + 
1 )  ->  (
( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  ->  ( m  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) ) )  <->  ( (
( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( x  +  1 )  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 ( x  + 
1 ) ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... ( x  +  1 ) ) ) ) ) ) ) )
278 eleq1 2343 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
m  e.  ( 1 ... n )  <->  n  e.  ( 1 ... n
) ) )
279 fveq2 5525 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
280279fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  n )
) )
281280oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  n
) ) ) )
282 oveq2 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
1 ... m )  =  ( 1 ... n
) )
283282reseq2d 4955 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... n ) ) )
284283oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... n ) ) ) )
285281, 284breq12d 4036 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
( X E ( 2nd `  ( g `
 m ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... m ) ) )  <-> 
( X E ( 2nd `  ( g `
 n ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... n ) ) ) ) )
286278, 285imbi12d 311 . . . . . . . . . . . . . . . 16  |-  ( m  =  n  ->  (
( m  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) )  <->  ( n  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  n )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... n ) ) ) ) ) )
287286imbi2d 307 . . . . . . . . . . . . . . 15  |-  ( m  =  n  ->  (
( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  ->  ( m  e.  ( 1 ... n
)  ->  ( X E ( 2nd `  (
g `  m )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) ) ) )  <->  ( (
( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
n  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 n ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... n ) ) ) ) ) ) )
28831ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E  e.  ( * Met `  V
) )
28911ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  X  e.  V )
290 nnuz 10263 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
291235, 290syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( ZZ>= `  1 )
)
292 eluzfz1 10803 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... n
) )
293291, 292syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  ( 1 ... n
) )
294 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( g : ( 1 ... n ) --> ( V  X.  V )  /\  1  e.  ( 1 ... n ) )  ->  ( g `  1 )  e.  ( V  X.  V
) )
29552, 293, 294syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  e.  ( V  X.  V
) )
296 xp2nd 6150 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
297295, 296syl 15 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
298 xmetcl 17896 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  1 )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
299288, 289, 297, 298syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
300 xrleid 10484 . . . . . . . . . . . . . . . . . 18  |-  ( ( X E ( 2nd `  ( g `  1
) ) )  e. 
RR*  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
301299, 300syl 15 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
302142ad2antrr 706 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e.  Mnd )
30383a1i 10 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  NN )
304 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E : ( V  X.  V ) --> (
RR*  \  {  -oo }
)  /\  ( g `  1 )  e.  ( V  X.  V
) )  ->  ( E `  ( g `  1 ) )  e.  ( RR*  \  {  -oo } ) )
30546, 295, 304syl2anc 642 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  ( g `  1 ) )  e.  ( RR*  \  {  -oo } ) )
306 fveq2 5525 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  1  ->  (
g `  j )  =  ( g ` 
1 ) )
307306fveq2d 5529 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  1  ->  ( E `  ( g `  j ) )  =  ( E `  (
g `  1 )
) )
30867, 307gsumsn 15220 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( E `  ( g `  1 ) )  e.  ( RR*  \  {  -oo } ) )  -> 
( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
309302, 303, 305, 308syl3anc 1182 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
310288, 32syl 15 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> RR* )
311 fcompt 5694 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E : ( V  X.  V ) --> RR* 
/\  g : ( 1 ... n ) --> ( V  X.  V
) )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
312310, 52, 311syl2anc 642 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
313312reseq1d 4954 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( ( j  e.  ( 1 ... n )  |->  ( E `  ( g `
 j ) ) )  |`  { 1 } ) )
314293snssd 3760 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  { 1 }  C_  ( 1 ... n ) )
315 resmpt 5000 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { 1 }  C_  (
1 ... n )  -> 
( ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) )  |`  { 1 } )  =  ( j  e. 
{ 1 }  |->  ( E `  ( g `
 j ) ) ) )
316314, 315syl 15 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( j  e.  ( 1 ... n ) 
|->  ( E `  (
g `  j )
) )  |`  { 1 } )  =  ( j  e.  { 1 }  |->  ( E `  ( g `  j
) ) ) )
317313, 316eqtrd 2315 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( j  e.  { 1 } 
|->  ( E `  (
g `  j )
) ) )
318317oveq2d 5874 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) ) )
319 df-ov 5861 . . . . . . . . . . . . . . . . . . 19  |-  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )
320 1st2nd2 6159 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
321295, 320syl 15 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
322230simp1d 967 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
) )
323 xp1st 6149 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
324295, 323syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
325 f1fveq 5786 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : V -1-1-> B  /\  ( ( 1st `  (
g `  1 )
)  e.  V  /\  X  e.  V )
)  ->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  <->  ( 1st `  (
g `  1 )
)  =  X ) )
326234, 324, 289, 325syl12anc 1180 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( 1st `  ( g `  1
) )  =  X ) )
327322, 326mpbid 201 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  =  X )
328327opeq1d 3802 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. ( 1st `  ( g ` 
1 ) ) ,  ( 2nd `  (
g `  1 )
) >.  =  <. X , 
( 2nd `  (
g `  1 )
) >. )
329321, 328eqtr2d 2316 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. X , 
( 2nd `  (
g `  1 )
) >.  =  ( g `
 1 ) )
330329fveq2d 5529 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )  =  ( E `  ( g `
 1 ) ) )
331319, 330syl5eq 2327 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  ( g `
 1 ) ) )
332309, 318, 3313eqtr4d 2325 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( X E ( 2nd `  ( g `
 1 ) ) ) )
333301, 332breqtrrd 4049 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
334333a1d 22 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) )
335 simprl 732 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  NN )
336335, 290syl6eleq 2373 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( ZZ>= ` 
1 ) )
337 simprr 733 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( x  +  1 )  e.  ( 1 ... n ) )
338 peano2fzr 10808 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( ZZ>= ` 
1 )  /\  (
x  +  1 )  e.  ( 1 ... n ) )  ->  x  e.  ( 1 ... n ) )
339336, 337, 338syl2anc 642 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( 1 ... n ) )
340339expr 598 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  NN )  ->  ( ( x  +  1 )  e.  ( 1 ... n )  ->  x  e.  ( 1 ... n
) ) )
341340imim1d 69 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  NN )  ->  ( ( x  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... x ) ) ) )  ->  ( (
x  +  1 )  e.  ( 1 ... n )  ->  ( X E ( 2nd `  (
g `  x )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) ) ) )
342288adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E  e.  ( * Met `  V ) )
343289adantr 451 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  X  e.  V )
34452adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
g : ( 1 ... n ) --> ( V  X.  V ) )
345 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g : ( 1 ... n ) --> ( V  X.  V )  /\  x  e.  ( 1 ... n ) )  ->  ( g `  x )  e.  ( V  X.  V ) )
346344, 339, 345syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  x
)  e.  ( V  X.  V ) )
347 xp2nd 6150 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  x )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  x ) )  e.  V )
348346, 347syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  x )
)  e.  V )
349 xmetcl 17896 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  x )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  x )
) )  e.  RR* )
350342, 343, 348, 349syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  e.  RR* )
35169a1i 10 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  W  e. CMnd )
352 fzfid 11035 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  e.  Fin )
35354adantr 451 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
) )
354 ssun1 3338 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( 1 ... x )  C_  ( ( 1 ... x )  u.  {
( x  +  1 ) } )
355 fzsuc 10835 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( x  + 
1 ) )  =  ( ( 1 ... x )  u.  {
( x  +  1 ) } ) )
356336, 355syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  =  ( ( 1 ... x )  u.  { ( x  +  1 ) } ) )
357 elfzuz3 10795 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  +  1 )  e.  ( 1 ... n )  ->  n  e.  ( ZZ>= `  ( x  +  1 ) ) )
358357ad2antll 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  n  e.  ( ZZ>= `  ( x  +  1
) ) )
359 fzss2 10831 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  ( ZZ>= `  (
x  +  1 ) )  ->  ( 1 ... ( x  + 
1 ) )  C_  ( 1 ... n
) )
360358, 359syl 15 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  C_  ( 1 ... n ) )
361356, 360eqsstr3d 3213 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( 1 ... x )  u.  {
( x  +  1 ) } )  C_  ( 1 ... n
) )
362354, 361syl5ss 3190 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  C_  ( 1 ... n ) )
363 fssres 5408 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
)  /\  ( 1 ... x )  C_  ( 1 ... n
) )  ->  (
( E  o.  g
)  |`  ( 1 ... x ) ) : ( 1 ... x
) --> ( RR*  \  {  -oo } ) )
364353, 362, 363syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( E  o.  g )  |`  (
1 ... x ) ) : ( 1 ... x ) --> ( RR*  \  {  -oo } ) )
365352, 364fisuppfi 14450 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( `' ( ( E  o.  g )  |`  ( 1 ... x
) ) " ( _V  \  { 0 } ) )  e.  Fin )
36667, 68, 351, 352, 364, 365gsumcl 15198 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) )  e.  ( RR*  \  {  -oo } ) )
36723, 366sseldi 3178 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) )  e.  RR* )
368342, 32syl 15 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E : ( V  X.  V ) --> RR* )
369 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g : ( 1 ... n ) --> ( V  X.  V )  /\  ( x  + 
1 )  e.  ( 1 ... n ) )  ->  ( g `  ( x  +  1 ) )  e.  ( V  X.  V ) )
370344, 337, 369syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  (
x  +  1 ) )  e.  ( V  X.  V ) )
371 ffvelrn 5663 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E : ( V  X.  V ) --> RR* 
/\  ( g `  ( x  +  1
) )  e.  ( V  X.  V ) )  ->  ( E `  ( g `  (
x  +  1 ) ) )  e.  RR* )
372368, 370, 371syl2anc 642 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E `  (
g `  ( x  +  1 ) ) )  e.  RR* )
373 xleadd1a 10573 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( X E ( 2nd `  (
g `  x )
) )  e.  RR*  /\  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) )  e.  RR*  /\  ( E `  ( g `  ( x  +  1 ) ) )  e. 
RR* )  /\  ( X E ( 2nd `  (
g `  x )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) )  ->  (
( X E ( 2nd `  ( g `
 x ) ) ) + e ( E `  ( g `
 ( x  + 
1 ) ) ) )  <_  ( ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) + e ( E `  ( g `
 ( x  + 
1 ) ) ) ) )
374373ex 423 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( X E ( 2nd `  ( g `
 x ) ) )  e.  RR*  /\  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) )  e.  RR*  /\  ( E `  ( g `  ( x  +  1 ) ) )  e. 
RR* )  ->  (
( X E ( 2nd `  ( g `
 x ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  ( 1 ... x ) ) )  ->  ( ( X E ( 2nd `  (
g `  x )
) ) + e
( E `  (
g `  ( x  +  1 ) ) ) )  <_  (
( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) + e ( E `  ( g `
 ( x  + 
1 ) ) ) ) ) )
375350, 367, 372, 374syl3anc 1182 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( X E ( 2nd `  (
g `  x )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) )  ->  ( ( X E ( 2nd `  (
g `  x )
) ) + e
( E `  (
g `  ( x  +  1 ) ) ) )  <_  (
( W  gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) + e ( E `  ( g `
 ( x  + 
1 ) ) ) ) ) )
376 xp2nd 6150 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  ( x  +  1
) ) )  e.  V )
377370, 376syl 15 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  ( x  +  1 ) ) )  e.  V )
378