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

Theorem imasdsf1olem 21380
Description: Lemma for imasdsf1o 21381. (Contributed by Mario Carneiro, 21-Aug-2015.) (Proof shortened by AV, 6-Oct-2020.)
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 5836 . . . . 5  |-  ( F : V -1-1-onto-> B  ->  F : V -onto-> B )
53, 4syl 17 . . . 4  |-  ( ph  ->  F : V -onto-> B
)
6 imasdsf1o.r . . . 4  |-  ( ph  ->  R  e.  Z )
7 eqid 2423 . . . 4  |-  ( dist `  R )  =  (
dist `  R )
8 imasdsf1o.d . . . 4  |-  D  =  ( dist `  U
)
9 f1of 5829 . . . . . 6  |-  ( F : V -1-1-onto-> B  ->  F : V
--> B )
103, 9syl 17 . . . . 5  |-  ( ph  ->  F : V --> B )
11 imasdsf1o.x . . . . 5  |-  ( ph  ->  X  e.  V )
1210, 11ffvelrnd 6036 . . . 4  |-  ( ph  ->  ( F `  X
)  e.  B )
13 imasdsf1o.y . . . . 5  |-  ( ph  ->  Y  e.  V )
1410, 13ffvelrnd 6036 . . . 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 15410 . . 3  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  = inf ( 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 ) ) )
1918infeq1i 7998 . . 3  |- inf ( T ,  RR* ,  <  )  = inf ( U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) , 
RR* ,  <  )
2017, 19syl6eqr 2482 . 2  |-  ( ph  ->  ( ( F `  X ) D ( F `  Y ) )  = inf ( T ,  RR* ,  <  )
)
21 xrsbas 18977 . . . . . . . . . . . 12  |-  RR*  =  ( Base `  RR*s )
22 xrsadd 18978 . . . . . . . . . . . 12  |-  +e 
=  ( +g  `  RR*s
)
23 imasdsf1o.w . . . . . . . . . . . 12  |-  W  =  ( RR*ss  ( RR*  \  { -oo } ) )
24 xrsex 18976 . . . . . . . . . . . . 13  |-  RR*s 
e.  _V
2524a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  RR*s 
e.  _V )
26 fzfid 12187 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1 ... n )  e. 
Fin )
27 difss 3593 . . . . . . . . . . . . 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 21336 . . . . . . . . . . . . . . . 16  |-  ( E  e.  ( *Met `  V )  ->  E : ( V  X.  V ) --> RR* )
31 ffn 5744 . . . . . . . . . . . . . . . 16  |-  ( E : ( V  X.  V ) --> RR*  ->  E  Fn  ( V  X.  V ) )
3229, 30, 313syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  E  Fn  ( V  X.  V ) )
33 xmetcl 21338 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e. 
RR* )
34 xmetge0 21351 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  0  <_  ( f E g ) )
35 ge0nemnf 11470 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( f E g )  e.  RR*  /\  0  <_  ( f E g ) )  ->  (
f E g )  =/= -oo )
3633, 34, 35syl2anc 666 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  =/= -oo )
37 eldifsn 4123 . . . . . . . . . . . . . . . . . . 19  |-  ( ( f E g )  e.  ( RR*  \  { -oo } )  <->  ( (
f E g )  e.  RR*  /\  (
f E g )  =/= -oo ) )
3833, 36, 37sylanbrc 669 . . . . . . . . . . . . . . . . . 18  |-  ( ( E  e.  ( *Met `  V )  /\  f  e.  V  /\  g  e.  V
)  ->  ( f E g )  e.  ( RR*  \  { -oo } ) )
39383expb 1207 . . . . . . . . . . . . . . . . 17  |-  ( ( E  e.  ( *Met `  V )  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  { -oo } ) )
4029, 39sylan 474 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( f  e.  V  /\  g  e.  V ) )  -> 
( f E g )  e.  ( RR*  \  { -oo } ) )
4140ralrimivva 2847 . . . . . . . . . . . . . . 15  |-  ( ph  ->  A. f  e.  V  A. g  e.  V  ( f E g )  e.  ( RR*  \  { -oo } ) )
42 ffnov 6412 . . . . . . . . . . . . . . 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 669 . . . . . . . . . . . . . 14  |-  ( ph  ->  E : ( V  X.  V ) --> (
RR*  \  { -oo }
) )
4443ad2antrr 731 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> ( RR*  \  { -oo } ) )
45 ssrab2 3547 . . . . . . . . . . . . . . . . 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 3495 . . . . . . . . . . . . . . . 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 3465 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) ) )
49 elmapi 7499 . . . . . . . . . . . . . 14  |-  ( g  e.  ( ( V  X.  V )  ^m  ( 1 ... n
) )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
5048, 49syl 17 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  g : ( 1 ... n ) --> ( V  X.  V ) )
51 fco 5754 . . . . . . . . . . . . 13  |-  ( ( E : ( V  X.  V ) --> (
RR*  \  { -oo }
)  /\  g :
( 1 ... n
) --> ( V  X.  V ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  { -oo }
) )
5244, 50, 51syl2anc 666 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) : ( 1 ... n ) --> ( RR*  \  { -oo } ) )
53 0re 9645 . . . . . . . . . . . . 13  |-  0  e.  RR
54 rexr 9688 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  e.  RR* )
55 renemnf 9691 . . . . . . . . . . . . . 14  |-  ( 0  e.  RR  ->  0  =/= -oo )
56 eldifsn 4123 . . . . . . . . . . . . . 14  |-  ( 0  e.  ( RR*  \  { -oo } )  <->  ( 0  e.  RR*  /\  0  =/= -oo ) )
5754, 55, 56sylanbrc 669 . . . . . . . . . . . . 13  |-  ( 0  e.  RR  ->  0  e.  ( RR*  \  { -oo } ) )
5853, 57mp1i 13 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  0  e.  ( RR*  \  { -oo } ) )
59 xaddid2 11535 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( 0 +e x )  =  x )
60 xaddid1 11534 . . . . . . . . . . . . . 14  |-  ( x  e.  RR*  ->  ( x +e 0 )  =  x )
6159, 60jca 535 . . . . . . . . . . . . 13  |-  ( x  e.  RR*  ->  ( ( 0 +e x )  =  x  /\  ( x +e 0 )  =  x ) )
6261adantl 468 . . . . . . . . . . . 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 16512 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  =  ( W  gsumg  ( E  o.  g
) ) )
6423, 21ressbas2 15173 . . . . . . . . . . . . 13  |-  ( (
RR*  \  { -oo }
)  C_  RR*  ->  ( RR*  \  { -oo }
)  =  ( Base `  W ) )
6527, 64ax-mp 5 . . . . . . . . . . . 12  |-  ( RR*  \  { -oo } )  =  ( Base `  W
)
6623xrs10 19000 . . . . . . . . . . . 12  |-  0  =  ( 0g `  W )
6723xrs1cmn 19001 . . . . . . . . . . . . 13  |-  W  e. CMnd
6867a1i 11 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e. CMnd )
69 c0ex 9639 . . . . . . . . . . . . . 14  |-  0  e.  _V
7069a1i 11 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  0  e.  _V )
7152, 26, 70fdmfifsupp 7897 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g ) finSupp  0 )
7265, 66, 68, 26, 52, 71gsumcl 17542 . . . . . . . . . . 11  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( E  o.  g
) )  e.  (
RR*  \  { -oo }
) )
7363, 72eqeltrd 2511 . . . . . . . . . 10  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  e.  (
RR*  \  { -oo }
) )
7473eldifad 3449 . . . . . . . . 9  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( RR*s  gsumg  ( E  o.  g
) )  e.  RR* )
75 eqid 2423 . . . . . . . . 9  |-  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) )  =  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )
7674, 75fmptd 6059 . . . . . . . 8  |-  ( (
ph  /\  n  e.  NN )  ->  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) : S --> RR* )
77 frn 5750 . . . . . . . 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 17 . . . . . . 7  |-  ( (
ph  /\  n  e.  NN )  ->  ran  (
g  e.  S  |->  (
RR*s  gsumg  ( E  o.  g
) ) )  C_  RR* )
7978ralrimiva 2840 . . . . . 6  |-  ( ph  ->  A. n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )  C_  RR* )
80 iunss 4338 . . . . . 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 216 . . . . 5  |-  ( ph  ->  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) )  C_  RR* )
8218, 81syl5eqss 3509 . . . 4  |-  ( ph  ->  T  C_  RR* )
83 infxrcl 11621 . . . 4  |-  ( T 
C_  RR*  -> inf ( T ,  RR* ,  <  )  e.  RR* )
8482, 83syl 17 . . 3  |-  ( ph  -> inf ( T ,  RR* ,  <  )  e.  RR* )
85 xmetcl 21338 . . . 4  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  ( X E Y )  e.  RR* )
8629, 11, 13, 85syl3anc 1265 . . 3  |-  ( ph  ->  ( X E Y )  e.  RR* )
87 1nn 10622 . . . . . . 7  |-  1  e.  NN
88 1ex 9640 . . . . . . . . . . . 12  |-  1  e.  _V
89 opex 4683 . . . . . . . . . . . 12  |-  <. X ,  Y >.  e.  _V
9088, 89f1osn 5866 . . . . . . . . . . 11  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } -1-1-onto-> { <. X ,  Y >. }
91 f1of 5829 . . . . . . . . . . 11  |-  ( {
<. 1 ,  <. X ,  Y >. >. } : { 1 } -1-1-onto-> { <. X ,  Y >. }  ->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. } )
9290, 91ax-mp 5 . . . . . . . . . 10  |-  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> { <. X ,  Y >. }
93 opelxpi 4883 . . . . . . . . . . . 12  |-  ( ( X  e.  V  /\  Y  e.  V )  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9411, 13, 93syl2anc 666 . . . . . . . . . . 11  |-  ( ph  -> 
<. X ,  Y >.  e.  ( V  X.  V
) )
9594snssd 4143 . . . . . . . . . 10  |-  ( ph  ->  { <. X ,  Y >. }  C_  ( V  X.  V ) )
96 fss 5752 . . . . . . . . . 10  |-  ( ( { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> { <. X ,  Y >. }  /\  {
<. X ,  Y >. } 
C_  ( V  X.  V ) )  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9792, 95, 96sylancr 668 . . . . . . . . 9  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. } : { 1 } --> ( V  X.  V ) )
9829elfvexd 5907 . . . . . . . . . . 11  |-  ( ph  ->  V  e.  _V )
99 xpexg 6605 . . . . . . . . . . 11  |-  ( ( V  e.  _V  /\  V  e.  _V )  ->  ( V  X.  V
)  e.  _V )
10098, 98, 99syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ( V  X.  V
)  e.  _V )
101 snex 4660 . . . . . . . . . 10  |-  { 1 }  e.  _V
102 elmapg 7491 . . . . . . . . . 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 ) ) )
103100, 101, 102sylancl 667 . . . . . . . . 9  |-  ( ph  ->  ( { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V
)  ^m  { 1 } )  <->  { <. 1 ,  <. X ,  Y >. >. } : {
1 } --> ( V  X.  V ) ) )
10497, 103mpbird 236 . . . . . . . 8  |-  ( ph  ->  { <. 1 ,  <. X ,  Y >. >. }  e.  ( ( V  X.  V )  ^m  {
1 } ) )
105 op1stg 6817 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 1st `  <. X ,  Y >. )  =  X )
10611, 13, 105syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ( 1st `  <. X ,  Y >. )  =  X )
107106fveq2d 5883 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X ) )
108 op2ndg 6818 . . . . . . . . . . 11  |-  ( ( X  e.  V  /\  Y  e.  V )  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
10911, 13, 108syl2anc 666 . . . . . . . . . 10  |-  ( ph  ->  ( 2nd `  <. X ,  Y >. )  =  Y )
110109fveq2d 5883 . . . . . . . . 9  |-  ( ph  ->  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) )
111107, 110jca 535 . . . . . . . 8  |-  ( ph  ->  ( ( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
11224a1i 11 . . . . . . . . . 10  |-  ( ph  -> 
RR*s  e.  _V )
113 snfi 7655 . . . . . . . . . . 11  |-  { 1 }  e.  Fin
114113a1i 11 . . . . . . . . . 10  |-  ( ph  ->  { 1 }  e.  Fin )
11527a1i 11 . . . . . . . . . 10  |-  ( ph  ->  ( RR*  \  { -oo } )  C_  RR* )
116 xmetge0 21351 . . . . . . . . . . . . . . 15  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  Y  e.  V
)  ->  0  <_  ( X E Y ) )
11729, 11, 13, 116syl3anc 1265 . . . . . . . . . . . . . 14  |-  ( ph  ->  0  <_  ( X E Y ) )
118 ge0nemnf 11470 . . . . . . . . . . . . . 14  |-  ( ( ( X E Y )  e.  RR*  /\  0  <_  ( X E Y ) )  ->  ( X E Y )  =/= -oo )
11986, 117, 118syl2anc 666 . . . . . . . . . . . . 13  |-  ( ph  ->  ( X E Y )  =/= -oo )
120 eldifsn 4123 . . . . . . . . . . . . 13  |-  ( ( X E Y )  e.  ( RR*  \  { -oo } )  <->  ( ( X E Y )  e. 
RR*  /\  ( X E Y )  =/= -oo ) )
12186, 119, 120sylanbrc 669 . . . . . . . . . . . 12  |-  ( ph  ->  ( X E Y )  e.  ( RR*  \  { -oo } ) )
122 fconst6g 5787 . . . . . . . . . . . 12  |-  ( ( X E Y )  e.  ( RR*  \  { -oo } )  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  { -oo } ) )
123121, 122syl 17 . . . . . . . . . . 11  |-  ( ph  ->  ( { 1 }  X.  { ( X E Y ) } ) : { 1 } --> ( RR*  \  { -oo } ) )
124 fcoconst 6073 . . . . . . . . . . . . . 14  |-  ( ( E  Fn  ( V  X.  V )  /\  <. X ,  Y >.  e.  ( V  X.  V
) )  ->  ( E  o.  ( {
1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `  <. X ,  Y >. ) } ) )
12532, 94, 124syl2anc 666 . . . . . . . . . . . . 13  |-  ( ph  ->  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( { 1 }  X.  { ( E `
 <. X ,  Y >. ) } ) )
12688, 89xpsn 6079 . . . . . . . . . . . . . 14  |-  ( { 1 }  X.  { <. X ,  Y >. } )  =  { <. 1 ,  <. X ,  Y >. >. }
127126coeq2i 5012 . . . . . . . . . . . . 13  |-  ( E  o.  ( { 1 }  X.  { <. X ,  Y >. } ) )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )
128 df-ov 6306 . . . . . . . . . . . . . . . 16  |-  ( X E Y )  =  ( E `  <. X ,  Y >. )
129128eqcomi 2436 . . . . . . . . . . . . . . 15  |-  ( E `
 <. X ,  Y >. )  =  ( X E Y )
130129sneqi 4008 . . . . . . . . . . . . . 14  |-  { ( E `  <. X ,  Y >. ) }  =  { ( X E Y ) }
131130xpeq2i 4872 . . . . . . . . . . . . 13  |-  ( { 1 }  X.  {
( E `  <. X ,  Y >. ) } )  =  ( { 1 }  X.  { ( X E Y ) } )
132125, 127, 1313eqtr3g 2487 . . . . . . . . . . . 12  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( { 1 }  X.  { ( X E Y ) } ) )
133132feq1d 5730 . . . . . . . . . . 11  |-  ( ph  ->  ( ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  { -oo } )  <->  ( { 1 }  X.  { ( X E Y ) } ) : {
1 } --> ( RR*  \  { -oo } ) ) )
134123, 133mpbird 236 . . . . . . . . . 10  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) : { 1 } --> ( RR*  \  { -oo } ) )
13553, 57mp1i 13 . . . . . . . . . 10  |-  ( ph  ->  0  e.  ( RR*  \  { -oo } ) )
13661adantl 468 . . . . . . . . . 10  |-  ( (
ph  /\  x  e.  RR* )  ->  ( (
0 +e x )  =  x  /\  ( x +e 0 )  =  x ) )
13721, 22, 23, 112, 114, 115, 134, 135, 136gsumress 16512 . . . . . . . . 9  |-  ( ph  ->  ( RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
138 fconstmpt 4895 . . . . . . . . . . 11  |-  ( { 1 }  X.  {
( X E Y ) } )  =  ( j  e.  {
1 }  |->  ( X E Y ) )
139132, 138syl6eq 2480 . . . . . . . . . 10  |-  ( ph  ->  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } )  =  ( j  e.  {
1 }  |->  ( X E Y ) ) )
140139oveq2d 6319 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )  =  ( W  gsumg  ( j  e.  { 1 } 
|->  ( X E Y ) ) ) )
141 cmnmnd 17438 . . . . . . . . . . 11  |-  ( W  e. CMnd  ->  W  e.  Mnd )
14267, 141mp1i 13 . . . . . . . . . 10  |-  ( ph  ->  W  e.  Mnd )
14387a1i 11 . . . . . . . . . 10  |-  ( ph  ->  1  e.  NN )
144 eqidd 2424 . . . . . . . . . . 11  |-  ( j  =  1  ->  ( X E Y )  =  ( X E Y ) )
14565, 144gsumsn 17580 . . . . . . . . . 10  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( X E Y )  e.  ( RR*  \  { -oo } ) )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
146142, 143, 121, 145syl3anc 1265 . . . . . . . . 9  |-  ( ph  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( X E Y ) ) )  =  ( X E Y ) )
147137, 140, 1463eqtrrd 2469 . . . . . . . 8  |-  ( ph  ->  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
148 fveq1 5878 . . . . . . . . . . . . . . 15  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  ( { <. 1 ,  <. X ,  Y >. >. } `  1
) )
14988, 89fvsn 6110 . . . . . . . . . . . . . . 15  |-  ( {
<. 1 ,  <. X ,  Y >. >. } ` 
1 )  =  <. X ,  Y >.
150148, 149syl6eq 2480 . . . . . . . . . . . . . 14  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
g `  1 )  =  <. X ,  Y >. )
151150fveq2d 5883 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 1st `  ( g ` 
1 ) )  =  ( 1st `  <. X ,  Y >. )
)
152151fveq2d 5883 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  ( 1st `  <. X ,  Y >. ) ) )
153152eqeq1d 2425 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  <. X ,  Y >. )
)  =  ( F `
 X ) ) )
154150fveq2d 5883 . . . . . . . . . . . . 13  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( 2nd `  ( g ` 
1 ) )  =  ( 2nd `  <. X ,  Y >. )
)
155154fveq2d 5883 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  ( 2nd `  <. X ,  Y >. ) ) )
156155eqeq1d 2425 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( F `  ( 2nd `  ( g ` 
1 ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  <. X ,  Y >. )
)  =  ( F `
 Y ) ) )
157153, 156anbi12d 716 . . . . . . . . . 10  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  <->  ( ( F `  ( 1st ` 
<. X ,  Y >. ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y ) ) ) )
158 coeq2 5010 . . . . . . . . . . . 12  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( E  o.  g )  =  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) )
159158oveq2d 6319 . . . . . . . . . . 11  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  ( RR*s  gsumg  ( E  o.  g
) )  =  (
RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) )
160159eqeq2d 2437 . . . . . . . . . 10  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( X E Y )  =  ( RR*s  gsumg  ( E  o.  g
) )  <->  ( X E Y )  =  (
RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) ) )
161157, 160anbi12d 716 . . . . . . . . 9  |-  ( g  =  { <. 1 ,  <. X ,  Y >. >. }  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 1 ) ) )  =  ( F `
 Y ) )  /\  ( X E Y )  =  (
RR*s  gsumg  ( E  o.  g
) ) )  <->  ( (
( F `  ( 1st `  <. X ,  Y >. ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  <. X ,  Y >. ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  { <. 1 ,  <. X ,  Y >. >. } ) ) ) ) )
162161rspcev 3183 . . . . . . . 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 ) ) ) )
163104, 111, 147, 162syl12anc 1263 . . . . . . 7  |-  ( ph  ->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) )
164 ovex 6331 . . . . . . . . . 10  |-  ( X E Y )  e. 
_V
16575elrnmpt 5098 . . . . . . . . . 10  |-  ( ( X E Y )  e.  _V  ->  (
( X E Y )  e.  ran  (
g  e.  S  |->  (
RR*s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  ( X E Y )  =  (
RR*s  gsumg  ( E  o.  g
) ) ) )
166164, 165ax-mp 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
) ) )
16715rexeqi 3031 . . . . . . . . . . 11  |-  ( E. g  e.  S  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) )  <->  E. g  e.  {
h  e.  ( ( V  X.  V )  ^m  ( 1 ... n ) )  |  ( ( F `  ( 1st `  ( h `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( h `
 i ) ) )  =  ( F `
 ( 1st `  (
h `  ( i  +  1 ) ) ) ) ) }  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g
) ) )
168 fveq1 5878 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  1 )  =  ( g ` 
1 ) )
169168fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 1st `  ( h ` 
1 ) )  =  ( 1st `  (
g `  1 )
) )
170169fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  1
) ) )  =  ( F `  ( 1st `  ( g ` 
1 ) ) ) )
171170eqeq1d 2425 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 1st `  ( h ` 
1 ) ) )  =  ( F `  X )  <->  ( F `  ( 1st `  (
g `  1 )
) )  =  ( F `  X ) ) )
172 fveq1 5878 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  (
h `  n )  =  ( g `  n ) )
173172fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( 2nd `  ( h `  n ) )  =  ( 2nd `  (
g `  n )
) )
174173fveq2d 5883 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  ( 2nd `  ( g `  n ) ) ) )
175174eqeq1d 2425 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y ) ) )
176 fveq1 5878 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  i )  =  ( g `  i ) )
177176fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 2nd `  ( h `  i ) )  =  ( 2nd `  (
g `  i )
) )
178177fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 2nd `  ( g `  i ) ) ) )
179 fveq1 5878 . . . . . . . . . . . . . . . . 17  |-  ( h  =  g  ->  (
h `  ( i  +  1 ) )  =  ( g `  ( i  +  1 ) ) )
180179fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( h  =  g  ->  ( 1st `  ( h `  ( i  +  1 ) ) )  =  ( 1st `  (
g `  ( i  +  1 ) ) ) )
181180fveq2d 5883 . . . . . . . . . . . . . . 15  |-  ( h  =  g  ->  ( F `  ( 1st `  ( h `  (
i  +  1 ) ) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )
182178, 181eqeq12d 2445 . . . . . . . . . . . . . 14  |-  ( h  =  g  ->  (
( F `  ( 2nd `  ( h `  i ) ) )  =  ( F `  ( 1st `  ( h `
 ( i  +  1 ) ) ) )  <->  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
183182ralbidv 2865 . . . . . . . . . . . . 13  |-  ( h  =  g  ->  ( A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) )  <->  A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) )
184171, 175, 1833anbi123d 1336 . . . . . . . . . . . 12  |-  ( h  =  g  ->  (
( ( F `  ( 1st `  ( h `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( h `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( h `
 i ) ) )  =  ( F `
 ( 1st `  (
h `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  n )
) )  =  ( F `  Y )  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) ) )
185184rexrab 3236 . . . . . . . . . . 11  |-  ( E. g  e.  { h  e.  ( ( V  X.  V )  ^m  (
1 ... n ) )  |  ( ( F `
 ( 1st `  (
h `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( h `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( h `  i
) ) )  =  ( F `  ( 1st `  ( h `  ( i  +  1 ) ) ) ) ) }  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) )  <->  E. g  e.  (
( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) )
186167, 185bitri 253 . . . . . . . . . 10  |-  ( E. g  e.  S  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) )
187 oveq2 6311 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
1 ... n )  =  ( 1 ... 1
) )
188 1z 10969 . . . . . . . . . . . . . 14  |-  1  e.  ZZ
189 fzsn 11842 . . . . . . . . . . . . . 14  |-  ( 1  e.  ZZ  ->  (
1 ... 1 )  =  { 1 } )
190188, 189ax-mp 5 . . . . . . . . . . . . 13  |-  ( 1 ... 1 )  =  { 1 }
191187, 190syl6eq 2480 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
1 ... n )  =  { 1 } )
192191oveq2d 6319 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( V  X.  V
)  ^m  ( 1 ... n ) )  =  ( ( V  X.  V )  ^m  { 1 } ) )
193 df-3an 985 . . . . . . . . . . . . 13  |-  ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) )
194 ral0 3903 . . . . . . . . . . . . . . . 16  |-  A. i  e.  (/)  ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) )
195 oveq1 6310 . . . . . . . . . . . . . . . . . . . 20  |-  ( n  =  1  ->  (
n  -  1 )  =  ( 1  -  1 ) )
196 1m1e0 10680 . . . . . . . . . . . . . . . . . . . 20  |-  ( 1  -  1 )  =  0
197195, 196syl6eq 2480 . . . . . . . . . . . . . . . . . . 19  |-  ( n  =  1  ->  (
n  -  1 )  =  0 )
198197oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  ( 1 ... 0
) )
199 fz10 11822 . . . . . . . . . . . . . . . . . 18  |-  ( 1 ... 0 )  =  (/)
200198, 199syl6eq 2480 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  (
1 ... ( n  - 
1 ) )  =  (/) )
201200raleqdv 3032 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( A. i  e.  (
1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) )  <->  A. i  e.  (/)  ( F `
 ( 2nd `  (
g `  i )
) )  =  ( F `  ( 1st `  ( g `  (
i  +  1 ) ) ) ) ) )
202194, 201mpbiri 237 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )
203202biantrud 510 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  <->  ( (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) ) )
204 fveq2 5879 . . . . . . . . . . . . . . . . . 18  |-  ( n  =  1  ->  (
g `  n )  =  ( g ` 
1 ) )
205204fveq2d 5883 . . . . . . . . . . . . . . . . 17  |-  ( n  =  1  ->  ( 2nd `  ( g `  n ) )  =  ( 2nd `  (
g `  1 )
) )
206205fveq2d 5883 . . . . . . . . . . . . . . . 16  |-  ( n  =  1  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  ( 2nd `  ( g ` 
1 ) ) ) )
207206eqeq1d 2425 . . . . . . . . . . . . . . 15  |-  ( n  =  1  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) )
208207anbi2d 709 . . . . . . . . . . . . . 14  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
209203, 208bitr3d 259 . . . . . . . . . . . . 13  |-  ( n  =  1  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y ) )  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
210193, 209syl5bb 261 . . . . . . . . . . . 12  |-  ( n  =  1  ->  (
( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) )  <->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) ) ) )
211210anbi1d 710 . . . . . . . . . . 11  |-  ( n  =  1  ->  (
( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) )  <->  ( ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  /\  ( F `  ( 2nd `  (
g `  1 )
) )  =  ( F `  Y ) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) ) )
212192, 211rexeqbidv 3041 . . . . . . . . . 10  |-  ( n  =  1  ->  ( E. g  e.  (
( V  X.  V
)  ^m  ( 1 ... n ) ) ( ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) ) )
213186, 212syl5bb 261 . . . . . . . . 9  |-  ( n  =  1  ->  ( E. g  e.  S  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) )  <->  E. g  e.  ( ( V  X.  V
)  ^m  { 1 } ) ( ( ( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) ) )
214166, 213syl5bb 261 . . . . . . . 8  |-  ( n  =  1  ->  (
( X E Y )  e.  ran  (
g  e.  S  |->  (
RR*s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  ( ( V  X.  V )  ^m  {
1 } ) ( ( ( F `  ( 1st `  ( g `
 1 ) ) )  =  ( F `
 X )  /\  ( F `  ( 2nd `  ( g `  1
) ) )  =  ( F `  Y
) )  /\  ( X E Y )  =  ( RR*s  gsumg  ( E  o.  g ) ) ) ) )
215214rspcev 3183 . . . . . . 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 ) ) ) )
21687, 163, 215sylancr 668 . . . . . 6  |-  ( ph  ->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) )
217 eliun 4302 . . . . . 6  |-  ( ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) )  <->  E. n  e.  NN  ( X E Y )  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
218216, 217sylibr 216 . . . . 5  |-  ( ph  ->  ( X E Y )  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) ) )
219218, 18syl6eleqr 2522 . . . 4  |-  ( ph  ->  ( X E Y )  e.  T )
220 infxrlb 11622 . . . 4  |-  ( ( T  C_  RR*  /\  ( X E Y )  e.  T )  -> inf ( T ,  RR* ,  <  )  <_  ( X E Y ) )
22182, 219, 220syl2anc 666 . . 3  |-  ( ph  -> inf ( T ,  RR* ,  <  )  <_  ( X E Y ) )
22218eleq2i 2501 . . . . . . 7  |-  ( p  e.  T  <->  p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
223 eliun 4302 . . . . . . 7  |-  ( p  e.  U_ n  e.  NN  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g
) ) )  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
224222, 223bitri 253 . . . . . 6  |-  ( p  e.  T  <->  E. n  e.  NN  p  e.  ran  ( g  e.  S  |->  ( RR*s  gsumg  ( E  o.  g ) ) ) )
225 vex 3085 . . . . . . . . 9  |-  p  e. 
_V
22675elrnmpt 5098 . . . . . . . . 9  |-  ( p  e.  _V  ->  (
p  e.  ran  (
g  e.  S  |->  (
RR*s  gsumg  ( E  o.  g
) ) )  <->  E. g  e.  S  p  =  ( RR*s  gsumg  ( E  o.  g
) ) ) )
227225, 226ax-mp 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
) ) )
228184, 15elrab2 3232 . . . . . . . . . . . . . . . . 17  |-  ( g  e.  S  <->  ( g  e.  ( ( V  X.  V )  ^m  (
1 ... n ) )  /\  ( ( F `
 ( 1st `  (
g `  1 )
) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `
 n ) ) )  =  ( F `
 Y )  /\  A. i  e.  ( 1 ... ( n  - 
1 ) ) ( F `  ( 2nd `  ( g `  i
) ) )  =  ( F `  ( 1st `  ( g `  ( i  +  1 ) ) ) ) ) ) )
229228simprbi 466 . . . . . . . . . . . . . . . 16  |-  ( g  e.  S  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
230229adantl 468 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  /\  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  /\  A. i  e.  ( 1 ... (
n  -  1 ) ) ( F `  ( 2nd `  ( g `
 i ) ) )  =  ( F `
 ( 1st `  (
g `  ( i  +  1 ) ) ) ) ) )
231230simp2d 1019 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
) )
2323ad2antrr 731 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-onto-> B )
233 f1of1 5828 . . . . . . . . . . . . . . . 16  |-  ( F : V -1-1-onto-> B  ->  F : V -1-1-> B )
234232, 233syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  F : V -1-1-> B )
235 simplr 761 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  NN )
236 elfz1end 11831 . . . . . . . . . . . . . . . . . 18  |-  ( n  e.  NN  <->  n  e.  ( 1 ... n
) )
237235, 236sylib 200 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( 1 ... n
) )
23850, 237ffvelrnd 6036 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  n )  e.  ( V  X.  V
) )
239 xp2nd 6836 . . . . . . . . . . . . . . . 16  |-  ( ( g `  n )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  n ) )  e.  V )
240238, 239syl 17 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  e.  V )
24113ad2antrr 731 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  Y  e.  V )
242 f1fveq 6176 . . . . . . . . . . . . . . 15  |-  ( ( F : V -1-1-> B  /\  ( ( 2nd `  (
g `  n )
)  e.  V  /\  Y  e.  V )
)  ->  ( ( F `  ( 2nd `  ( g `  n
) ) )  =  ( F `  Y
)  <->  ( 2nd `  (
g `  n )
)  =  Y ) )
243234, 240, 241, 242syl12anc 1263 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 2nd `  ( g `  n ) ) )  =  ( F `  Y )  <->  ( 2nd `  ( g `  n
) )  =  Y ) )
244231, 243mpbid 214 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g `  n ) )  =  Y )
245244oveq2d 6319 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  n )
) )  =  ( X E Y ) )
246 eleq1 2495 . . . . . . . . . . . . . . . . 17  |-  ( m  =  1  ->  (
m  e.  ( 1 ... n )  <->  1  e.  ( 1 ... n
) ) )
247 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
g `  m )  =  ( g ` 
1 ) )
248247fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  1 )
) )
249248oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  1
) ) ) )
250 oveq2 6311 . . . . . . . . . . . . . . . . . . . . 21  |-  ( m  =  1  ->  (
1 ... m )  =  ( 1 ... 1
) )
251250, 190syl6eq 2480 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  1  ->  (
1 ... m )  =  { 1 } )
252251reseq2d 5122 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  1  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  { 1 } ) )
253252oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  1  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
254249, 253breq12d 4434 . . . . . . . . . . . . . . . . 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 } ) ) ) )
255246, 254imbi12d 322 . . . . . . . . . . . . . . . 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 } ) ) ) ) )
256255imbi2d 318 . . . . . . . . . . . . . . 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 } ) ) ) ) ) )
257 eleq1 2495 . . . . . . . . . . . . . . . . 17  |-  ( m  =  x  ->  (
m  e.  ( 1 ... n )  <->  x  e.  ( 1 ... n
) ) )
258 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
g `  m )  =  ( g `  x ) )
259258fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  x )
) )
260259oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  x
) ) ) )
261 oveq2 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  x  ->  (
1 ... m )  =  ( 1 ... x
) )
262261reseq2d 5122 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  x  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... x ) ) )
263262oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  x  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... x ) ) ) )
264260, 263breq12d 4434 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
265257, 264imbi12d 322 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
266265imbi2d 318 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
267 eleq1 2495 . . . . . . . . . . . . . . . . 17  |-  ( m  =  ( x  + 
1 )  ->  (
m  e.  ( 1 ... n )  <->  ( x  +  1 )  e.  ( 1 ... n
) ) )
268 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
g `  m )  =  ( g `  ( x  +  1
) ) )
269268fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  ( x  +  1 ) ) ) )
270269oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  (
x  +  1 ) ) ) ) )
271 oveq2 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  ( x  + 
1 )  ->  (
1 ... m )  =  ( 1 ... (
x  +  1 ) ) )
272271reseq2d 5122 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  ( x  + 
1 )  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) )
273272oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  ( x  + 
1 )  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... ( x  + 
1 ) ) ) ) )
274270, 273breq12d 4434 . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
275267, 274imbi12d 322 . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
276275imbi2d 318 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
277 eleq1 2495 . . . . . . . . . . . . . . . . 17  |-  ( m  =  n  ->  (
m  e.  ( 1 ... n )  <->  n  e.  ( 1 ... n
) ) )
278 fveq2 5879 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
g `  m )  =  ( g `  n ) )
279278fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  ( 2nd `  ( g `  m ) )  =  ( 2nd `  (
g `  n )
) )
280279oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( X E ( 2nd `  (
g `  m )
) )  =  ( X E ( 2nd `  ( g `  n
) ) ) )
281 oveq2 6311 . . . . . . . . . . . . . . . . . . . 20  |-  ( m  =  n  ->  (
1 ... m )  =  ( 1 ... n
) )
282281reseq2d 5122 . . . . . . . . . . . . . . . . . . 19  |-  ( m  =  n  ->  (
( E  o.  g
)  |`  ( 1 ... m ) )  =  ( ( E  o.  g )  |`  (
1 ... n ) ) )
283282oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( m  =  n  ->  ( W  gsumg  ( ( E  o.  g )  |`  (
1 ... m ) ) )  =  ( W 
gsumg  ( ( E  o.  g )  |`  (
1 ... n ) ) ) )
284280, 283breq12d 4434 . . . . . . . . . . . . . . . . 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 ) ) ) ) )
285277, 284imbi12d 322 . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
286285imbi2d 318 . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
28729ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E  e.  ( *Met `  V ) )
28811ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  X  e.  V )
289 nnuz 11196 . . . . . . . . . . . . . . . . . . . . . . 23  |-  NN  =  ( ZZ>= `  1 )
290235, 289syl6eleq 2521 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  n  e.  ( ZZ>= `  1 )
)
291 eluzfz1 11808 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( n  e.  ( ZZ>= `  1
)  ->  1  e.  ( 1 ... n
) )
292290, 291syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  ( 1 ... n
) )
29350, 292ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  e.  ( V  X.  V
) )
294 xp2nd 6836 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
295293, 294syl 17 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 2nd `  ( g ` 
1 ) )  e.  V )
296 xmetcl 21338 . . . . . . . . . . . . . . . . . . 19  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  1 )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
297287, 288, 295, 296syl3anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  e.  RR* )
298 xrleid 11451 . . . . . . . . . . . . . . . . . 18  |-  ( ( X E ( 2nd `  ( g `  1
) ) )  e. 
RR*  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
299297, 298syl 17 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( X E ( 2nd `  (
g `  1 )
) ) )
300142ad2antrr 731 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  W  e.  Mnd )
30187a1i 11 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  1  e.  NN )
30244, 293ffvelrnd 6036 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  ( g `  1 ) )  e.  ( RR*  \  { -oo } ) )
303 fveq2 5879 . . . . . . . . . . . . . . . . . . . . 21  |-  ( j  =  1  ->  (
g `  j )  =  ( g ` 
1 ) )
304303fveq2d 5883 . . . . . . . . . . . . . . . . . . . 20  |-  ( j  =  1  ->  ( E `  ( g `  j ) )  =  ( E `  (
g `  1 )
) )
30565, 304gsumsn 17580 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W  e.  Mnd  /\  1  e.  NN  /\  ( E `  ( g `  1 ) )  e.  ( RR*  \  { -oo } ) )  -> 
( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
306300, 301, 302, 305syl3anc 1265 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) )  =  ( E `
 ( g ` 
1 ) ) )
307287, 30syl 17 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  E : ( V  X.  V ) --> RR* )
308 fcompt 6072 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( E : ( V  X.  V ) --> RR* 
/\  g : ( 1 ... n ) --> ( V  X.  V
) )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
309307, 50, 308syl2anc 666 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E  o.  g )  =  ( j  e.  ( 1 ... n
)  |->  ( E `  ( g `  j
) ) ) )
310309reseq1d 5121 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( ( j  e.  ( 1 ... n )  |->  ( E `  ( g `
 j ) ) )  |`  { 1 } ) )
311292snssd 4143 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  { 1 }  C_  ( 1 ... n ) )
312311resmptd 5173 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( j  e.  ( 1 ... n ) 
|->  ( E `  (
g `  j )
) )  |`  { 1 } )  =  ( j  e.  { 1 }  |->  ( E `  ( g `  j
) ) ) )
313310, 312eqtrd 2464 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( E  o.  g
)  |`  { 1 } )  =  ( j  e.  { 1 } 
|->  ( E `  (
g `  j )
) ) )
314313oveq2d 6319 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( W  gsumg  ( j  e.  {
1 }  |->  ( E `
 ( g `  j ) ) ) ) )
315 df-ov 6306 . . . . . . . . . . . . . . . . . . 19  |-  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )
316 1st2nd2 6842 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
317293, 316syl 17 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
g `  1 )  =  <. ( 1st `  (
g `  1 )
) ,  ( 2nd `  ( g `  1
) ) >. )
318230simp1d 1018 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
) )
319 xp1st 6835 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  1 )  e.  ( V  X.  V )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
320293, 319syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  e.  V )
321 f1fveq 6176 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( F : V -1-1-> B  /\  ( ( 1st `  (
g `  1 )
)  e.  V  /\  X  e.  V )
)  ->  ( ( F `  ( 1st `  ( g `  1
) ) )  =  ( F `  X
)  <->  ( 1st `  (
g `  1 )
)  =  X ) )
322234, 320, 288, 321syl12anc 1263 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
( F `  ( 1st `  ( g ` 
1 ) ) )  =  ( F `  X )  <->  ( 1st `  ( g `  1
) )  =  X ) )
323318, 322mpbid 214 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( 1st `  ( g ` 
1 ) )  =  X )
324323opeq1d 4191 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. ( 1st `  ( g ` 
1 ) ) ,  ( 2nd `  (
g `  1 )
) >.  =  <. X , 
( 2nd `  (
g `  1 )
) >. )
325317, 324eqtr2d 2465 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  <. X , 
( 2nd `  (
g `  1 )
) >.  =  ( g `
 1 ) )
326325fveq2d 5883 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( E `  <. X , 
( 2nd `  (
g `  1 )
) >. )  =  ( E `  ( g `
 1 ) ) )
