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

Theorem imasdsf1olem 18312
Description: Lemma for imasdsf1o 18313. (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 5622 . . . . 5  |-  ( F : V -1-1-onto-> B  ->  F : V -onto-> B )
53, 4syl 16 . . . 4  |-  ( ph  ->  F : V -onto-> B
)
6 imasdsf1o.r . . . 4  |-  ( ph  ->  R  e.  Z )
7 eqid 2388 . . . 4  |-  ( dist `  R )  =  (
dist `  R )
8 imasdsf1o.d . . . 4  |-  D  =  ( dist `  U
)
9 f1of 5615 . . . . . 6  |-  ( F : V -1-1-onto-> B  ->  F : V
--> B )
103, 9syl 16 . . . . 5  |-  ( ph  ->  F : V --> B )
11 imasdsf1o.x . . . . 5  |-  ( ph  ->  X  e.  V )
1210, 11ffvelrnd 5811 . . . 4  |-  ( ph  ->  ( F `  X
)  e.  B )
13 imasdsf1o.y . . . . 5  |-  ( ph  ->  Y  e.  V )
1410, 13ffvelrnd 5811 . . . 4  |-  ( ph  ->  ( F `  Y
)  e.  B )
15 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 ) ) ) ) ) }
16 imasdsf1o.e . . . 4  |-  E  =  ( ( dist `  R
)  |`  ( V  X.  V ) )
171, 2, 5, 6, 7, 8, 12, 14, 15, 16imasdsval2 13670 . . 3  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  sup ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) ,  RR* ,  `'  <  ) )
18 imasdsf1o.t . . . 4  |-  T  = 
U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )
1918supeq1i 7388 . . 3  |-  sup ( T ,  RR* ,  `'  <  )  =  sup ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) ,  RR* ,  `'  <  )
2017, 19syl6eqr 2438 . 2  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  sup ( T ,  RR* ,  `'  <  ) )
21 xrsbas 16641 . . . . . . . . . . . 12  |-  RR*  =  ( Base `  RR* s )
22 xrsadd 16642 . . . . . . . . . . . 12  |-  + e  =  ( +g  `  RR* s
)
23 imasdsf1o.w . . . . . . . . . . . 12  |-  W  =  ( RR* ss  ( RR*  \  {  -oo } ) )
24 xrsex 16640 . . . . . . . . . . . . 13  |-  RR* s  e.  _V
2524a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  RR* s  e.  _V )
26 fzfid 11240 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1 ... n )  e. 
Fin )
27 difss 3418 . . . . . . . . . . . . 13  |-  ( RR*  \  {  -oo } ) 
C_  RR*
2827a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*  \  {  -oo }
)  C_  RR* )
29 imasdsf1o.m . . . . . . . . . . . . . . . 16  |-  ( ph  ->  E  e.  ( * Met `  V ) )
30 xmetf 18269 . . . . . . . . . . . . . . . 16  |-  ( E  e.  ( * Met `  V )  ->  E : ( V  X.  V ) --> RR* )
31 ffn 5532 . . . . . . . . . . . . . . . 16  |-  ( E : ( V  X.  V ) --> RR*  ->  E  Fn  ( V  X.  V ) )
3229, 30, 313syl 19 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  Fn  ( V  X.  V ) )
33 xmetcl 18271 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e. 
RR* )
34 xmetge0 18284 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  0  <_  ( f E g ) )
35 ge0nemnf 10694 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f E g )  e.  RR*  /\  0  <_  ( f E g ) )  ->  (
f E g )  =/=  -oo )
3633, 34, 35syl2anc 643 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  =/= 
-oo )
37 eldifsn 3871 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f E g )  e.  ( RR*  \  {  -oo } )  <->  ( (
f E g )  e.  RR*  /\  (
f E g )  =/=  -oo ) )
3833, 36, 37sylanbrc 646 . . . . . . . . . . . . . . . . . 18  |-  ( ( E  e.  ( * Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e.  ( RR*  \  {  -oo } ) )
39383expb 1154 . . . . . . . . . . . . . . . . 17  |-  ( ( E  e.  ( * Met `  V )  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  {  -oo } ) )
4029, 39sylan 458 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  {  -oo } ) )
4140ralrimivva 2742 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. f  e.  V  A. g  e.  V  ( f E g )  e.  ( RR*  \  {  -oo } ) )
42 ffnov 6114 . . . . . . . . . . . . . . 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 } ) ) )
4332, 41, 42sylanbrc 646 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : ( V  X.  V ) --> (
RR*  \  {  -oo }
) )
4443ad2antrr 707 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> ( RR*  \  {  -oo } ) )
45 ssrab2 3372 . . . . . . . . . . . . . . . . 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 ) )
4615, 45eqsstri 3322 . . . . . . . . . . . . . . . 16  |-  S  C_  ( ( V  X.  V )  ^m  (
1 ... n ) )
4746a1i 11 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  n  e.  NN )  ->  S  C_  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
4847sselda 3292 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
49 elmapi 6975 . . . . . . . . . . . . . 14  |-  ( g  e.  ( ( V  X.  V )  ^m  ( 1 ... n
) )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
5048, 49syl 16 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
51 fco 5541 . . . . . . . . . . . . 13  |-  ( ( E : ( V  X.  V ) --> (
RR*  \  {  -oo }
)  /\  g :
( 1 ... n
) --> ( V  X.  V ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
) )
5244, 50, 51syl2anc 643 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) : ( 1 ... n ) --> ( RR*  \  {  -oo } ) )
53 0re 9025 . . . . . . . . . . . . 13  |-  0  e.  RR
54 rexr 9064 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  e.  RR* )
55 renemnf 9067 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  =/=  -oo )
56 eldifsn 3871 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( RR*  \  {  -oo } )  <->  ( 0  e.  RR*  /\  0  =/=  -oo ) )
5754, 55, 56sylanbrc 646 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  0  e.  ( RR*  \  {  -oo } ) )
5853, 57mp1i 12 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  0  e.  ( RR*  \  {  -oo } ) )
59 xaddid2 10759 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( 0 + e x )  =  x )
60 xaddid1 10758 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( x + e 0 )  =  x )
6159, 60jca 519 . . . . . . . . . . . . 13  |-  ( x  e.  RR*  ->  ( ( 0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
6261adantl 453 . . . . . . . . . . . 12  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  RR* )  ->  ( (
0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
6321, 22, 23, 25, 26, 28, 52, 58, 62gsumress 14705 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  =  ( W  gsumg  ( E  o.  g
) ) )
6423, 21ressbas2 13448 . . . . . . . . . . . . 13  |-  ( (
RR*  \  {  -oo }
)  C_  RR*  ->  ( RR*  \  {  -oo }
)  =  ( Base `  W ) )
6527, 64ax-mp 8 . . . . . . . . . . . 12  |-  ( RR*  \  {  -oo } )  =  ( Base `  W
)
6623xrs10 16661 . . . . . . . . . . . 12  |-  0  =  ( 0g `  W )
6723xrs1cmn 16662 . . . . . . . . . . . . 13  |-  W  e. CMnd
6867a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e. CMnd )
6926, 52fisuppfi 14701 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( `' ( E  o.  g ) " ( _V  \  { 0 } ) )  e.  Fin )
7065, 66, 68, 26, 52, 69gsumcl 15449 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( E  o.  g
) )  e.  (
RR*  \  {  -oo }
) )
7163, 70eqeltrd 2462 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  e.  (
RR*  \  {  -oo }
) )
7271eldifad 3276 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR* s  gsumg  ( E  o.  g
) )  e.  RR* )
73 eqid 2388 . . . . . . . . 9  |-  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  =  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )
7472, 73fmptd 5833 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) : S --> RR* )
75 frn 5538 . . . . . . . 8  |-  ( ( g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) ) : S --> RR*  ->  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7674, 75syl 16 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
g  e.  S  |->  (
RR* s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7776ralrimiva 2733 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )  C_  RR* )
78 iunss 4074 . . . . . 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* )
7977, 78sylibr 204 . . . . 5  |-  ( ph  ->  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) )  C_  RR* )
8018, 79syl5eqss 3336 . . . 4  |-  ( ph  ->  T  C_  RR* )
81 1nn 9944 . . . . . . 7  |-  1  e.  NN
82 1ex 9020 . . . . . . . . . . . 12  |-  1  e.  _V
83 opex 4369 . . . . . . . . . . . 12  |-  <. X ,  Y >.  e.  _V
8482, 83f1osn 5656 . . . . . . . . . . 11  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } -1-1-onto-> { <. X ,  Y >. }
85 f1of 5615 . . . . . . . . . . 11  |-  ( {
<. 1 ,  <. X ,  Y >. >. } : { 1 } -1-1-onto-> { <. X ,  Y >. }  ->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. } )
8684, 85ax-mp 8 . . . . . . . . . 10  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. }
87 opelxpi 4851 . . . . . . . . . . . 12  |-  ( ( X  e.  V  /\  Y  e.  V )  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
8811, 13, 87syl2anc 643 . . . . . . . . . . 11  |-  ( ph  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
8988snssd 3887 . . . . . . . . . 10  |-  ( ph  ->  { <. X ,  Y >. }  C_  ( V  X.  V ) )
90 fss 5540 . . . . . . . . . 10  |-  ( ( { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> { <. X ,  Y >. }  /\  {
<. X ,  Y >. } 
C_  ( V  X.  V ) )  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9186, 89, 90sylancr 645 . . . . . . . . 9  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9229elfvexd 5700 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  _V )
93 xpexg 4930 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  V  e.  _V )  ->  ( V  X.  V
)  e.  _V )
9492, 92, 93syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( V  X.  V
)  e.  _V )
95 snex 4347 . . . . . . . . . 10  |-  { 1 }  e.  _V
96 elmapg 6968 . . . . . . . . . 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 ) ) )
9794, 95, 96sylancl 644 . . . . . . . . 9  |-  ( ph  ->  ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V
)  ^m  { 1 } )  <->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> ( V  X.  V ) ) )
9891, 97mpbird 224 . . . . . . . 8  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V )  ^m  {
1 } ) )
99 op1stg 6299 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 1st `  <. X ,  Y >. )  =  X )
10011, 13, 99syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  <. X ,  Y >. )  =  X )
101100fveq2d 5673 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X ) )
102 op2ndg 6300 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
10311, 13, 102syl2anc 643 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
104103fveq2d 5673 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) )
105101, 104jca 519 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
10624a1i 11 . . . . . . . . . . 11  |-  ( ph  -> 
RR* s  e.  _V )
107 snfi 7124 . . . . . . . . . . . 12  |-  { 1 }  e.  Fin
108107a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  { 1 }  e.  Fin )
10927a1i 11 . . . . . . . . . . 11  |-  ( ph  ->  ( RR*  \  {  -oo } )  C_  RR* )
110 xmetcl 18271 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  ( X E Y )  e.  RR* )
11129, 11, 13, 110syl3anc 1184 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X E Y )  e.  RR* )
112 xmetge0 18284 . . . . . . . . . . . . . . . 16  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  0  <_  ( X E Y ) )
11329, 11, 13, 112syl3anc 1184 . . . . . . . . . . . . . . 15  |-  ( ph  ->  0  <_  ( X E Y ) )
114 ge0nemnf 10694 . . . . . . . . . . . . . . 15  |-  ( ( ( X E Y )  e.  RR*  /\  0  <_  ( X E Y ) )  ->  ( X E Y )  =/= 
-oo )
115111, 113, 114syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( X E Y )  =/=  -oo )
116 eldifsn 3871 . . . . . . . . . . . . . 14  |-  ( ( X E Y )  e.  ( RR*  \  {  -oo } )  <->  ( ( X E Y )  e. 
RR*  /\  ( X E Y )  =/=  -oo ) )
117111, 115, 116sylanbrc 646 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X E Y )  e.  ( RR*  \  {  -oo } ) )
118 fconst6g 5573 . . . . . . . . . . . . 13  |-  ( ( X E Y )  e.  ( RR*  \  {  -oo } )  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  {  -oo } ) )
119117, 118syl 16 . . . . . . . . . . . 12  |-  ( ph  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  {  -oo } ) )
120 fcoconst 5845 . . . . . . . . . . . . . . 15  |-  ( ( E  Fn  ( V  X.  V )  /\  <. X ,  Y >.  e.  ( V  X.  V
) )  ->  ( E  o.  ( {
1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `  <. X ,  Y >. ) } ) )
12132, 88, 120syl2anc 643 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `
 <. X ,  Y >. ) } ) )
12282, 83xpsn 5850 . . . . . . . . . . . . . . 15  |-  ( { 1 }  X.  { <. X ,  Y >. } )  =  { <. 1 ,  <. X ,  Y >. >. }
123122coeq2i 4974 . . . . . . . . . . . . . 14  |-  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )
124 df-ov 6024 . . . . . . . . . . . . . . . . 17  |-  ( X E Y )  =  ( E `  <. X ,  Y >. )
125124eqcomi 2392 . . . . . . . . . . . . . . . 16  |-  ( E `
 <. X ,  Y >. )  =  ( X E Y )
126125sneqi 3770 . . . . . . . . . . . . . . 15  |-  { ( E `  <. X ,  Y >. ) }  =  { ( X E Y ) }
127126xpeq2i 4840 . . . . . . . . . . . . . 14  |-  ( { 1 }  X.  {
( E `  <. X ,  Y >. ) } )  =  ( { 1 }  X.  { ( X E Y ) } )
128121, 123, 1273eqtr3g 2443 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( { 1 }  X.  { ( X E Y ) } ) )
129128feq1d 5521 . . . . . . . . . . . 12  |-  ( ph  ->  ( ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  {  -oo } )  <->  ( { 1 }  X.  { ( X E Y ) } ) : {
1 } --> ( RR*  \  {  -oo } ) ) )
130119, 129mpbird 224 . . . . . . . . . . 11  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  {  -oo } ) )
13153, 57mp1i 12 . . . . . . . . . . 11  |-  ( ph  ->  0  e.  ( RR*  \  {  -oo } ) )
13261adantl 453 . . . . . . . . . . 11  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
0 + e x )  =  x  /\  ( x + e
0 )  =  x ) )
13321, 22, 23, 106, 108, 109, 130, 131, 132gsumress 14705 . . . . . . . . . 10  |-  ( ph  ->  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
134 fconstmpt 4862 . . . . . . . . . . . 12  |-  ( { 1 }  X.  {
( X E Y ) } )  =  ( j  e.  {
1 }  |->  ( X E Y ) )
135128, 134syl6eq 2436 . . . . . . . . . . 11  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( j  e.  {
1 }  |->  ( X E Y ) ) )
136135oveq2d 6037 . . . . . . . . . 10  |-  ( ph  ->  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
137133, 136eqtrd 2420 . . . . . . . . 9  |-  ( ph  ->  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
138 cmnmnd 15355 . . . . . . . . . . 11  |-  ( W  e. CMnd  ->  W  e.  Mnd )
13967, 138mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  W  e.  Mnd )
14081a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  NN )
141 eqidd 2389 . . . . . . . . . . 11  |-  ( j  =  1  ->  ( X E Y )  =  ( X E Y ) )
14265, 141gsumsn 15471 . . . . . . . . . 10  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( X E Y )  e.  ( RR*  \  {  -oo } ) )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
143139, 140, 117, 142syl3anc 1184 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
144137, 143eqtr2d 2421 . . . . . . . 8  |-  ( ph  ->  ( X E Y )  =  ( RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
145 fveq1 5668 . . . . . . . . . . . . . . 15  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  ( { <. 1 ,  <. X ,  Y >. >. } `  1
) )
14682, 83fvsn 5866 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  <. X ,  Y >. >. } ` 
1 )  =  <. X ,  Y >.
147145, 146syl6eq 2436 . . . . . . . . . . . . . 14  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  <. X ,  Y >. )
148147fveq2d 5673 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 1st `  ( g ` 
1 ) )  =  ( 1st `  <. X ,  Y >. )
)
149148fveq2d 5673 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  ( 1st `  <. X ,  Y >. ) ) )
150149eqeq1d 2396 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  <. X ,  Y >. )
)  =  ( F `
 X ) ) )
