This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem imasdsf1olem

Description: Lemma for imasdsf1o . (Contributed by Mario Carneiro, 21-Aug-2015) (Proof shortened by AV, 6-Oct-2020)

Ref Expression
Hypotheses 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*s |`s ( 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 gsum ( E o. g ) ) )
Assertion imasdsf1olem 
|- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )

Proof

Step Hyp Ref Expression
1 imasdsf1o.u 
 |-  ( ph -> U = ( F "s R ) )
2 imasdsf1o.v 
 |-  ( ph -> V = ( Base ` R ) )
3 imasdsf1o.f 
 |-  ( ph -> F : V -1-1-onto-> B )
4 imasdsf1o.r 
 |-  ( ph -> R e. Z )
5 imasdsf1o.e 
 |-  E = ( ( dist ` R ) |` ( V X. V ) )
6 imasdsf1o.d 
 |-  D = ( dist ` U )
7 imasdsf1o.m 
 |-  ( ph -> E e. ( *Met ` V ) )
8 imasdsf1o.x 
 |-  ( ph -> X e. V )
9 imasdsf1o.y 
 |-  ( ph -> Y e. V )
10 imasdsf1o.w 
 |-  W = ( RR*s |`s ( RR* \ { -oo } ) )
11 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 ) ) ) ) ) }
12 imasdsf1o.t 
 |-  T = U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) )
13 f1ofo 
 |-  ( F : V -1-1-onto-> B -> F : V -onto-> B )
14 3 13 syl 
 |-  ( ph -> F : V -onto-> B )
15 eqid 
 |-  ( dist ` R ) = ( dist ` R )
16 f1of 
 |-  ( F : V -1-1-onto-> B -> F : V --> B )
17 3 16 syl 
 |-  ( ph -> F : V --> B )
18 17 8 ffvelcdmd 
 |-  ( ph -> ( F ` X ) e. B )
19 17 9 ffvelcdmd 
 |-  ( ph -> ( F ` Y ) e. B )
20 1 2 14 4 15 6 18 19 11 5 imasdsval2 
 |-  ( ph -> ( ( F ` X ) D ( F ` Y ) ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < ) )
21 12 infeq1i 
 |-  inf ( T , RR* , < ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) , RR* , < )
22 20 21 eqtr4di 
 |-  ( ph -> ( ( F ` X ) D ( F ` Y ) ) = inf ( T , RR* , < ) )
23 xrsbas 
 |-  RR* = ( Base ` RR*s )
24 xrsadd 
 |-  +e = ( +g ` RR*s )
25 xrsex 
 |-  RR*s e. _V
26 25 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR*s e. _V )
27 fzfid 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
28 difss 
 |-  ( RR* \ { -oo } ) C_ RR*
29 28 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR* \ { -oo } ) C_ RR* )
30 xmetf 
 |-  ( E e. ( *Met ` V ) -> E : ( V X. V ) --> RR* )
31 ffn 
 |-  ( E : ( V X. V ) --> RR* -> E Fn ( V X. V ) )
32 7 30 31 3syl 
 |-  ( ph -> E Fn ( V X. V ) )
33 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34 xmetge0 
 |-  ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35 ge0nemnf 
 |-  ( ( ( f E g ) e. RR* /\ 0 <_ ( f E g ) ) -> ( f E g ) =/= -oo )
36 33 34 35 syl2anc 
 |-  ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) =/= -oo )
37 eldifsn 
 |-  ( ( f E g ) e. ( RR* \ { -oo } ) <-> ( ( f E g ) e. RR* /\ ( f E g ) =/= -oo ) )
38 33 36 37 sylanbrc 
 |-  ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. ( RR* \ { -oo } ) )