327315, 326syl5eq 2476 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  =  ( E `  ( g `
 1 ) ) )
328306, 314, 3273eqtr4d 2474 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) )  =  ( X E ( 2nd `  ( g `
 1 ) ) ) )
329299, 328breqtrrd 4448 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  ( X E ( 2nd `  (
g `  1 )
) )  <_  ( W  gsumg  ( ( E  o.  g )  |`  { 1 } ) ) )
330329a1d 27 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S )  ->  (
1  e.  ( 1 ... n )  -> 
( X E ( 2nd `  ( g `
 1 ) ) )  <_  ( W  gsumg  ( ( E  o.  g
)  |`  { 1 } ) ) ) )
331 simprl 763 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  NN )
332331, 289syl6eleq 2521 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( ZZ>= ` 
1 ) )
333 simprr 765 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( x  +  1 )  e.  ( 1 ... n ) )
334 peano2fzr 11814 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( x  e.  ( ZZ>= ` 
1 )  /\  (
x  +  1 )  e.  ( 1 ... n ) )  ->  x  e.  ( 1 ... n ) )
335332, 333, 334syl2anc 666 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ( 1 ... n ) )
336335expr 619 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  x  e.  NN )  ->  ( ( x  +  1 )  e.  ( 1 ... n )  ->  x  e.  ( 1 ... n
) ) )
337336imim1d 79 . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
338287adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E  e.  ( *Met `  V ) )
339288adantr 467 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  X  e.  V )
34050adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
g : ( 1 ... n ) --> ( V  X.  V ) )
341340, 335ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( g `  x
)  e.  ( V  X.  V ) )
342 xp2nd 6836 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( g `  x )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  x ) )  e.  V )
343341, 342syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  x )
)  e.  V )
344 xmetcl 21338 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( E  e.  ( *Met `  V )  /\  X  e.  V  /\  ( 2nd `  (
g `  x )
)  e.  V )  ->  ( X E ( 2nd `  (
g `  x )
) )  e.  RR* )
345338, 339, 343, 344syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( X E ( 2nd `  ( g `
 x ) ) )  e.  RR* )
