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

Theorem imasdsf1olem 19789
Description: Lemma for imasdsf1o 19790. (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 5636 . . . . 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 2433 . . . 4  |-  ( dist `  R )  =  (
dist `  R )
8 imasdsf1o.d . . . 4  |-  D  =  ( dist `  U
)
9 f1of 5629 . . . . . 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 5832 . . . 4  |-  ( ph  ->  ( F `  X
)  e.  B )
13 imasdsf1o.y . . . . 5  |-  ( ph  ->  Y  e.  V )
1410, 13ffvelrnd 5832 . . . 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 14436 . . 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 7685 . . 3  |-  sup ( T ,  RR* ,  `'  <  )  =  sup ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) ,  RR* ,  `'  <  )
2017, 19syl6eqr 2483 . 2  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  =  sup ( T ,  RR* ,  `'  <  ) )
21 xrsbas 17675 . . . . . . . . . . . 12  |-  RR*  =  ( Base `  RR*s )
22 xrsadd 17676 . . . . . . . . . . . 12  |-  +e 
=  ( +g  `  RR*s
)
23 imasdsf1o.w . . . . . . . . . . . 12  |-  W  =  ( RR*ss  ( RR*  \  { -oo } ) )
24 xrsex 17674 . . . . . . . . . . . . 13  |-  RR*s 
e.  _V
2524a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  RR*s 
e.  _V )
26 fzfid 11778 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1 ... n )  e. 
Fin )
27 difss 3471 . . . . . . . . . . . . 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 19745 . . . . . . . . . . . . . . . 16  |-  ( E  e.  ( *Met `  V )  ->  E : ( V  X.  V ) --> RR* )
31 ffn 5547 . . . . . . . . . . . . . . . 16  |-  ( E : ( V  X.  V ) --> RR*  ->  E  Fn  ( V  X.  V ) )
3229, 30, 313syl 20 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  Fn  ( V  X.  V ) )
33 xmetcl 19747 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e. 
RR* )
34 xmetge0 19760 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  0  <_  ( f E g ) )
35 ge0nemnf 11132 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f E g )  e.  RR*  /\  0  <_  ( f E g ) )  ->  (
f E g )  =/= -oo )
3633, 34, 35syl2anc 654 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  =/= -oo )
37 eldifsn 3988 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f E g )  e.  ( RR*  \  { -oo } )  <->  ( (
f E g )  e.  RR*  /\  (
f E g )  =/= -oo ) )
3833, 36, 37sylanbrc 657 . . . . . . . . . . . . . . . . . 18  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e.  ( RR*  \  { -oo } ) )
39383expb 1181 . . . . . . . . . . . . . . . . 17  |-  ( ( E  e.  ( *Met `  V )  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  { -oo } ) )
4029, 39sylan 468 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  { -oo } ) )
4140ralrimivva 2798 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. f  e.  V  A. g  e.  V  ( f E g )  e.  ( RR*  \  { -oo } ) )
42 ffnov 6183 . . . . . . . . . . . . . . 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 657 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : ( V  X.  V ) --> (
RR*  \  { -oo }
) )
4443ad2antrr 718 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> ( RR*  \  { -oo } ) )
45 ssrab2 3425 . . . . . . . . . . . . . . . . 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 3374 . . . . . . . . . . . . . . . 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 3344 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
49 elmapi 7222 . . . . . . . . . . . . . 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 5556 . . . . . . . . . . . . 13  |-  ( ( E : ( V  X.  V ) --> (
RR*  \  { -oo }
)  /\  g :
( 1 ... n
) --> ( V  X.  V ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  { -oo }
) )
5244, 50, 51syl2anc 654 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) : ( 1 ... n ) --> ( RR*  \  { -oo } ) )
53 0re 9373 . . . . . . . . . . . . 13  |-  0  e.  RR
54 rexr 9416 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  e.  RR* )
55 renemnf 9419 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  =/= -oo )
56 eldifsn 3988 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( RR*  \  { -oo } )  <->  ( 0  e.  RR*  /\  0  =/= -oo ) )
5754, 55, 56sylanbrc 657 . . . . . . . . . . . . 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 11197 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( 0 +e x )  =  x )
60 xaddid1 11196 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( x +e 0 )  =  x )
6159, 60jca 529 . . . . . . . . . . . . 13  |-  ( x  e.  RR*  ->  ( ( 0 +e x )  =  x  /\  ( x +e 0 )  =  x ) )
6261adantl 463 . . . . . . . . . . . 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 15486 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  =  ( W  gsumg  ( E  o.  g
) ) )
6423, 21ressbas2 14211 . . . . . . . . . . . . 13  |-  ( (
RR*  \  { -oo }
)  C_  RR*  ->  ( RR*  \  { -oo }
)  =  ( Base `  W ) )
6527, 64ax-mp 5 . . . . . . . . . . . 12  |-  ( RR*  \  { -oo } )  =  ( Base `  W
)
6623xrs10 17695 . . . . . . . . . . . 12  |-  0  =  ( 0g `  W )
6723xrs1cmn 17696 . . . . . . . . . . . . 13  |-  W  e. CMnd
6867a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e. CMnd )
69 c0ex 9367 . . . . . . . . . . . . . 14  |-  0  e.  _V
7069a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  0  e.  _V )
7152, 26, 70fdmfifsupp 7618 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) finSupp  0 )
7265, 66, 68, 26, 52, 71gsumcl 16376 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( E  o.  g
) )  e.  (
RR*  \  { -oo }
) )
7363, 72eqeltrd 2507 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  e.  (
RR*  \  { -oo }
) )
7473eldifad 3328 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  e.  RR* )
75 eqid 2433 . . . . . . . . 9  |-  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) )  =  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )
7674, 75fmptd 5855 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) : S --> RR* )
77 frn 5553 . . . . . . . 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 16 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
g  e.  S  |->  (
RR*s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7978ralrimiva 2789 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )  C_  RR* )
80 iunss 4199 . . . . . 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 212 . . . . 5  |-  ( ph  ->  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )  C_  RR* )
8218, 81syl5eqss 3388 . . . 4  |-  ( ph  ->  T  C_  RR* )
83 1nn 10320 . . . . . . 7  |-  1  e.  NN
84 1ex 9368 . . . . . . . . . . . 12  |-  1  e.  _V
85 opex 4544 . . . . . . . . . . . 12  |-  <. X ,  Y >.  e.  _V
8684, 85f1osn 5666 . . . . . . . . . . 11  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } -1-1-onto-> { <. X ,  Y >. }
87 f1of 5629 . . . . . . . . . . 11  |-  ( {
<. 1 ,  <. X ,  Y >. >. } : { 1 } -1-1-onto-> { <. X ,  Y >. }  ->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. } )
8886, 87ax-mp 5 . . . . . . . . . 10  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. }
89 opelxpi 4858 . . . . . . . . . . . 12  |-  ( ( X  e.  V  /\  Y  e.  V )  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9011, 13, 89syl2anc 654 . . . . . . . . . . 11  |-  ( ph  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9190snssd 4006 . . . . . . . . . 10  |-  ( ph  ->  { <. X ,  Y >. }  C_  ( V  X.  V ) )
92 fss 5555 . . . . . . . . . 10  |-  ( ( { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> { <. X ,  Y >. }  /\  {
<. X ,  Y >. } 
C_  ( V  X.  V ) )  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9388, 91, 92sylancr 656 . . . . . . . . 9  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9429elfvexd 5706 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  _V )
95 xpexg 6496 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  V  e.  _V )  ->  ( V  X.  V
)  e.  _V )
9694, 94, 95syl2anc 654 . . . . . . . . . 10  |-  ( ph  ->  ( V  X.  V
)  e.  _V )
97 snex 4521 . . . . . . . . . 10  |-  { 1 }  e.  _V
98 elmapg 7215 . . . . . . . . . 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 ) ) )
9996, 97, 98sylancl 655 . . . . . . . . 9  |-  ( ph  ->  ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V
)  ^m  { 1 } )  <->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> ( V  X.  V ) ) )
10093, 99mpbird 232 . . . . . . . 8  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V )  ^m  {
1 } ) )
101 op1stg 6578 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 1st `  <. X ,  Y >. )  =  X )
10211, 13, 101syl2anc 654 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  <. X ,  Y >. )  =  X )
103102fveq2d 5683 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X ) )
104 op2ndg 6579 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
10511, 13, 104syl2anc 654 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
106105fveq2d 5683 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) )
107103, 106jca 529 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
10824a1i 11 . . . . . . . . . 10  |-  ( ph  -> 
RR*s  e.  _V )
109 snfi 7378 . . . . . . . . . . 11  |-  { 1 }  e.  Fin
110109a1i 11 . . . . . . . . . 10  |-  ( ph  ->  { 1 }  e.  Fin )
11127a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( RR*  \  { -oo } )  C_  RR* )
112 xmetcl 19747 . . . . . . . . . . . . . 14  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  ( X E Y )  e.  RR* )
11329, 11, 13, 112syl3anc 1211 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X E Y )  e.  RR* )
114 xmetge0 19760 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  0  <_  ( X E Y ) )
11529, 11, 13, 114syl3anc 1211 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  ( X E Y ) )
116 ge0nemnf 11132 . . . . . . . . . . . . . 14  |-  ( ( ( X E Y )  e.  RR*  /\  0  <_  ( X E Y ) )  ->  ( X E Y )  =/= -oo )
117113, 115, 116syl2anc 654 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X E Y )  =/= -oo )
118 eldifsn 3988 . . . . . . . . . . . . 13  |-  ( ( X E Y )  e.  ( RR*  \  { -oo } )  <->  ( ( X E Y )  e. 
RR*  /\  ( X E Y )  =/= -oo ) )
119113, 117, 118sylanbrc 657 . . . . . . . . . . . 12  |-  ( ph  ->  ( X E Y )  e.  ( RR*  \  { -oo } ) )
120 fconst6g 5587 . . . . . . . . . . . 12  |-  ( ( X E Y )  e.  ( RR*  \  { -oo } )  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  { -oo } ) )
121119, 120syl 16 . . . . . . . . . . 11  |-  ( ph  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  { -oo } ) )
122 fcoconst 5867 . . . . . . . . . . . . . 14  |-  ( ( E  Fn  ( V  X.  V )  /\  <. X ,  Y >.  e.  ( V  X.  V
) )  ->  ( E  o.  ( {
1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `  <. X ,  Y >. ) } ) )
12332, 90, 122syl2anc 654 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `
 <. X ,  Y >. ) } ) )
12484, 85xpsn 5872 . . . . . . . . . . . . . 14  |-  ( { 1 }  X.  { <. X ,  Y >. } )  =  { <. 1 ,  <. X ,  Y >. >. }
125124coeq2i 4987 . . . . . . . . . . . . 13  |-  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )
126 df-ov 6083 . . . . . . . . . . . . . . . 16  |-  ( X E Y )  =  ( E `  <. X ,  Y >. )
127126eqcomi 2437 . . . . . . . . . . . . . . 15  |-  ( E `
 <. X ,  Y >. )  =  ( X E Y )
128127sneqi 3876 . . . . . . . . . . . . . 14  |-  { ( E `  <. X ,  Y >. ) }  =  { ( X E Y ) }
129128xpeq2i 4848 . . . . . . . . . . . . 13  |-  ( { 1 }  X.  {
( E `  <. X ,  Y >. ) } )  =  ( { 1 }  X.  { ( X E Y ) } )
130123, 125, 1293eqtr3g 2488 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( { 1 }  X.  { ( X E Y ) } ) )
131130feq1d 5534 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  { -oo } )  <->  ( { 1 }  X.  { ( X E Y ) } ) : {
1 } --> ( RR*  \  { -oo } ) ) )
132121, 131mpbird 232 . . . . . . . . . 10  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  { -oo } ) )
13353, 57mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( RR*  \  { -oo } ) )
13461adantl 463 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
0 +e x )  =  x  /\  ( x +e 0 )  =  x ) )
13521, 22, 23, 108, 110, 111, 132, 133, 134gsumress 15486 . . . . . . . . 9  |-  ( ph  ->  ( RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
136 fconstmpt 4869 . . . . . . . . . . 11  |-  ( { 1 }  X.  {
( X E Y ) } )  =  ( j  e.  {
1 }  |->  ( X E Y ) )
137130, 136syl6eq 2481 . . . . . . . . . 10  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( j  e.  {
1 }  |->  ( X E Y ) ) )
138137oveq2d 6096 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
139 cmnmnd 16271 . . . . . . . . . . 11  |-  ( W  e. CMnd  ->  W  e.  Mnd )
14067, 139mp1i 12 . . . . . . . . . 10  |-  ( ph  ->  W  e.  Mnd )
14183a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  NN )
142 eqidd 2434 . . . . . . . . . . 11  |-  ( j  =  1  ->  ( X E Y )  =  ( X E Y ) )
14365, 142gsumsn 16424 . . . . . . . . . 10  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( X E Y )  e.  ( RR*  \  { -oo } ) )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
144140, 141, 119, 143syl3anc 1211 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
145135, 138, 1443eqtrrd 2470 . . . . . . . 8  |-  ( ph  ->  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
146 fveq1 5678 . . . . . . . . . . . . . . 15  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  ( { <. 1 ,  <. X ,  Y >. >. } `  1
) )
14784, 85fvsn 5898 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  <. X ,  Y >. >. } ` 
1 )  =  <. X ,  Y >.
148146, 147syl6eq 2481 . . . . . . . . . . . . . 14  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  <. X ,  Y >. )
149148fveq2d 5683 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 1st `  ( g ` 
1 ) )  =  ( 1st `  <. X ,  Y >. )
)
150149fveq2d 5683 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  ( 1st `  <. X ,  Y >. ) ) )
151150eqeq1d 2441 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  <. X ,  Y >. )
)  =  ( F `
 X ) ) )