39 38 3expb 
 |-  ( ( E e. ( *Met ` V ) /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
40 7 39 sylan 
 |-  ( ( ph /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
41 40 ralrimivva 
 |-  ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42 ffnov 
 |-  ( 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 } ) ) )
43 32 41 42 sylanbrc 
 |-  ( ph -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
44 43 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
45 11 ssrab3 
 |-  S C_ ( ( V X. V ) ^m ( 1 ... n ) )
46 45 a1i 
 |-  ( ( ph /\ n e. NN ) -> S C_ ( ( V X. V ) ^m ( 1 ... n ) ) )
47 46 sselda 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
48 elmapi 
 |-  ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
49 47 48 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g : ( 1 ... n ) --> ( V X. V ) )
50 fco 
 |-  ( ( E : ( V X. V ) --> ( RR* \ { -oo } ) /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
51 44 49 50 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
52 0re 
 |-  0 e. RR
53 rexr 
 |-  ( 0 e. RR -> 0 e. RR* )
54 renemnf 
 |-  ( 0 e. RR -> 0 =/= -oo )
55 eldifsn 
 |-  ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
56 53 54 55 sylanbrc 
 |-  ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
57 52 56 mp1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. ( RR* \ { -oo } ) )
58 xaddlid 
 |-  ( x e. RR* -> ( 0 +e x ) = x )
59 xaddrid 
 |-  ( x e. RR* -> ( x +e 0 ) = x )
60 58 59 jca 
 |-  ( x e. RR* -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
61 60 adantl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
62 23 24 10 26 27 29 51 57 61 gsumress 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsum ( E o. g ) ) = ( W gsum ( E o. g ) ) )
63 10 23 ressbas2 
 |-  ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
64 28 63 ax-mp 
 |-  ( RR* \ { -oo } ) = ( Base ` W )
65 10 xrs10 
 |-  0 = ( 0g ` W )
66 10 xrs1cmn 
 |-  W e. CMnd
67 66 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
68 c0ex 
 |-  0 e. _V
69 68 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. _V )
70 51 27 69 fdmfifsupp 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) finSupp 0 )
71 64 65 67 27 51 70 gsumcl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsum ( E o. g ) ) e. ( RR* \ { -oo } ) )
72 62 71 eqeltrd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsum ( E o. g ) ) e. ( RR* \ { -oo } ) )
73 72 eldifad 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsum ( E o. g ) ) e. RR* )
74 73 fmpttd 
 |-  ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) : S --> RR* )
75 74 frnd 
 |-  ( ( ph /\ n e. NN ) -> ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) C_ RR* )
76 75 ralrimiva 
 |-  ( ph -> A. n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) C_ RR* )
77 iunss 
 |-  ( U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) C_ RR* <-> A. n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) C_ RR* )
78 76 77 sylibr 
 |-  ( ph -> U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) C_ RR* )
79 12 78 eqsstrid 
 |-  ( ph -> T C_ RR* )
80 infxrcl 
 |-  ( T C_ RR* -> inf ( T , RR* , < ) e. RR* )
81 79 80 syl 
 |-  ( ph -> inf ( T , RR* , < ) e. RR* )
82 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
83 7 8 9 82 syl3anc 
 |-  ( ph -> ( X E Y ) e. RR* )
84 1nn 
 |-  1 e. NN
85 1ex 
 |-  1 e. _V
86 opex 
 |-  <. X , Y >. e. _V
87 85 86 f1osn 
 |-  { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
88 f1of 
 |-  ( { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. } -> { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } )
89 87 88 ax-mp 
 |-  { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. }
90 8 9 opelxpd 
 |-  ( ph -> <. X , Y >. e. ( V X. V ) )
91 90 snssd 
 |-  ( ph -> { <. X , Y >. } C_ ( V X. V ) )
92 fss 
 |-  ( ( { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } /\ { <. X , Y >. } C_ ( V X. V ) ) -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
93 89 91 92 sylancr 
 |-  ( ph -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
94 7 elfvexd 
 |-  ( ph -> V e. _V )
95 94 94 xpexd 
 |-  ( ph -> ( V X. V ) e. _V )
96 snex 
 |-  { 1 } e. _V
97 elmapg 
 |-  ( ( ( V X. V ) e. _V /\ { 1 } e. _V ) -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
98 95 96 97 sylancl 
 |-  ( ph -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
99 93 98 mpbird 
 |-  ( ph -> { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) )
100 op1stg 
 |-  ( ( X e. V /\ Y e. V ) -> ( 1st ` <. X , Y >. ) = X )
101 8 9 100 syl2anc 
 |-  ( ph -> ( 1st ` <. X , Y >. ) = X )
102 101 fveq2d 
 |-  ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
103 op2ndg 
 |-  ( ( X e. V /\ Y e. V ) -> ( 2nd ` <. X , Y >. ) = Y )
104 8 9 103 syl2anc 
 |-  ( ph -> ( 2nd ` <. X , Y >. ) = Y )
105 104 fveq2d 
 |-  ( ph -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
106 102 105 jca 
 |-  ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
107 25 a1i 
 |-  ( ph -> RR*s e. _V )
108 snfi 
 |-  { 1 } e. Fin
109 108 a1i 
 |-  ( ph -> { 1 } e. Fin )
110 28 a1i 
 |-  ( ph -> ( RR* \ { -oo } ) C_ RR* )
111 xmetge0 
 |-  ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
112 7 8 9 111 syl3anc 
 |-  ( ph -> 0 <_ ( X E Y ) )
113 ge0nemnf 
 |-  ( ( ( X E Y ) e. RR* /\ 0 <_ ( X E Y ) ) -> ( X E Y ) =/= -oo )
114 83 112 113 syl2anc 
 |-  ( ph -> ( X E Y ) =/= -oo )
115 eldifsn 
 |-  ( ( X E Y ) e. ( RR* \ { -oo } ) <-> ( ( X E Y ) e. RR* /\ ( X E Y ) =/= -oo ) )
116 83 114 115 sylanbrc 
 |-  ( ph -> ( X E Y ) e. ( RR* \ { -oo } ) )
117 fconst6g 
 |-  ( ( X E Y ) e. ( RR* \ { -oo } ) -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
118 116 117 syl 
 |-  ( ph -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
119 fcoconst 
 |-  ( ( E Fn ( V X. V ) /\ <. X , Y >. e. ( V X. V ) ) -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
120 32 90 119 syl2anc 
 |-  ( ph -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
121 85 86 xpsn 
 |-  ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
122 121 coeq2i 
 |-  ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
123 df-ov 
 |-  ( X E Y ) = ( E ` <. X , Y >. )
124 123 eqcomi 
 |-  ( E ` <. X , Y >. ) = ( X E Y )
125 124 sneqi 
 |-  { ( E ` <. X , Y >. ) } = { ( X E Y ) }
126 125 xpeq2i 
 |-  ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
127 120 122 126 3eqtr3g 
 |-  ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
128 127 feq1d 
 |-  ( ph -> ( ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) <-> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) ) )