34667a1i 11 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  W  e. CMnd )
347 fzfid 12187 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  e.  Fin )
34852adantr 467 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E  o.  g
) : ( 1 ... n ) --> (
RR*  \  { -oo }
) )
349 fzsuc 11845 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( x  e.  ( ZZ>= `  1
)  ->  ( 1 ... ( x  + 
1 ) )  =  ( ( 1 ... x )  u.  {
( x  +  1 ) } ) )
350332, 349syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  =  ( ( 1 ... x )  u.  { ( x  +  1 ) } ) )
351 elfzuz3 11799 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ( x  +  1 )  e.  ( 1 ... n )  ->  n  e.  ( ZZ>= `  ( x  +  1 ) ) )
352351ad2antll 734 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  n  e.  ( ZZ>= `  ( x  +  1
) ) )
353 fzss2 11840 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( n  e.  ( ZZ>= `  (
x  +  1 ) )  ->  ( 1 ... ( x  + 
1 ) )  C_  ( 1 ... n
) )
354352, 353syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... (
x  +  1 ) )  C_  ( 1 ... n ) )
355350, 354eqsstr3d 3500 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( ( 1 ... x )  u.  {
( x  +  1 ) } )  C_  ( 1 ... n
) )
356355unssad 3644 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 1 ... x
)  C_  ( 1 ... n ) )
357348, 356fssresd 5765 . . . . . . . . . . . . . . . . . . . . . . . . 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, 347, 358fdmfifsupp 7897 . . . . . . . . . . . . . . . . . . . . . . . . 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, 346, 347, 357, 359gsumcl 17542 . . . . . . . . . . . . . . . . . . . . . . . 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 3449 . . . . . . . . . . . . . . . . . . . . . . 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* )
362338, 30syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  E : ( V  X.  V ) --> RR* )
363340, 333ffvelrnd 6036 . . . . . . . . . . . . . . . . . . . . . . . 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 6036 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( E `  (
g `  ( x  +  1 ) ) )  e.  RR* )
365 xleadd1a 11541 . . . . . . . . . . . . . . . . . . . . . . . 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 436 . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
367345, 361, 364, 366syl3anc 1265 . . . . . . . . . . . . . . . . . . . . . 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 6836 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  ( 2nd `  ( g `  ( x  +  1
) ) )  e.  V )
369363, 368syl 17 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( 2nd `  (
g `  ( x  +  1 ) ) )  e.  V )
370 xmettri 21358 . . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
371338, 339, 369, 343, 370syl13anc 1267 . . . . . . . . . . . . . . . . . . . . . . . 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 6842 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( ( g `  ( x  +  1 ) )  e.  ( V  X.  V )  ->  (
g `  ( x  +  1 ) )  =  <. ( 1st `  (
g `  ( x  +  1 ) ) ) ,  ( 2nd `  ( g `  (
x  +  1 ) ) ) >. )
373363, 372syl 17 . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10961 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34  |-  ( x  e.  NN  ->  x  e.  ZZ )
375374ad2antrl 733 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  ->  x  e.  ZZ )
376 eluzp1m1 11184 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33  |-  ( ( x  e.  ZZ  /\  n  e.  ( ZZ>= `  ( x  +  1
) ) )  -> 
( n  -  1 )  e.  ( ZZ>= `  x ) )
377375, 352, 376syl2anc 666 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( ( ( ( ph  /\  n  e.  NN )  /\  g  e.  S
)  /\  ( x  e.  NN  /\  ( x  +  1 )  e.  ( 1 ... n
) ) )  -> 
( n  -  1 )  e.  ( ZZ>= `  x ) )
378 elfzuzb 11796 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32  |-  ( x  e.  ( 1 ... ( n  -  1 ) )  <->  ( x  e.  ( ZZ>= `  1 )  /\  ( n  -  1 )  e.  ( ZZ>= `  x ) ) )
379332, 377, 378sylanbrc