152148fveq2d 5683 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 2nd `  ( g ` 
1 ) )  =  ( 2nd `  <. X ,  Y >. )
)
153152fveq2d 5683 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  ( 2nd `  <. X ,  Y >. ) ) )
154153eqeq1d 2441 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 2nd `  ( g ` 
1 ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
155151, 154anbi12d 703 . . . . . . . . . 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 ) ) ) )
156 coeq2 4985 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( E  o.  g )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )
157156oveq2d 6096 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( RR*s  gsumg  ( E  o.  g
) )  =  (
RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
158157eqeq2d 2444 . . . . . . . . . 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 >. >. } ) ) ) )
159155, 158anbi12d 703 . . . . . . . . 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 >. >. } ) ) ) ) )
160159rspcev 3062 . . . . . . . 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 ) ) ) )
161100, 107, 145, 160syl12anc 1209 . . . . . . 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 ) ) ) )
162 ovex 6105 . . . . . . . . . 10  |-  ( X E Y )  e. 
_V
16375elrnmpt 5073 . . . . . . . . . 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
) ) ) )
164162, 163ax-mp 5 . . . . . . . . 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
) ) )
16515rexeqi 2912 . . . . . . . . . . 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
) ) )
166 fveq1 5678 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  1 )  =  ( g ` 
1 ) )
167166fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 1st `  ( h ` 
1 ) )  =  ( 1st `  (
g `  1 )
) )
168167fveq2d 5683 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  1
) ) )  =  ( F `  ( 1st `  ( g ` 
1 ) ) ) )
169168eqeq1d 2441 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 1st `  ( h ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  (
g `  1 )
) )  =  ( F `  X ) ) )
170 fveq1 5678 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  n )  =  ( g `  n ) )
171170fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 2nd `  ( h `  n ) )  =  ( 2nd `  (
g `  n )
) )
172171fveq2d 5683 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  ( 2nd `  ( g `  n ) ) ) )
173172eqeq1d 2441 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y ) ) )
174 fveq1 5678 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  i )  =  ( g `  i ) )
175174fveq2d 5683 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 2nd `  ( h `  i ) )  =  ( 2nd `  (
g `  i )
) )
176175fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 2nd `  ( g `  i ) ) ) )
177 fveq1 5678 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  ( i  +  1 ) )  =  ( g `  ( i  +  1 ) ) )
178177fveq2d 5683 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 1st `  ( h `  ( i  +  1 ) ) )  =  ( 1st `  (
g `  ( i  +  1 ) ) ) )
179178fveq2d 5683 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  (
i  +  1 ) ) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )
180176, 179eqeq12d 2447 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  i ) ) )  =  ( F `  ( 1st `  ( h `
 ( i  +  1 ) ) ) )  <->  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
181180ralbidv 2725 . . . . . . . . . . . . 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 ) ) ) ) ) )
182169, 173, 1813anbi123d 1282 . . . . . . . . . . . 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 ) ) ) ) ) ) )
183182rexrab 3112 . . . . . . . . . . 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 ) ) ) )
184165, 183bitri 249 . . . . . . . . . 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 ) ) ) )
185 oveq2 6088 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
186 1z 10663 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
187 fzsn 11486 . . . . . . . . . . . . . 14  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
188186, 187ax-mp 5 . . . . . . . . . . . . 13  |-  ( 1 ... 1 )  =  { 1 }
189185, 188syl6eq 2481 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
1 ... n )  =  { 1 } )
190189oveq2d 6096 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( V  X.  V
)  ^m  ( 1 ... n ) )  =  ( ( V  X.  V )  ^m  { 1 } ) )
191 df-3an 960 . . . . . . . . . . . . 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 ) ) ) ) ) )
192 ral0 3772 . . . . . . . . . . . . . . . 16  |-  A. i  e.  (/)  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) )
193 oveq1 6087 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
194 1m1e0 10377 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  -  1 )  =  0
195193, 194syl6eq 2481 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
196195oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  ( 1 ... 0
) )
197 fz10 11456 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... 0 )  =  (/)
198196, 197syl6eq 2481 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  (/) )
199198raleqdv 2913 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200192, 199mpbiri 233 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )
201200biantrud 504 . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
202 fveq2 5679 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
g `  n )  =  ( g ` 
1 ) )
203202fveq2d 5683 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( 2nd `  ( g `  n ) )  =  ( 2nd `  (
g `  1 )
) )
204203fveq2d 5683 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  ( 2nd `  ( g ` 
1 ) ) ) )
205204eqeq1d 2441 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) )
206205anbi2d 696 . . . . . . . . . . . . . 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 ) ) ) )
207201, 206bitr3d 255 . . . . . . . . . . . . 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 ) ) ) )
208191, 207syl5bb 257 . . . . . . . . . . . 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 ) ) ) )
209208anbi1d 697 . . . . . . . . . . 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 ) ) ) ) )
210190, 209rexeqbidv 2922 . . . . . . . . . 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 ) ) ) ) )
211184, 210syl5bb 257 . . . . . . . . 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 ) ) ) ) )
212164, 211syl5bb 257 . . . . . . . 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 ) ) ) ) )
213212rspcev 3062 . . . . . . 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 ) ) ) )
21483, 161, 213sylancr 656 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) )
215 eliun 4163 . . . . . 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 ) ) ) )
216214, 215sylibr 212 . . . . 5  |-  ( ph  ->  ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) )
217216, 18syl6eleqr 2524 . . . 4  |-  ( ph  ->  ( X E Y )  e.  T )
218 infmxrlb 11283 . . . 4  |-  ( ( T  C_  RR*  /\  ( X E Y )  e.  T )  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
21982, 217, 218syl2anc 654 . . 3  |-  ( ph  ->  sup ( T ,  RR* ,  `'  <  )  <_  ( X E Y ) )
22018eleq2i 2497 . . . . . . 7  |-  ( p  e.  T  <->  p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
221 eliun 4163 . . . . . . 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 ) ) ) )
222220, 221bitri 249 . . . . . 6  |-  ( p  e.  T  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
223 vex 2965 . . . . . . . . 9  |-  p  e. 
_V
22475elrnmpt 5073 . . . . . . . . 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
) ) ) )
225223, 224ax-mp 5 . . . . . . . 8  |-  ( p  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  p  =  ( RR*s  gsumg  ( E  o.  g
) ) )
226182, 15elrab2 3108 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
227226simprbi 461 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
228227adantl 463 . . . . . . . . . . . . . . 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 ) ) ) ) ) )
229228simp2d 994 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )
2303ad2antrr 718 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-onto-> B )
231 f1of1 5628 . . . . . . . . . . . . . . . 16  |-  ( F : V -1-1-onto-> B  ->  F : V -1-1-> B )
232230, 231syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-> B )
233 simplr 747 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  NN )
234 elfz1end 11465 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  <->  n  e.  ( 1 ... n
) )
235233, 234sylib 196 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( 1 ... n
) )
23650, 235ffvelrnd 5832 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  n )  e.  ( V  X.  V
) )
237 xp2nd 6596 . . . . . . . . . . . . . . . 16  |-  ( ( g `  n )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  n ) )  e.  V )
238236, 237syl 16 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  e.  V )
23913ad2antrr 718 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  Y  e.  V )
240 f1fveq 5962 . . . . . . . . . . . . . . 15  |-  ( ( F : V -1-1-> B  /\  ( ( 2nd `  (
g `  n )
)  e.  V  /\  Y  e.  V )
)  ->  ( ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  <->  ( 2nd `  (
g `  n )
)  =  Y ) )
241232, 238, 239, 240syl12anc 1209 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( 2nd `  ( g `  n
) )  =  Y ) )
242229, 241mpbid 210 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  =  Y )
243242oveq2d 6096 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  n )
) )  =  ( X E Y ) )
244 eleq1 2493 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  e.  ( 1 ... n )  <->  1  e.  ( 1 ... n
) ) )
245 fveq2 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
g `  m )  =  ( g ` 
1 ) )
246245fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  1 )
) )
247246oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  1
) ) ) )
248 oveq2 6088 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
249248, 188syl6eq 2481 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
250249reseq2d 5097 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  { 1 } ) )
251250oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
252247, 251breq12d 4293 . . . . . . . . . . . . . . . . 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 } ) ) ) )
253244, 252imbi12d 320 . . . . . . . . . . . . . . . 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 } ) ) ) ) )
254253imbi2d 316 . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
255 eleq1 2493 . . . . . . . . . . . . . . . . 17  |-  ( m  =  x  ->  (
m  e.  ( 1 ... n )  <->  x  e.  ( 1 ... n
) ) )
256 fveq2 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
g `  m )  =  ( g `  x ) )
257256fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  x )
) )
258257oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  x
) ) ) )
259 oveq2 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
1 ... m )  =  ( 1 ... x
) )
260259reseq2d 5097 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... x ) ) )
261260oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) )
262258, 261breq12d 4293 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
263255, 262imbi12d 320 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
264263imbi2d 316 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
265 eleq1 2493 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( x  + 
1 )  ->  (
m  e.  ( 1 ... n )  <->  ( x  +  1 )  e.  ( 1 ... n
) ) )
266 fveq2 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
g `  m )  =  ( g `  ( x  +  1
) ) )
267266fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  ( x  +  1 ) ) ) )
268267oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) )
269 oveq2 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
1 ... m )  =  ( 1 ... (
x  +  1 ) ) )
270269reseq2d 5097 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) )
271270oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) ) )
272268, 271breq12d 4293 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
273265, 272imbi12d 320 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
274273imbi2d 316 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
275 eleq1 2493 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
m  e.  ( 1 ... n )  <->  n  e.  ( 1 ... n
) ) )
276 fveq2 5679 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
277276fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  n )
) )
278277oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  n
) ) ) )
279 oveq2 6088 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
1 ... m )  =  ( 1 ... n
) )
280279reseq2d 5097 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... n ) ) )
281280oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... n ) ) ) )
282278, 281breq12d 4293 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
283275, 282imbi12d 320 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
284283imbi2d 316 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
28529ad2antrr 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E  e.  ( *Met `  V ) )
28611ad2antrr 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  X  e.  V )
287 nnuz 10883 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
288233, 287syl6eleq 2523 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( ZZ>= `  1 )
)
289 eluzfz1 11444 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... n
) )
290288, 289syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  ( 1 ... n
) )
29150, 290ffvelrnd 5832 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  e.  ( V  X.  V
) )
292 xp2nd 6596 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
293291, 292syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
294 xmetcl 19747 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  1 )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
295285, 286, 293, 294syl3anc 1211 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
296 xrleid 11114 . . . . . . . . . . . . . . . . . 18  |-  ( ( X E ( 2nd `  ( g `  1
) ) )  e. 
RR*  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
297295, 296syl 16 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
298140ad2antrr 718 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e.  Mnd )
29983a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  NN )
30044, 291ffvelrnd 5832 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  ( g `  1 ) )  e.  ( RR*  \  { -oo } ) )
301 fveq2 5679 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  1  ->  (
g `  j )  =  ( g ` 
1 ) )
302301fveq2d 5683 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  1  ->  ( E `  ( g `  j ) )  =  ( E `  (
g `  1 )
) )
30365, 302gsumsn 16424 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( E `  ( g `  1 ) )  e.  ( RR*  \  { -oo } ) )  -> 
( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
304298, 299, 300, 303syl3anc 1211 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
305285, 30syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> RR* )
306 fcompt 5866 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E : ( V  X.  V ) --> RR* 
/\  g : ( 1 ... n ) --> ( V  X.  V
) )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
307305, 50, 306syl2anc 654 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
308307reseq1d 5096 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( ( j  e.  ( 1 ... n )  |->  ( E `  ( g `
 j ) ) )  |`  { 1 } ) )
309290snssd 4006 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  { 1 }  C_  ( 1 ... n ) )
310 resmpt 5144 . . . . . . . . . . . . . . . . . . . . 21  |-  ( { 1 }  C_  (
1 ... n )  -> 
( ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) )  |`  { 1 } )  =  ( j  e. 
{ 1 }  |->  ( E `  ( g `
 j ) ) ) )