129 118 128 mpbird 
 |-  ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) )
130 52 56 mp1i 
 |-  ( ph -> 0 e. ( RR* \ { -oo } ) )
131 60 adantl 
 |-  ( ( ph /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
132 23 24 10 107 109 110 129 130 131 gsumress 
 |-  ( ph -> ( RR*s gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) )
133 fconstmpt 
 |-  ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
134 127 133 eqtrdi 
 |-  ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
135 134 oveq2d 
 |-  ( ph -> ( W gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsum ( j e. { 1 } |-> ( X E Y ) ) ) )
136 cmnmnd 
 |-  ( W e. CMnd -> W e. Mnd )
137 66 136 mp1i 
 |-  ( ph -> W e. Mnd )
138 84 a1i 
 |-  ( ph -> 1 e. NN )
139 eqidd 
 |-  ( j = 1 -> ( X E Y ) = ( X E Y ) )
140 64 139 gsumsn 
 |-  ( ( W e. Mnd /\ 1 e. NN /\ ( X E Y ) e. ( RR* \ { -oo } ) ) -> ( W gsum ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
141 137 138 116 140 syl3anc 
 |-  ( ph -> ( W gsum ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
142 132 135 141 3eqtrrd 
 |-  ( ph -> ( X E Y ) = ( RR*s gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) )
143 fveq1 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
144 85 86 fvsn 
 |-  ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
145 143 144 eqtrdi 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
146 145 fveq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
147 146 fveqeq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
148 145 fveq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
149 148 fveqeq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
150 147 149 anbi12d 
 |-  ( 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 ) ) ) )
151 coeq2 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
152 151 oveq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( RR*s gsum ( E o. g ) ) = ( RR*s gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) )
153 152 eqeq2d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( ( X E Y ) = ( RR*s gsum ( E o. g ) ) <-> ( X E Y ) = ( RR*s gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) ) )
154 150 153 anbi12d 
 |-  ( g = { <. 1 , <. X , Y >. >. } -> ( ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsum ( E o. g ) ) ) <-> ( ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsum ( E o. { <. 1 , <. X , Y >. >. } ) ) ) ) )