151147fveq2d 5673 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 2nd `  ( g ` 
1 ) )  =  ( 2nd `  <. X ,  Y >. )
)
152151fveq2d 5673 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  ( 2nd `  <. X ,  Y >. ) ) )
153152eqeq1d 2396 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 2nd `  ( g ` 
1 ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
154150, 153anbi12d 692 . . . . . . . . . 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 ) ) ) )
155 coeq2 4972 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( E  o.  g )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )
156155oveq2d 6037 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( RR* s  gsumg  ( E  o.  g
) )  =  (
RR* s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
157156eqeq2d 2399 . . . . . . . . . 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 >. >. } ) ) ) )
158154, 157anbi12d 692 . . . . . . . . 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 >. >. } ) ) ) ) )
159158rspcev 2996 . . . . . . . 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 ) ) ) )
16098, 105, 144, 159syl12anc 1182 . . . . . . 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 ) ) ) )
161 ovex 6046 . . . . . . . . . 10  |-  ( X E Y )  e. 
_V
16273elrnmpt 5058 . . . . . . . . . 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
) ) ) )
163161, 162ax-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
) ) )
16415rexeqi 2853 . . . . . . . . . . 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
) ) )
165 fveq1 5668 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  1 )  =  ( g ` 
1 ) )
166165fveq2d 5673 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 1st `  ( h ` 
1 ) )  =  ( 1st `  (
g `  1 )
) )
167166fveq2d 5673 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  1
) ) )  =  ( F `  ( 1st `  ( g ` 
1 ) ) ) )
168167eqeq1d 2396 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 1st `  ( h ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  (
g `  1 )
) )  =  ( F `  X ) ) )
169 fveq1 5668 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  n )  =  ( g `  n ) )
170169fveq2d 5673 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 2nd `  ( h `  n ) )  =  ( 2nd `  (
g `  n )
) )
171170fveq2d 5673 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  ( 2nd `  ( g `  n ) ) ) )
172171eqeq1d 2396 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y ) ) )
173 fveq1 5668 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  i )  =  ( g `  i ) )
174173fveq2d 5673 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 2nd `  ( h `  i ) )  =  ( 2nd `  (
g `  i )
) )
175174fveq2d 5673 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 2nd `  ( g `  i ) ) ) )
176 fveq1 5668 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  ( i  +  1 ) )  =  ( g `  ( i  +  1 ) ) )
177176fveq2d 5673 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 1st `  ( h `  ( i  +  1 ) ) )  =  ( 1st `  (
g `  ( i  +  1 ) ) ) )
178177fveq2d 5673 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  (
i  +  1 ) ) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )
179175, 178eqeq12d 2402 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  i ) ) )  =  ( F `  ( 1st `  ( h `
 ( i  +  1 ) ) ) )  <->  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
180179ralbidv 2670 . . . . . . . . . . . . 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 ) ) ) ) ) )
181168, 172, 1803anbi123d 1254 . . . . . . . . . . . 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 ) ) ) ) ) ) )
182181rexrab 3042 . . . . . . . . . . 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 ) ) ) )
183164, 182bitri 241 . . . . . . . . . 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 ) ) ) )
184 oveq2 6029 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
185 1z 10244 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
186 fzsn 11027 . . . . . . . . . . . . . 14  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
187185, 186ax-mp 8 . . . . . . . . . . . . 13  |-  ( 1 ... 1 )  =  { 1 }
188184, 187syl6eq 2436 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
1 ... n )  =  { 1 } )
189188oveq2d 6037 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( V  X.  V
)  ^m  ( 1 ... n ) )  =  ( ( V  X.  V )  ^m  { 1 } ) )
190 df-3an 938 . . . . . . . . . . . . 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 ) ) ) ) ) )
191 ral0 3676 . . . . . . . . . . . . . . . 16  |-  A. i  e.  (/)  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) )
192 oveq1 6028 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
193 1m1e0 10001 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  -  1 )  =  0
194192, 193syl6eq 2436 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
195194oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  ( 1 ... 0
) )
196 fz10 11008 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... 0 )  =  (/)
197195, 196syl6eq 2436 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  (/) )
198197raleqdv 2854 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
199191, 198mpbiri 225 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )
200199biantrud 494 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
201 fveq2 5669 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
g `  n )  =  ( g ` 
1 ) )
202201fveq2d 5673 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( 2nd `  ( g `  n ) )  =  ( 2nd `  (
g `  1 )
) )
203202fveq2d 5673 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  ( 2nd `  ( g ` 
1 ) ) ) )
204203eqeq1d 2396 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) )
205204anbi2d 685 . . . . . . . . . . . . . 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 ) ) ) )
206200, 205bitr3d 247 . . . . . . . . . . . . 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 ) ) ) )
207190, 206syl5bb 249 . . . . . . . . . . . 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 ) ) ) )
208207anbi1d 686 . . . . . . . . . . 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 ) ) ) ) )
209189, 208rexeqbidv 2861 . . . . . . . . . 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 ) ) ) ) )
210183, 209syl5bb 249 . . . . . . . . 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 ) ) ) ) )
211163, 210syl5bb 249 . . . . . . . 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 ) ) ) ) )
212211rspcev 2996 . . . . . . 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 ) ) ) )
21381, 160, 212sylancr 645 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) )
214 eliun 4040 . . . . . 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 ) ) ) )
215213, 214sylibr 204 . . . . 5  |-  ( ph  ->  ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g
) ) ) )
216215, 18syl6eleqr 2479 . . . 4  |-  ( ph  ->  ( X E Y )  e.  T )
217 infmxrlb 10845 . . . 4  |-  ( ( T  C_  RR*  /\  ( X E Y )  e.  T )  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
21880, 216, 217syl2anc 643 . . 3  |-  ( ph  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
21918eleq2i 2452 . . . . . . 7  |-  ( p  e.  T  <->  p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
220 eliun 4040 . . . . . . 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 ) ) ) )
221219, 220bitri 241 . . . . . 6  |-  ( p  e.  T  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR* s  gsumg  ( E  o.  g ) ) ) )
222 vex 2903 . . . . . . . . 9  |-  p  e. 
_V
22373elrnmpt 5058 . . . . . . . . 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
) ) ) )
224222, 223ax-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
) ) )
225181, 15elrab2 3038 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
226225simprbi 451 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
227226adantl 453 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
228227simp2d 970 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )
2293ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-onto-> B )
230 f1of1 5614 . . . . . . . . . . . . . . . 16  |-  ( F : V -1-1-onto-> B  ->  F : V -1-1-> B )
231229, 230syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-> B )
232 simplr 732 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  NN )
233 elfz1end 11014 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  <->  n  e.  ( 1 ... n
) )
234232, 233sylib 189 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( 1 ... n
) )
23550, 234ffvelrnd 5811 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  n )  e.  ( V  X.  V
) )
236 xp2nd 6317 . . . . . . . . . . . . . . . 16  |-  ( ( g `  n )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  n ) )  e.  V )
237235, 236syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  e.  V )
23813ad2antrr 707 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  Y  e.  V )
239 f1fveq 5948 . . . . . . . . . . . . . . 15  |-  ( ( F : V -1-1-> B  /\  ( ( 2nd `  (
g `  n )
)  e.  V  /\  Y  e.  V )
)  ->  ( ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  <->  ( 2nd `  (
g `  n )
)  =  Y ) )
240231, 237, 238, 239syl12anc 1182 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( 2nd `  ( g `  n
) )  =  Y ) )
241228, 240mpbid 202 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  =  Y )
242241oveq2d 6037 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  n )
) )  =  ( X E Y ) )
243 eleq1 2448 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  e.  ( 1 ... n )  <->  1  e.  ( 1 ... n
) ) )
244 fveq2 5669 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
g `  m )  =  ( g ` 
1 ) )
245244fveq2d 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  1 )
) )
246245oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  1
) ) ) )
247 oveq2 6029 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
248247, 187syl6eq 2436 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
249248reseq2d 5087 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  { 1 } ) )
250249oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
251246, 250breq12d 4167 . . . . . . . . . . . . . . . . 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 } ) ) ) )
252243, 251imbi12d 312 . . . . . . . . . . . . . . . 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 } ) ) ) ) )
253252imbi2d 308 . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
254 eleq1 2448 . . . . . . . . . . . . . . . . 17  |-  ( m  =  x  ->  (
m  e.  ( 1 ... n )  <->  x  e.  ( 1 ... n
) ) )
255 fveq2 5669 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
g `  m )  =  ( g `  x ) )
256255fveq2d 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  x )
) )
257256oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  x
) ) ) )
258 oveq2 6029 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
1 ... m )  =  ( 1 ... x
) )
259258reseq2d 5087 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... x ) ) )
260259oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) )
261257, 260breq12d 4167 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
262254, 261imbi12d 312 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
263262imbi2d 308 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
264 eleq1 2448 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( x  + 
1 )  ->  (
m  e.  ( 1 ... n )  <->  ( x  +  1 )  e.  ( 1 ... n
) ) )
265 fveq2 5669 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
g `  m )  =  ( g `  ( x  +  1
) ) )
266265fveq2d 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  ( x  +  1 ) ) ) )
267266oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) )
268 oveq2 6029 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
1 ... m )  =  ( 1 ... (
x  +  1 ) ) )
269268reseq2d 5087 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) )
270269oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) ) )
271267, 270breq12d 4167 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
272264, 271imbi12d 312 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
273272imbi2d 308 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
274 eleq1 2448 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
m  e.  ( 1 ... n )  <->  n  e.  ( 1 ... n
) ) )
275 fveq2 5669 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
276275fveq2d 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  n )
) )
277276oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  n
) ) ) )
278 oveq2 6029 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
1 ... m )  =  ( 1 ... n
) )
279278reseq2d 5087 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... n ) ) )
280279oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... n ) ) ) )
281277, 280breq12d 4167 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
282274, 281imbi12d 312 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
283282imbi2d 308 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
28429ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E  e.  ( * Met `  V
) )
28511ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  X  e.  V )
286 nnuz 10454 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
287232, 286syl6eleq 2478 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( ZZ>= `  1 )
)
288 eluzfz1 10997 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... n
) )
289287, 288syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  ( 1 ... n
) )
29050, 289ffvelrnd 5811 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  e.  ( V  X.  V
) )
291 xp2nd 6317 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
292290, 291syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
293 xmetcl 18271 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  1 )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
294284, 285, 292, 293syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
295 xrleid 10676 . . . . . . . . . . . . . . . . . 18  |-  ( ( X E ( 2nd `  ( g `  1
) ) )  e. 
RR*  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
296294, 295syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
297139ad2antrr 707 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e.  Mnd )
29881a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  NN )
29944, 290ffvelrnd 5811 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  ( g `  1 ) )  e.  ( RR*  \  {  -oo } ) )
300 fveq2 5669 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  1  ->  (
g `  j )  =  ( g ` 
1 ) )
301300fveq2d 5673 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  1  ->  ( E `  ( g `  j ) )  =  ( E `  (
g `  1 )
) )
30265, 301gsumsn 15471 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( E `  ( g `  1 ) )  e.  ( RR*  \  {  -oo } ) )  -> 
( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
303297, 298, 299, 302syl3anc 1184 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
304284, 30syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> RR* )
305 fcompt 5844 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E : ( V  X.  V ) --> RR* 
/\  g : ( 1 ... n ) --> ( V  X.  V
) )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
306304, 50, 305syl2anc 643 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
307306reseq1d 5086 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( ( j  e.  ( 1 ... n )  |->  ( E `  ( g `
 j ) ) )  |`  { 1 } ) )
308289snssd 3887 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  { 1 }  C_  ( 1 ... n ) )
309 resmpt 5132 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { 1 }  C_  (
1 ... n )  -> 
( ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) )  |`  { 1 } )  =  ( j  e. 
{ 1 }  |->  ( E `  ( g `
 j ) ) ) )
310308, 309syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( j  e.  ( 1 ... n ) 
|->  ( E `  (
g `  j )
) )  |`  { 1 } )  =  ( j  e.  { 1 }  |->  ( E `  ( g `  j
) ) ) )
311307, 310eqtrd 2420 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( j  e.  { 1 } 
|->  ( E `  (
g `  j )
) ) )
312311oveq2d 6037 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) ) )
313 df-ov 6024 . . . . . . . . . . . . . . . . . . 19  |-  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )
314 1st2nd2 6326 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
315290, 314syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
316227simp1d 969 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
) )
317 xp1st 6316 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
318290, 317syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
319 f1fveq 5948 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : V -1-1-> B  /\  ( ( 1st `  (
g `  1 )
)  e.  V  /\  X  e.  V )
)  ->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  <->  ( 1st `  (
g `  1 )
)  =  X ) )
320231, 318, 285, 319syl12anc 1182 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( 1st `  ( g `  1
) )  =  X ) )
321316, 320mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  =  X )
322321opeq1d 3933 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. ( 1st `  ( g ` 
1 ) ) ,  ( 2nd `  (
g `  1 )
) >.  =  <. X , 
( 2nd `  (
g `  1 )
) >. )
323315, 322eqtr2d 2421 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. X , 
( 2nd `  (
g `  1 )
) >.  =  ( g `
 1 ) )
324323fveq2d 5673 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )  =  ( E `  ( g `
 1 ) ) )
325313, 324syl5eq 2432 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  ( g `
 1 ) ) )