311309, 310syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( j  e.  ( 1 ... n ) 
|->  ( E `  (
g `  j )
) )  |`  { 1 } )  =  ( j  e.  { 1 }  |->  ( E `  ( g `  j
) ) ) )
312308, 311eqtrd 2465 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( j  e.  { 1 } 
|->  ( E `  (
g `  j )
) ) )
313312oveq2d 6096 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) ) )
314 df-ov 6083 . . . . . . . . . . . . . . . . . . 19  |-  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )
315 1st2nd2 6602 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
316291, 315syl 16 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
317228simp1d 993 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
) )
318 xp1st 6595 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
319291, 318syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
320 f1fveq 5962 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : V -1-1-> B  /\  ( ( 1st `  (
g `  1 )
)  e.  V  /\  X  e.  V )
)  ->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  <->  ( 1st `  (
g `  1 )
)  =  X ) )
321232, 319, 286, 320syl12anc 1209 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( 1st `  ( g `  1
) )  =  X ) )
322317, 321mpbid 210 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  =  X )
323322opeq1d 4053 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. ( 1st `  ( g ` 
1 ) ) ,  ( 2nd `  (
g `  1 )
) >.  =  <. X , 
( 2nd `  (
g `  1 )
) >. )
324316, 323eqtr2d 2466 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. X , 
( 2nd `  (
g `  1 )
) >.  =  ( g `
 1 ) )
325324fveq2d 5683 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )  =  ( E `  ( g `
 1 ) ) )
326314, 325syl5eq 2477 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  ( g `
 1 ) ) )
327304, 313, 3263eqtr4d 2475 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( X E ( 2nd `  ( g `
 1 ) ) ) )
328297, 327breqtrrd 4306 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
329328a1d 25 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) )
330 simprl 748 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  NN )
331330, 287syl6eleq 2523 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( ZZ>= ` 
1 ) )
332 simprr 749 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( x  +  1 )  e.  ( 1 ... n ) )
333 peano2fzr 11449 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( ZZ>= ` 
1 )  /\  (
x  +  1 )  e.  ( 1 ... n ) )  ->  x  e.  ( 1 ... n ) )
334331, 332, 333syl2anc 654 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( 1 ... n ) )
335334expr 610 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  NN )  ->  ( ( x  +  1 )  e.  ( 1 ... n )  ->  x  e.  ( 1 ... n
) ) )
336335imim1d 75 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
337285adantr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E  e.  ( *Met `  V ) )
338286adantr 462 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  X  e.  V )
33950adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
g : ( 1 ... n ) --> ( V  X.  V ) )
340339, 334ffvelrnd 5832 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  x
)  e.  ( V  X.  V ) )
341 xp2nd 6596 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  x )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  x ) )  e.  V )
342340, 341syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  x )
)  e.  V )
343 xmetcl 19747 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  x )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  x )
) )  e.  RR* )
344337, 338, 342, 343syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  e.  RR* )
34567a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  W  e. CMnd )
346 fzfid 11778 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  e.  Fin )
34752adantr 462 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  { -oo }
) )
348 fzsuc 11488 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( x  + 
1 ) )  =  ( ( 1 ... x )  u.  {
( x  +  1 ) } ) )
349331, 348syl 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 ) } ) )
350 elfzuz3 11436 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  +  1 )  e.  ( 1 ... n )  ->  n  e.  ( ZZ>= `  ( x  +  1 ) ) )
351350ad2antll 721 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  n  e.  ( ZZ>= `  ( x  +  1
) ) )
352 fzss2 11484 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  ( ZZ>= `  (
x  +  1 ) )  ->  ( 1 ... ( x  + 
1 ) )  C_  ( 1 ... n
) )
353351, 352syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  C_  ( 1 ... n ) )
354349, 353eqsstr3d 3379 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( 1 ... x )  u.  {
( x  +  1 ) } )  C_  ( 1 ... n
) )
355354unssad 3521 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  C_  ( 1 ... n ) )
356 fssres 5566 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  { -oo }
)  /\  ( 1 ... x )  C_  ( 1 ... n
) )  ->  (
( E  o.  g
)  |`  ( 1 ... x ) ) : ( 1 ... x
) --> ( RR*  \  { -oo } ) )
357347, 355, 356syl2anc 654 . . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
35869a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
0  e.  _V )
359357, 346, 358fdmfifsupp 7618 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( E  o.  g )  |`  (
1 ... x ) ) finSupp 
0 )
36065, 66, 345, 346, 357, 359gsumcl 16376 . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
361360eldifad 3328 . . . . . . . . . . . . . . . . . . . . . . 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* )
362337, 30syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E : ( V  X.  V ) --> RR* )
363339, 332ffvelrnd 5832 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  (
x  +  1 ) )  e.  ( V  X.  V ) )
364362, 363ffvelrnd 5832 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E `  (
g `  ( x  +  1 ) ) )  e.  RR* )
365 xleadd1a 11203 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
366365ex 434 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
367344, 361, 364, 366syl3anc 1211 . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
368 xp2nd 6596 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  ( x  +  1
) ) )  e.  V )
369363, 368syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  ( x  +  1 ) ) )  e.  V )
370 xmettri 19767 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
371337, 338, 369, 342, 370syl13anc 1213 . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
372 1st2nd2 6602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  (
g `  ( x  +  1 ) )  =  <. ( 1st `  (
g `  ( x  +  1 ) ) ) ,  ( 2nd `  ( g `  (
x  +  1 ) ) ) >. )
373363, 372syl 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 ) ) ) >. )
374 nnz 10655 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  NN  ->  x  e.  ZZ )
375374ad2antrl 720 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ZZ )
376 eluzp1m1 10871 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ZZ  /\  n  e.  ( ZZ>= `  ( x  +  1
) ) )  -> 
( n  -  1 )  e.  ( ZZ>= `  x