155 154 rspcev 
 |-  ( ( { <. 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 gsum ( 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 gsum ( E o. g ) ) ) )
156 99 106 142 155 syl12anc 
 |-  ( 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 gsum ( E o. g ) ) ) )
157 ovex 
 |-  ( X E Y ) e. _V
158 eqid 
 |-  ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsum ( E o. g ) ) )
159 158 elrnmpt 
 |-  ( ( X E Y ) e. _V -> ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. g e. S ( X E Y ) = ( RR*s gsum ( E o. g ) ) ) )
160 157 159 ax-mp 
 |-  ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. g e. S ( X E Y ) = ( RR*s gsum ( E o. g ) ) )
161 11 rexeqi 
 |-  ( E. g e. S ( X E Y ) = ( RR*s gsum ( 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 gsum ( E o. g ) ) )
162 fveq1 
 |-  ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
163 162 fveq2d 
 |-  ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
164 163 fveqeq2d 
 |-  ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
165 fveq1 
 |-  ( h = g -> ( h ` n ) = ( g ` n ) )
166 165 fveq2d 
 |-  ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
167 166 fveqeq2d 
 |-  ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
168 fveq1 
 |-  ( h = g -> ( h ` i ) = ( g ` i ) )
169 168 fveq2d 
 |-  ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
170 169 fveq2d 
 |-  ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
171 fveq1 
 |-  ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
172 171 fveq2d 
 |-  ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
173 172 fveq2d 
 |-  ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
174 170 173 eqeq12d 
 |-  ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
175 174 ralbidv 
 |-  ( 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 ) ) ) ) ) )
176 164 167 175 3anbi123d 
 |-  ( 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 ) ) ) ) ) ) )
177 176 rexrab 
 |-  ( 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 gsum ( 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 gsum ( E o. g ) ) ) )
178 161 177 bitri 
 |-  ( E. g e. S ( X E Y ) = ( RR*s gsum ( 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 gsum ( E o. g ) ) ) )
179 oveq2 
 |-  ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
180 1z 
 |-  1 e. ZZ
181 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
182 180 181 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
183 179 182 eqtrdi 
 |-  ( n = 1 -> ( 1 ... n ) = { 1 } )
184 183 oveq2d 
 |-  ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
185 df-3an 
 |-  ( ( ( 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 ) ) ) ) ) )
186 ral0 
 |-  A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
187 oveq1 
 |-  ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
188 1m1e0 
 |-  ( 1 - 1 ) = 0
189 187 188 eqtrdi 
 |-  ( n = 1 -> ( n - 1 ) = 0 )
190 189 oveq2d 
 |-  ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
191 fz10 
 |-  ( 1 ... 0 ) = (/)
192 190 191 eqtrdi 
 |-  ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
193 192 raleqdv 
 |-  ( 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 ) ) ) ) ) )
194 186 193 mpbiri 
 |-  ( n = 1 -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
195 194 biantrud 
 |-  ( 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 ) ) ) ) ) ) )
196 2fveq3 
 |-  ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
197 196 fveqeq2d 
 |-  ( n = 1 -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) )
198 197 anbi2d 
 |-  ( 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 ) ) ) )
199 195 198 bitr3d 
 |-  ( 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 ) ) ) )
200 185 199 bitrid 
 |-  ( 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 ) ) ) )
201 200 anbi1d 
 |-  ( 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 gsum ( E o. g ) ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsum ( E o. g ) ) ) ) )
202 184 201 rexeqbidv 
 |-  ( 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 gsum ( 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 gsum ( E o. g ) ) ) ) )
203 178 202 bitrid 
 |-  ( n = 1 -> ( E. g e. S ( X E Y ) = ( RR*s gsum ( 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 gsum ( E o. g ) ) ) ) )
204 160 203 bitrid 
 |-  ( n = 1 -> ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( 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 gsum ( E o. g ) ) ) ) )
205 204 rspcev 
 |-  ( ( 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 gsum ( E o. g ) ) ) ) -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