326303, 312, 3253eqtr4d 2430 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( X E ( 2nd `  ( g `
 1 ) ) ) )
327296, 326breqtrrd 4180 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
328327a1d 23 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) )
329 simprl 733 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  NN )
330329, 286syl6eleq 2478 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( ZZ>= ` 
1 ) )
331 simprr 734 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( x  +  1 )  e.  ( 1 ... n ) )
332 peano2fzr 11002 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( ZZ>= ` 
1 )  /\  (
x  +  1 )  e.  ( 1 ... n ) )  ->  x  e.  ( 1 ... n ) )
333330, 331, 332syl2anc 643 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( 1 ... n ) )
334333expr 599 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  NN )  ->  ( ( x  +  1 )  e.  ( 1 ... n )  ->  x  e.  ( 1 ... n
) ) )
335334imim1d 71 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
336284adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E  e.  ( * Met `  V ) )
337285adantr 452 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  X  e.  V )
33850adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
g : ( 1 ... n ) --> ( V  X.  V ) )
339338, 333ffvelrnd 5811 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  x
)  e.  ( V  X.  V ) )
340 xp2nd 6317 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  x )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  x ) )  e.  V )
341339, 340syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  x )
)  e.  V )
342 xmetcl 18271 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E  e.  ( * Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  x )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  x )
) )  e.  RR* )
343336, 337, 341, 342syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  e.  RR* )
34467a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  W  e. CMnd )
345 fzfid 11240 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  e.  Fin )
34652adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
) )
347 fzsuc 11029 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( x  + 
1 ) )  =  ( ( 1 ... x )  u.  {
( x  +  1 ) } ) )
348330, 347syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  =  ( ( 1 ... x )  u.  { ( x  +  1 ) } ) )
349 elfzuz3 10989 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  +  1 )  e.  ( 1 ... n )  ->  n  e.  ( ZZ>= `  ( x  +  1 ) ) )
350349ad2antll 710 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  n  e.  ( ZZ>= `  ( x  +  1
) ) )
351 fzss2 11025 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  ( ZZ>= `  (
x  +  1 ) )  ->  ( 1 ... ( x  + 
1 ) )  C_  ( 1 ... n
) )
352350, 351syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  C_  ( 1 ... n ) )
353348, 352eqsstr3d 3327 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( 1 ... x )  u.  {
( x  +  1 ) } )  C_  ( 1 ... n
) )
354353unssad 3468 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  C_  ( 1 ... n ) )
355 fssres 5551 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  {  -oo }
)  /\  ( 1 ... x )  C_  ( 1 ... n
) )  ->  (
( E  o.  g
)  |`  ( 1 ... x ) ) : ( 1 ... x
) --> ( RR*  \  {  -oo } ) )
356346, 354, 355syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
357345, 356fisuppfi 14701 . . . . . . . . . . . . . . . . . . . . . . . . 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 )
35865, 66, 344, 345, 356, 357gsumcl 15449 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
359358eldifad 3276 . . . . . . . . . . . . . . . . . . . . . . 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* )
360336, 30syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E : ( V  X.  V ) --> RR* )
361338, 331ffvelrnd 5811 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  (
x  +  1 ) )  e.  ( V  X.  V ) )
362360, 361ffvelrnd 5811 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E `  (
g `  ( x  +  1 ) ) )  e.  RR* )
363 xleadd1a 10765 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
364363ex 424 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
365343, 359, 362, 364syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
366 xp2nd 6317 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  ( x  +  1
) ) )  e.  V )
367361, 366syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  ( x  +  1 ) ) )  e.  V )
368 xmettri 18290 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( E  e.  ( * Met `  V )  /\  ( X  e.  V  /\  ( 2nd `  ( g `  (
x  +  1 ) ) )  e.  V  /\  ( 2nd `  (
g `  x )
)  e.  V ) )  ->  ( X E ( 2nd `  (
g `  ( x  +  1 ) ) ) )  <_  (
( X E ( 2nd `  ( g `
 x ) ) ) + e ( ( 2nd `  (
g `  x )
) E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) ) )
369336, 337, 367, 341, 368syl13anc 1186 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( X E ( 2nd `  ( g `
 ( x  + 
1 ) ) ) )  <_  ( ( X E ( 2nd `  (
g `  x )
) ) + e
( ( 2nd `  (
g `  x )
) E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) ) )
370 1st2nd2 6326 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  (
g `  ( x  +  1 ) )  =  <. ( 1st `  (
g `  ( x  +  1 ) ) ) ,  ( 2nd `  ( g `  (
x  +  1 ) ) ) >. )
371361, 370syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  (
x  +  1 ) )  =  <. ( 1st `  ( g `  ( x  +  1
) ) ) ,  ( 2nd `  (
g `  ( x  +  1 ) ) ) >. )
372 nnz 10236 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  NN  ->  x  e.  ZZ )
373372ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ZZ )
374 eluzp1m1 10442 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ZZ  /\  n  e.  ( ZZ>= `  ( x  +  1
) ) )  -> 
( n  -  1 )  e.  ( ZZ>= `  x ) )
375373, 350, 374syl2anc 64