206 84 156 205 sylancr 
 |-  ( ph -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
207 eliun 
 |-  ( ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
208 206 207 sylibr 
 |-  ( ph -> ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
209 208 12 eleqtrrdi 
 |-  ( ph -> ( X E Y ) e. T )
210 infxrlb 
 |-  ( ( T C_ RR* /\ ( X E Y ) e. T ) -> inf ( T , RR* , < ) <_ ( X E Y ) )
211 79 209 210 syl2anc 
 |-  ( ph -> inf ( T , RR* , < ) <_ ( X E Y ) )
212 12 eleq2i 
 |-  ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
213 eliun 
 |-  ( p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
214 212 213 bitri 
 |-  ( p e. T <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) )
215 158 elrnmpt 
 |-  ( p e. _V -> ( p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. g e. S p = ( RR*s gsum ( E o. g ) ) ) )
216 215 elv 
 |-  ( p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) <-> E. g e. S p = ( RR*s gsum ( E o. g ) ) )
217 176 11 elrab2 
 |-  ( 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 ) ) ) ) ) ) )
218 217 simprbi 
 |-  ( 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 ) ) ) ) ) )
219 218 adantl 
 |-  ( ( ( 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 ) ) ) ) ) )
220 219 simp2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) )
221 3 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-onto-> B )
222 f1of1 
 |-  ( F : V -1-1-onto-> B -> F : V -1-1-> B )
223 221 222 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-> B )
224 simplr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
225 elfz1end 
 |-  ( n e. NN <-> n e. ( 1 ... n ) )
226 224 225 sylib 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( 1 ... n ) )
227 49 226 ffvelcdmd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
228 xp2nd 
 |-  ( ( g ` n ) e. ( V X. V ) -> ( 2nd ` ( g ` n ) ) e. V )
229 227 228 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) e. V )
230 9 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> Y e. V )
231 f1fveq 
 |-  ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` n ) ) e. V /\ Y e. V ) ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
232 223 229 230 231 syl12anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
233 220 232 mpbid 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) = Y )
234 233 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
235 eleq1 
 |-  ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
236 2fveq3 
 |-  ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
237 236 oveq2d 
 |-  ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
238 oveq2 
 |-  ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
239 238 182 eqtrdi 
 |-  ( m = 1 -> ( 1 ... m ) = { 1 } )
240 239 reseq2d 
 |-  ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
241 240 oveq2d 
 |-  ( m = 1 -> ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsum ( ( E o. g ) |` { 1 } ) ) )
242 237 241 breq12d 
 |-  ( m = 1 -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsum ( ( E o. g ) |` { 1 } ) ) ) )
243 235 242 imbi12d 
 |-  ( m = 1 -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsum ( ( E o. g ) |` { 1 } ) ) ) ) )
244 243 imbi2d 
 |-  ( m = 1 -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsum ( ( E o. g ) |` { 1 } ) ) ) ) ) )
245 eleq1 
 |-  ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
246 2fveq3 
 |-  ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
247 246 oveq2d 
 |-  ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
248 oveq2 
 |-  ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
249 248 reseq2d 
 |-  ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
250 249 oveq2d 
 |-  ( m = x -> ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) )
251 247 250 breq12d 
 |-  ( m = x -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) )
252 245 251 imbi12d 
 |-  ( m = x -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
253 252 imbi2d 
 |-  ( m = x -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) ) )
254 eleq1 
 |-  ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
255 2fveq3 
 |-  ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
256 255 oveq2d 
 |-  ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
257 oveq2 
 |-  ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
258 257 reseq2d 
 |-  ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
259 258 oveq2d 
 |-  ( m = ( x + 1 ) -> ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
260 256 259 breq12d 
 |-  ( m = ( x + 1 ) -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) )
261 254 260 imbi12d 
 |-  ( m = ( x + 1 ) -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
262 261 imbi2d 
 |-  ( m = ( x + 1 ) -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) ) )
263 eleq1 
 |-  ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
264 2fveq3 
 |-  ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
265 264 oveq2d 
 |-  ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
266 oveq2 
 |-  ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
267 266 reseq2d 
 |-  ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
268 267 oveq2d 
 |-  ( m = n -> ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) )
269 265 268 breq12d 
 |-  ( m = n -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) ) )
270 263 269 imbi12d 
 |-  ( m = n -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) )
271 270 imbi2d 
 |-  ( m = n -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) ) )
272 7 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E e. ( *Met ` V ) )
273 8 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> X e. V )
274 nnuz 
 |-  NN = ( ZZ>= ` 1 )
275 224 274 eleqtrdi 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
276 eluzfz1 
 |-  ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
277 275 276 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. ( 1 ... n ) )
278 49 277 ffvelcdmd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
279 xp2nd 
 |-  ( ( g ` 1 ) e. ( V X. V ) -> ( 2nd ` ( g ` 1 ) ) e. V )
280 278 279 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` 1 ) ) e. V )
281 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` 1 ) ) e. V ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
282 272 273 280 281 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
283 282 xrleidd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
284 137 ad2antrr 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. Mnd )
285 84 a1i 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. NN )
286 44 278 ffvelcdmd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
287 2fveq3 
 |-  ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
288 64 287 gsumsn 
 |-  ( ( W e. Mnd /\ 1 e. NN /\ ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) ) -> ( W gsum ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
289 284 285 286 288 syl3anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsum ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
290 272 30 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> RR* )
291 fcompt 
 |-  ( ( E : ( V X. V ) --> RR* /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
292 290 49 291 syl2anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
293 292 reseq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
294 277 snssd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
295 294 resmptd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
296 293 295 eqtrd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
297 296 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsum ( ( E o. g ) |` { 1 } ) ) = ( W gsum ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) )
298 df-ov 
 |-  ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
299 1st2nd2 
 |-  ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
300 278 299 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
301 219 simp1d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
302 xp1st 
 |-  ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
303 278 302 syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
304 f1fveq 
 |-  ( ( F : V -1-1-> B /\ ( ( 1st ` ( g ` 1 ) ) e. V /\ X e. V ) ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
305 223 303 273 304 syl12anc 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
306 301 305 mpbid 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
307 306 opeq1d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
308 300 307 eqtr2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
309 308 fveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
310 298 309 eqtrid 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
311 289 297 310 3eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsum ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
312 283 311 breqtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsum ( ( E o. g ) |` { 1 } ) ) )
313 312 a1d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsum ( ( E o. g ) |` { 1 } ) ) ) )
314 simprl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
315 314 274 eleqtrdi 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
316 simprr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
317 peano2fzr 
 |-  ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
318 315 316 317 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
319 318 expr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
320 319 imim1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
321 272 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( *Met ` V ) )
322 273 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
323 49 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
324 323 318 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
325 xp2nd 
 |-  ( ( g ` x ) e. ( V X. V ) -> ( 2nd ` ( g ` x ) ) e. V )
326 324 325 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) e. V )
327 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` x ) ) e. V ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
328 321 322 326 327 syl3anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
329 66 a1i 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> W e. CMnd )
330 fzfid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
331 51 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
332 fzsuc 
 |-  ( x e. ( ZZ>= ` 1 ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
333 315 332 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
334 elfzuz3 
 |-  ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
335 334 ad2antll 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
336 fzss2 
 |-  ( n e. ( ZZ>= ` ( x + 1 ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
337 335 336 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
338 333 337 eqsstrrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) u. { ( x + 1 ) } ) C_ ( 1 ... n ) )
339 338 unssad 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
340 331 339 fssresd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) : ( 1 ... x ) --> ( RR* \ { -oo } ) )
341 68 a1i 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> 0 e. _V )
342 340 330 341 fdmfifsupp 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) finSupp 0 )
343 64 65 329 330 340 342 gsumcl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) e. ( RR* \ { -oo } ) )
344 343 eldifad 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* )
345 321 30 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> RR* )
346 323 316 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) e. ( V X. V ) )
347 345 346 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
348 xleadd1a 
 |-  ( ( ( ( X E ( 2nd ` ( g ` x ) ) ) e. RR* /\ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* /\ ( E ` ( g ` ( x + 1 ) ) ) e. RR* ) /\ ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
349 348 ex 
 |-  ( ( ( X E ( 2nd ` ( g ` x ) ) ) e. RR* /\ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* /\ ( E ` ( g ` ( x + 1 ) ) ) e. RR* ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
350 328 344 347 349 syl3anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
351 xp2nd 
 |-  ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
352 346 351 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
353 xmettri 
 |-  ( ( 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 ) ) ) ) ) )
354 321 322 352 326 353 syl13anc 
 |-  ( ( ( ( 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 ) ) ) ) ) )
355 1st2nd2 
 |-  ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
356 346 355 syl 
 |-  ( ( ( ( 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 ) ) ) >. )
357 2fveq3 
 |-  ( i = x -> ( 2nd ` ( g ` i ) ) = ( 2nd ` ( g ` x ) ) )
358 357 fveq2d 
 |-  ( i = x -> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 2nd ` ( g ` x ) ) ) )
359 fvoveq1 
 |-  ( i = x -> ( g ` ( i + 1 ) ) = ( g ` ( x + 1 ) ) )
360 359 fveq2d 
 |-  ( i = x -> ( 1st ` ( g ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) )
361 360 fveq2d 
 |-  ( i = x -> ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) )
362 358 361 eqeq12d 
 |-  ( i = x -> ( ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) ) )
363 219 simp3d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
364 363 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
365 nnz 
 |-  ( x e. NN -> x e. ZZ )
366 365 ad2antrl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
367 eluzp1m1 
 |-  ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
368 366 335 367 syl2anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
369 elfzuzb 
 |-  ( x e. ( 1 ... ( n - 1 ) ) <-> ( x e. ( ZZ>= ` 1 ) /\ ( n - 1 ) e. ( ZZ>= ` x ) ) )
370 315 368 369 sylanbrc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... ( n - 1 ) ) )
371 362 364 370 rspcdva 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) )
372 223 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> F : V -1-1-> B )
373 xp1st 
 |-  ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 1st ` ( g ` ( x + 1 ) ) ) e. V )
374 346 373 syl 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1st ` ( g ` ( x + 1 ) ) ) e. V )
375 f1fveq 
 |-  ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` x ) ) e. V /\ ( 1st ` ( g ` ( x + 1 ) ) ) e. V ) ) -> ( ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) <-> ( 2nd ` ( g ` x ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) ) )
376 372 326 374 375 syl12anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) <-> ( 2nd ` ( g ` x ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) ) )
377 371 376 mpbid 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) )
378 377 opeq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> <. ( 2nd ` ( g ` x ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
379 356 378 eqtr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) = <. ( 2nd ` ( g ` x ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
380 379 fveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) = ( E ` <. ( 2nd ` ( g ` x ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. ) )
381 df-ov 
 |-  ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) = ( E ` <. ( 2nd ` ( g ` x ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
382 380 381 eqtr4di 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) = ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
383 382 oveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) = ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) ) )
384 354 383 breqtrrd 
 |-  ( ( ( ( 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 ( E ` ( g ` ( x + 1 ) ) ) ) )
385 xmetcl 
 |-  ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` ( x + 1 ) ) ) e. V ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* )
386 321 322 352 385 syl3anc 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* )
387 328 347 xaddcld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* )
388 344 347 xaddcld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* )
389 xrletr 
 |-  ( ( ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* /\ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* /\ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* ) -> ( ( ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) /\ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
390 386 387 388 389 syl3anc 
 |-  ( ( ( ( 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 ( E ` ( g ` ( x + 1 ) ) ) ) /\ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
391 384 390 mpand 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
392 350 391 syld 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
393 xrex 
 |-  RR* e. _V
394 393 difexi 
 |-  ( RR* \ { -oo } ) e. _V
395 10 24 ressplusg 
 |-  ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` W ) )
396 394 395 ax-mp 
 |-  +e = ( +g ` W )
397 44 ad2antrr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... x ) ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
398 fzelp1 
 |-  ( j e. ( 1 ... x ) -> j e. ( 1 ... ( x + 1 ) ) )
399 49 ad2antrr 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... ( x + 1 ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
400 337 sselda 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... ( x + 1 ) ) ) -> j e. ( 1 ... n ) )
401 399 400 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... ( x + 1 ) ) ) -> ( g ` j ) e. ( V X. V ) )
402 398 401 sylan2 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... x ) ) -> ( g ` j ) e. ( V X. V ) )
403 397 402 ffvelcdmd 
 |-  ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... x ) ) -> ( E ` ( g ` j ) ) e. ( RR* \ { -oo } ) )
404 fzp1disj 
 |-  ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/)
405 404 a1i 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/) )
406 disjsn 
 |-  ( ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/) <-> -. ( x + 1 ) e. ( 1 ... x ) )
407 405 406 sylib 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> -. ( x + 1 ) e. ( 1 ... x ) )
408 44 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
409 408 346 ffvelcdmd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. ( RR* \ { -oo } ) )
410 2fveq3 
 |-  ( j = ( x + 1 ) -> ( E ` ( g ` j ) ) = ( E ` ( g ` ( x + 1 ) ) ) )
411 64 396 329 330 403 316 407 409 410 gsumunsn 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) ) = ( ( W gsum ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
412 292 adantr 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
413 412 333 reseq12d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` ( ( 1 ... x ) u. { ( x + 1 ) } ) ) )
414 338 resmptd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` ( ( 1 ... x ) u. { ( x + 1 ) } ) ) = ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) )
415 413 414 eqtrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) = ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) )
416 415 oveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) = ( W gsum ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) ) )
417 412 reseq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` ( 1 ... x ) ) )
418 339 resmptd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` ( 1 ... x ) ) = ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) )
419 417 418 eqtrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) = ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) )
420 419 oveq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) = ( W gsum ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) )
421 420 oveq1d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) = ( ( W gsum ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
422 411 416 421 3eqtr4d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) = ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
423 422 breq2d 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) <-> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
424 392 423 sylibrd 
 |-  ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) )
425 320 424 animpimp2impd 
 |-  ( x e. NN -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) -> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) ) )
426 244 253 262 271 313 425 nnind 
 |-  ( n e. NN -> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) )
427 224 426 mpcom 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) ) )
428 226 427 mpd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) )
429 234 428 eqbrtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E Y ) <_ ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) )
430 ffn 
 |-  ( ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) -> ( E o. g ) Fn ( 1 ... n ) )
431 fnresdm 
 |-  ( ( E o. g ) Fn ( 1 ... n ) -> ( ( E o. g ) |` ( 1 ... n ) ) = ( E o. g ) )
432 51 430 431 3syl 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` ( 1 ... n ) ) = ( E o. g ) )
433 432 oveq2d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) = ( W gsum ( E o. g ) ) )
434 62 433 eqtr4d 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsum ( E o. g ) ) = ( W gsum ( ( E o. g ) |` ( 1 ... n ) ) ) )
435 429 434 breqtrrd 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E Y ) <_ ( RR*s gsum ( E o. g ) ) )
436 breq2 
 |-  ( p = ( RR*s gsum ( E o. g ) ) -> ( ( X E Y ) <_ p <-> ( X E Y ) <_ ( RR*s gsum ( E o. g ) ) ) )
437 435 436 syl5ibrcom 
 |-  ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( p = ( RR*s gsum ( E o. g ) ) -> ( X E Y ) <_ p ) )
438 437 rexlimdva 
 |-  ( ( ph /\ n e. NN ) -> ( E. g e. S p = ( RR*s gsum ( E o. g ) ) -> ( X E Y ) <_ p ) )
439 216 438 biimtrid 
 |-  ( ( ph /\ n e. NN ) -> ( p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) -> ( X E Y ) <_ p ) )
440 439 rexlimdva 
 |-  ( ph -> ( E. n e. NN p e. ran ( g e. S |-> ( RR*s gsum ( E o. g ) ) ) -> ( X E Y ) <_ p ) )
441 214 440 biimtrid 
 |-  ( ph -> ( p e. T -> ( X E Y ) <_ p ) )
442 441 ralrimiv 
 |-  ( ph -> A. p e. T ( X E Y ) <_ p )
443 infxrgelb 
 |-  ( ( T C_ RR* /\ ( X E Y ) e. RR* ) -> ( ( X E Y ) <_ inf ( T , RR* , < ) <-> A. p e. T ( X E Y ) <_ p ) )
444 79 83 443 syl2anc 
 |-  ( ph -> ( ( X E Y ) <_ inf ( T , RR* , < ) <-> A. p e. T ( X E Y ) <_ p ) )
445 442 444 mpbird 
 |-  ( ph -> ( X E Y ) <_ inf ( T , RR* , < ) )
446 81 83 211 445 xrletrid 
 |-  ( ph -> inf ( T , RR* , < ) = ( X E Y ) )
447 22 446 eqtrd 
 |-  ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )