Theorem imasdsf1olem 22178

Description: Lemma for imasdsf1o 22179. (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*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 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.

Step	Hyp	Ref	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 6144	. . . . 5 |- ( F : V -1-1-onto-> B -> F : V -onto-> B )
5	3, 4	syl 17	. . . 4 |- ( ph -> F : V -onto-> B )
6		imasdsf1o.r	. . . 4 |- ( ph -> R e. Z )
7		eqid 2622	. . . 4 |- ( dist ` R ) = ( dist ` R )
8		imasdsf1o.d	. . . 4 |- D = ( dist ` U )
9		f1of 6137	. . . . . 6 |- ( F : V -1-1-onto-> B -> F : V --> B )
10	3, 9	syl 17	. . . . 5 |- ( ph -> F : V --> B )
11		imasdsf1o.x	. . . . 5 |- ( ph -> X e. V )
12	10, 11	ffvelrnd 6360	. . . 4 |- ( ph -> ( F ` X ) e. B )
13		imasdsf1o.y	. . . . 5 |- ( ph -> Y e. V )
14	10, 13	ffvelrnd 6360	. . . 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 ) )
17	1, 2, 5, 6, 7, 8, 12, 14, 15, 16	imasdsval2 16176	. . 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 ) ) )
19	18	infeq1i 8384	. . 3 |- inf ( T , RR* , < ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , < )
20	17, 19	syl6eqr 2674	. 2 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = inf ( T , RR* , < ) )
21		xrsbas 19762	. . . . . . . . . . . 12 |- RR* = ( Base ` RR*s )
22		xrsadd 19763	. . . . . . . . . . . 12 |- +e = ( +g ` RR*s )
23		imasdsf1o.w	. . . . . . . . . . . 12 |- W = ( RR*s ↾s ( RR* \ { -oo } ) )
24		xrsex 19761	. . . . . . . . . . . . 13 |- RR*s e. _V
25	24	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR*s e. _V )
26		fzfid 12772	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
27		difss 3737	. . . . . . . . . . . . 13 |- ( RR* \ { -oo } ) C_ RR*
28	27	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR* \ { -oo } ) C_ RR* )
29		imasdsf1o.m	. . . . . . . . . . . . . . . 16 |- ( ph -> E e. ( *Met ` V ) )
30		xmetf 22134	. . . . . . . . . . . . . . . 16 |- ( E e. ( *Met ` V ) -> E : ( V X. V ) --> RR* )
31		ffn 6045	. . . . . . . . . . . . . . . 16 |- ( E : ( V X. V ) --> RR* -> E Fn ( V X. V ) )
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 |- ( ph -> E Fn ( V X. V ) )
33		xmetcl 22136	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34		xmetge0 22149	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35		ge0nemnf 12004	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f E g ) e. RR* /\ 0 <_ ( f E g ) ) -> ( f E g ) =/= -oo )
36	33, 34, 35	syl2anc 693	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) =/= -oo )
37		eldifsn 4317	. . . . . . . . . . . . . . . . . . 19 |- ( ( f E g ) e. ( RR* \ { -oo } ) <-> ( ( f E g ) e. RR* /\ ( f E g ) =/= -oo ) )
38	33, 36, 37	sylanbrc 698	. . . . . . . . . . . . . . . . . 18 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. ( RR* \ { -oo } ) )
39	38	3expb 1266	. . . . . . . . . . . . . . . . 17 |- ( ( E e. ( *Met ` V ) /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
40	29, 39	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
41	40	ralrimivva 2971	. . . . . . . . . . . . . . 15 |- ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42		ffnov 6764	. . . . . . . . . . . . . . 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 } ) ) )
43	32, 41, 42	sylanbrc 698	. . . . . . . . . . . . . 14 |- ( ph -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
44	43	ad2antrr 762	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
45		ssrab2 3687	. . . . . . . . . . . . . . . . 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 ) )
46	15, 45	eqsstri 3635	. . . . . . . . . . . . . . . 16 |- S C_ ( ( V X. V ) ^m ( 1 ... n ) )
47	46	a1i 11	. . . . . . . . . . . . . . 15 |- ( ( ph /\ n e. NN ) -> S C_ ( ( V X. V ) ^m ( 1 ... n ) ) )
48	47	sselda 3603	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
49		elmapi 7879	. . . . . . . . . . . . . 14 |- ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
50	48, 49	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g : ( 1 ... n ) --> ( V X. V ) )
51		fco 6058	. . . . . . . . . . . . 13 |- ( ( E : ( V X. V ) --> ( RR* \ { -oo } ) /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
52	44, 50, 51	syl2anc 693	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
53		0re 10040	. . . . . . . . . . . . 13 |- 0 e. RR
54		rexr 10085	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 e. RR* )
55		renemnf 10088	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 =/= -oo )
56		eldifsn 4317	. . . . . . . . . . . . . 14 |- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
57	54, 55, 56	sylanbrc 698	. . . . . . . . . . . . 13 |- ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
58	53, 57	mp1i 13	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. ( RR* \ { -oo } ) )
59		xaddid2 12073	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( 0 +e x ) = x )
60		xaddid1 12072	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( x +e 0 ) = x )
61	59, 60	jca 554	. . . . . . . . . . . . 13 |- ( x e. RR* -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
62	61	adantl 482	. . . . . . . . . . . 12 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
63	21, 22, 23, 25, 26, 28, 52, 58, 62	gsumress 17276	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) = ( W gsumg ( E o. g ) ) )
64	23, 21	ressbas2 15931	. . . . . . . . . . . . 13 |- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
65	27, 64	ax-mp 5	. . . . . . . . . . . 12 |- ( RR* \ { -oo } ) = ( Base ` W )
66	23	xrs10 19785	. . . . . . . . . . . 12 |- 0 = ( 0g ` W )
67	23	xrs1cmn 19786	. . . . . . . . . . . . 13 |- W e. CMnd
68	67	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
69		c0ex 10034	. . . . . . . . . . . . . 14 |- 0 e. _V
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. _V )
71	52, 26, 70	fdmfifsupp 8285	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) finSupp 0 )
72	65, 66, 68, 26, 52, 71	gsumcl 18316	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
73	63, 72	eqeltrd 2701	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
74	73	eldifad 3586	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. RR* )
75		eqid 2622	. . . . . . . . 9 |- ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
76	74, 75	fmptd 6385	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* )
77		frn 6053	. . . . . . . 8 |- ( ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* -> ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
78	76, 77	syl 17	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
79	78	ralrimiva 2966	. . . . . 6 |- ( ph -> A. n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
80		iunss 4561	. . . . . 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* )
81	79, 80	sylibr 224	. . . . 5 |- ( ph -> U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
82	18, 81	syl5eqss 3649	. . . 4 |- ( ph -> T C_ RR* )
83		infxrcl 12163	. . . 4 |- ( T C_ RR* -> inf ( T , RR* , < ) e. RR* )
84	82, 83	syl 17	. . 3 |- ( ph -> inf ( T , RR* , < ) e. RR* )
85		xmetcl 22136	. . . 4 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
86	29, 11, 13, 85	syl3anc 1326	. . 3 |- ( ph -> ( X E Y ) e. RR* )
87		1nn 11031	. . . . . . 7 |- 1 e. NN
88		1ex 10035	. . . . . . . . . . . 12 |- 1 e. _V
89		opex 4932	. . . . . . . . . . . 12 |- <. X , Y >. e. _V
90	88, 89	f1osn 6176	. . . . . . . . . . 11 |- { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
91		f1of 6137	. . . . . . . . . . 11 |- ( { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. } -> { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } )
92	90, 91	ax-mp 5	. . . . . . . . . 10 |- { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. }
93		opelxpi 5148	. . . . . . . . . . . 12 |- ( ( X e. V /\ Y e. V ) -> <. X , Y >. e. ( V X. V ) )
94	11, 13, 93	syl2anc 693	. . . . . . . . . . 11 |- ( ph -> <. X , Y >. e. ( V X. V ) )
95	94	snssd 4340	. . . . . . . . . 10 |- ( ph -> { <. X , Y >. } C_ ( V X. V ) )
96		fss 6056	. . . . . . . . . 10 |- ( ( { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } /\ { <. X , Y >. } C_ ( V X. V ) ) -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
97	92, 95, 96	sylancr 695	. . . . . . . . 9 |- ( ph -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
98	29	elfvexd 6222	. . . . . . . . . . 11 |- ( ph -> V e. _V )
99		xpexg 6960	. . . . . . . . . . 11 |- ( ( V e. _V /\ V e. _V ) -> ( V X. V ) e. _V )
100	98, 98, 99	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( V X. V ) e. _V )
101		snex 4908	. . . . . . . . . 10 |- { 1 } e. _V
102		elmapg 7870	. . . . . . . . . 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 ) ) )
103	100, 101, 102	sylancl 694	. . . . . . . . 9 |- ( ph -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
104	97, 103	mpbird 247	. . . . . . . 8 |- ( ph -> { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) )
105		op1stg 7180	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 1st ` <. X , Y >. ) = X )
106	11, 13, 105	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( 1st ` <. X , Y >. ) = X )
107	106	fveq2d 6195	. . . . . . . . 9 |- ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
108		op2ndg 7181	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 2nd ` <. X , Y >. ) = Y )
109	11, 13, 108	syl2anc 693	. . . . . . . . . 10 |- ( ph -> ( 2nd ` <. X , Y >. ) = Y )
110	109	fveq2d 6195	. . . . . . . . 9 |- ( ph -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
111	107, 110	jca 554	. . . . . . . 8 |- ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
112	24	a1i 11	. . . . . . . . . 10 |- ( ph -> RR*s e. _V )
113		snfi 8038	. . . . . . . . . . 11 |- { 1 } e. Fin
114	113	a1i 11	. . . . . . . . . 10 |- ( ph -> { 1 } e. Fin )
115	27	a1i 11	. . . . . . . . . 10 |- ( ph -> ( RR* \ { -oo } ) C_ RR* )
116		xmetge0 22149	. . . . . . . . . . . . . . 15 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
117	29, 11, 13, 116	syl3anc 1326	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( X E Y ) )
118		ge0nemnf 12004	. . . . . . . . . . . . . 14 |- ( ( ( X E Y ) e. RR* /\ 0 <_ ( X E Y ) ) -> ( X E Y ) =/= -oo )
119	86, 117, 118	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) =/= -oo )
120		eldifsn 4317	. . . . . . . . . . . . 13 |- ( ( X E Y ) e. ( RR* \ { -oo } ) <-> ( ( X E Y ) e. RR* /\ ( X E Y ) =/= -oo ) )
121	86, 119, 120	sylanbrc 698	. . . . . . . . . . . 12 |- ( ph -> ( X E Y ) e. ( RR* \ { -oo } ) )
122		fconst6g 6094	. . . . . . . . . . . 12 |- ( ( X E Y ) e. ( RR* \ { -oo } ) -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
123	121, 122	syl 17	. . . . . . . . . . 11 |- ( ph -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
124		fcoconst 6401	. . . . . . . . . . . . . 14 |- ( ( E Fn ( V X. V ) /\ <. X , Y >. e. ( V X. V ) ) -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
125	32, 94, 124	syl2anc 693	. . . . . . . . . . . . 13 |- ( ph -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
126	88, 89	xpsn 6407	. . . . . . . . . . . . . 14 |- ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
127	126	coeq2i 5282	. . . . . . . . . . . . 13 |- ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
128		df-ov 6653	. . . . . . . . . . . . . . . 16 |- ( X E Y ) = ( E ` <. X , Y >. )
129	128	eqcomi 2631	. . . . . . . . . . . . . . 15 |- ( E ` <. X , Y >. ) = ( X E Y )
130	129	sneqi 4188	. . . . . . . . . . . . . 14 |- { ( E ` <. X , Y >. ) } = { ( X E Y ) }
131	130	xpeq2i 5136	. . . . . . . . . . . . 13 |- ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
132	125, 127, 131	3eqtr3g 2679	. . . . . . . . . . . 12 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
133	132	feq1d 6030	. . . . . . . . . . 11 |- ( ph -> ( ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) <-> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) ) )
134	123, 133	mpbird 247	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) )
135	53, 57	mp1i 13	. . . . . . . . . 10 |- ( ph -> 0 e. ( RR* \ { -oo } ) )
136	61	adantl 482	. . . . . . . . . 10 |- ( ( ph /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
137	21, 22, 23, 112, 114, 115, 134, 135, 136	gsumress 17276	. . . . . . . . 9 |- ( ph -> ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
138		fconstmpt 5163	. . . . . . . . . . 11 |- ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
139	132, 138	syl6eq 2672	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
140	139	oveq2d 6666	. . . . . . . . 9 |- ( ph -> ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
141		cmnmnd 18208	. . . . . . . . . . 11 |- ( W e. CMnd -> W e. Mnd )
142	67, 141	mp1i 13	. . . . . . . . . 10 |- ( ph -> W e. Mnd )
143	87	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN )
144		eqidd 2623	. . . . . . . . . . 11 |- ( j = 1 -> ( X E Y ) = ( X E Y ) )
145	65, 144	gsumsn 18354	. . . . . . . . . 10 |- ( ( W e. Mnd /\ 1 e. NN /\ ( X E Y ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
146	142, 143, 121, 145	syl3anc 1326	. . . . . . . . 9 |- ( ph -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
147	137, 140, 146	3eqtrrd 2661	. . . . . . . 8 |- ( ph -> ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
148		fveq1 6190	. . . . . . . . . . . . . . 15 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
149	88, 89	fvsn 6446	. . . . . . . . . . . . . . 15 |- ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
150	148, 149	syl6eq 2672	. . . . . . . . . . . . . 14 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
151	150	fveq2d 6195	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
152	151	fveq2d 6195	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
153	152	eqeq1d 2624	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
154	150	fveq2d 6195	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
155	154	fveq2d 6195	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
156	155	eqeq1d 2624	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
157	153, 156	anbi12d 747	. . . . . . . . . 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 5280	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
159	158	oveq2d 6666	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( RR*s gsumg ( E o. g ) ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
160	159	eqeq2d 2632	. . . . . . . . . 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 >. >. } ) ) ) )
161	157, 160	anbi12d 747	. . . . . . . . 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 >. >. } ) ) ) ) )
162	161	rspcev 3309	. . . . . . . 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 ) ) ) )
163	104, 111, 147, 162	syl12anc 1324	. . . . . . 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 6678	. . . . . . . . . 10 |- ( X E Y ) e. _V
165	75	elrnmpt 5372	. . . . . . . . . 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 ) ) ) )
166	164, 165	ax-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 ) ) )
167	15	rexeqi 3143	. . . . . . . . . . 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 6190	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
169	168	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
170	169	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( g ` 1 ) ) ) )
171	170	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
172		fveq1 6190	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` n ) = ( g ` n ) )
173	172	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
174	173	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( g ` n ) ) ) )
175	174	eqeq1d 2624	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
176		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` i ) = ( g ` i ) )
177	176	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
178	177	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
179		fveq1 6190	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
180	179	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
181	180	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
182	178, 181	eqeq12d 2637	. . . . . . . . . . . . . 14 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
183	182	ralbidv 2986	. . . . . . . . . . . . 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 ) ) ) ) ) )
184	171, 175, 183	3anbi123d 1399	. . . . . . . . . . . 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 ) ) ) ) ) ) )
185	184	rexrab 3370	. . . . . . . . . . 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 ) ) ) )
186	167, 185	bitri 264	. . . . . . . . . 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 6658	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
188		1z 11407	. . . . . . . . . . . . . 14 |- 1 e. ZZ
189		fzsn 12383	. . . . . . . . . . . . . 14 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
190	188, 189	ax-mp 5	. . . . . . . . . . . . 13 |- ( 1 ... 1 ) = { 1 }
191	187, 190	syl6eq 2672	. . . . . . . . . . . 12 |- ( n = 1 -> ( 1 ... n ) = { 1 } )
192	191	oveq2d 6666	. . . . . . . . . . 11 |- ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
193		df-3an 1039	. . . . . . . . . . . . 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 4076	. . . . . . . . . . . . . . . 16 |- A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
195		oveq1 6657	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
196		1m1e0 11089	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 - 1 ) = 0
197	195, 196	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = 0 )
198	197	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
199		fz10 12362	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... 0 ) = (/)
200	198, 199	syl6eq 2672	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
201	200	raleqdv 3144	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
202	194, 201	mpbiri 248	. . . . . . . . . . . . . . 15 |- ( n = 1 -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
203	202	biantrud 528	. . . . . . . . . . . . . 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 6191	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( g ` n ) = ( g ` 1 ) )
205	204	fveq2d 6195	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
206	205	fveq2d 6195	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` ( 2nd ` ( g ` 1 ) ) ) )
207	206	eqeq1d 2624	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) )
208	207	anbi2d 740	. . . . . . . . . . . . . 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 ) ) ) )
209	203, 208	bitr3d 270	. . . . . . . . . . . . 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 ) ) ) )
210	193, 209	syl5bb 272	. . . . . . . . . . . 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 ) ) ) )
211	210	anbi1d 741	. . . . . . . . . . 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 ) ) ) ) )
212	192, 211	rexeqbidv 3153	. . . . . . . . . 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 ) ) ) ) )
213	186, 212	syl5bb 272	. . . . . . . . 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 ) ) ) ) )
214	166, 213	syl5bb 272	. . . . . . . 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 ) ) ) ) )
215	214	rspcev 3309	. . . . . . 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 ) ) ) )
216	87, 163, 215	sylancr 695	. . . . . 6 |- ( ph -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
217		eliun 4524	. . . . . 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 ) ) ) )
218	216, 217	sylibr 224	. . . . 5 |- ( ph -> ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
219	218, 18	syl6eleqr 2712	. . . 4 |- ( ph -> ( X E Y ) e. T )
220		infxrlb 12164	. . . 4 |- ( ( T C_ RR* /\ ( X E Y ) e. T ) -> inf ( T , RR* , < ) <_ ( X E Y ) )
221	82, 219, 220	syl2anc 693	. . 3 |- ( ph -> inf ( T , RR* , < ) <_ ( X E Y ) )
222	18	eleq2i 2693	. . . . . . 7 |- ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
223		eliun 4524	. . . . . . 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 ) ) ) )
224	222, 223	bitri 264	. . . . . 6 |- ( p e. T <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
225		vex 3203	. . . . . . . . 9 |- p e. _V
226	75	elrnmpt 5372	. . . . . . . . 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 ) ) ) )
227	225, 226	ax-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 ) ) )
228	184, 15	elrab2 3366	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
229	228	simprbi 480	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
230	229	adantl 482	. . . . . . . . . . . . . . 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 ) ) ) ) ) )
231	230	simp2d 1074	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) )
232	3	ad2antrr 762	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-onto-> B )
233		f1of1 6136	. . . . . . . . . . . . . . . 16 |- ( F : V -1-1-onto-> B -> F : V -1-1-> B )
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-> B )
235		simplr 792	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
236		elfz1end 12371	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN <-> n e. ( 1 ... n ) )
237	235, 236	sylib 208	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( 1 ... n ) )
238	50, 237	ffvelrnd 6360	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
239		xp2nd 7199	. . . . . . . . . . . . . . . 16 |- ( ( g ` n ) e. ( V X. V ) -> ( 2nd ` ( g ` n ) ) e. V )
240	238, 239	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) e. V )
241	13	ad2antrr 762	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> Y e. V )
242		f1fveq 6519	. . . . . . . . . . . . . . 15 |- ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` n ) ) e. V /\ Y e. V ) ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
243	234, 240, 241, 242	syl12anc 1324	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
244	231, 243	mpbid 222	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) = Y )
245	244	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
246		eleq1 2689	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
247		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( g ` m ) = ( g ` 1 ) )
248	247	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
249	248	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
250		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
251	250, 190	syl6eq 2672	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
252	251	reseq2d 5396	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
253	252	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
254	249, 253	breq12d 4666	. . . . . . . . . . . . . . . . 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 } ) ) ) )
255	246, 254	imbi12d 334	. . . . . . . . . . . . . . . 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 } ) ) ) ) )
256	255	imbi2d 330	. . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
258		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( g ` m ) = ( g ` x ) )
259	258	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
260	259	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
261		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
262	261	reseq2d 5396	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
263	262	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) )
264	260, 263	breq12d 4666	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
265	257, 264	imbi12d 334	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
266	265	imbi2d 330	. . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
268		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( g ` m ) = ( g ` ( x + 1 ) ) )
269	268	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
270	269	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
271		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
272	271	reseq2d 5396	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
273	272	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
274	270, 273	breq12d 4666	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
275	267, 274	imbi12d 334	. . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
276	275	imbi2d 330	. . . . . . . . . . . . . . 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 2689	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
278		fveq2 6191	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( g ` m ) = ( g ` n ) )
279	278	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
280	279	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
281		oveq2 6658	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
282	281	reseq2d 5396	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
283	282	oveq2d 6666	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
284	280, 283	breq12d 4666	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
285	277, 284	imbi12d 334	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
286	285	imbi2d 330	. . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
287	29	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E e. ( *Met ` V ) )
288	11	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> X e. V )
289		nnuz 11723	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN = ( ZZ>= ` 1 )
290	235, 289	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
291		eluzfz1 12348	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
292	290, 291	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. ( 1 ... n ) )
293	50, 292	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
294		xp2nd 7199	. . . . . . . . . . . . . . . . . . . 20 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 2nd ` ( g ` 1 ) ) e. V )
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` 1 ) ) e. V )
296		xmetcl 22136	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` 1 ) ) e. V ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
297	287, 288, 295, 296	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
298		xrleid 11983	. . . . . . . . . . . . . . . . . 18 |- ( ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
299	297, 298	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
300	142	ad2antrr 762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. Mnd )
301	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. NN )
302	44, 293	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
303		fveq2 6191	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = 1 -> ( g ` j ) = ( g ` 1 ) )
304	303	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20 |- ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
305	65, 304	gsumsn 18354	. . . . . . . . . . . . . . . . . . 19 |- ( ( W e. Mnd /\ 1 e. NN /\ ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
306	300, 301, 302, 305	syl3anc 1326	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
307	287, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> RR* )
308		fcompt 6400	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( E : ( V X. V ) --> RR* /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
309	307, 50, 308	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
310	309	reseq1d 5395	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
311	292	snssd 4340	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
312	311	resmptd 5452	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
313	310, 312	eqtrd 2656	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
314	313	oveq2d 6666	. . . . . . . . . . . . . . . . . 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 6653	. . . . . . . . . . . . . . . . . . 19 |- ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
316		1st2nd2 7205	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
317	293, 316	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
318	230	simp1d 1073	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
319		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
320	293, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
321		f1fveq 6519	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : V -1-1-> B /\ ( ( 1st ` ( g ` 1 ) ) e. V /\ X e. V ) ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
322	234, 320, 288, 321	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
323	318, 322	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
324	323	opeq1d 4408	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
325	317, 324	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
326	325	fveq2d 6195	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
327	315, 326	syl5eq 2668	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
328	306, 314, 327	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
329	299, 328	breqtrrd 4681	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
330	329	a1d 25	. . . . . . . . . . . . . . 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 794	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
332	331, 289	syl6eleq 2711	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
333		simprr 796	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
334		peano2fzr 12354	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
335	332, 333, 334	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
336	335	expr 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
337	336	imim1d 82	. . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
338	287	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( *Met ` V ) )
339	288	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
340	50	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
341	340, 335	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
342		xp2nd 7199	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` x ) e. ( V X. V ) -> ( 2nd ` ( g ` x ) ) e. V )
343	341, 342	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) e. V )
344		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` x ) ) e. V ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
345	338, 339, 343, 344	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
346	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> W e. CMnd )
347		fzfid 12772	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
348	52	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 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 12388	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( ZZ>= ` 1 ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
350	332, 349	syl 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 12339	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
352	351	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
353		fzss2 12381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n e. ( ZZ>= ` ( x + 1 ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
354	352, 353	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
355	350, 354	eqsstr3d 3640	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) u. { ( x + 1 ) } ) C_ ( 1 ... n ) )
356	355	unssad 3790	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
357	348, 356	fssresd 6071	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
358	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> 0 e. _V )
359	357, 347, 358	fdmfifsupp 8285	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) finSupp 0 )
360	65, 66, 346, 347, 357, 359	gsumcl 18316	. . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
361	360	eldifad 3586	. . . . . . . . . . . . . . . . . . . . . . 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* )
362	338, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> RR* )
363	340, 333	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) e. ( V X. V ) )
364	362, 363	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
365		xleadd1a 12083	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
366	365	ex 450	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
367	345, 361, 364, 366	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . 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 7199	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
369	363, 368	syl 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 22156	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
371	338, 339, 369, 343, 370	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . 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 7205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
373	363, 372	syl 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 11399	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. NN -> x e. ZZ )
375	374	ad2antrl 764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
376		eluzp1m1 11711	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
377	375, 352, 376	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
378		elfzuzb 12336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. ( 1 ... ( n - 1 ) ) <-> ( x e. ( ZZ>= ` 1 ) /\ ( n - 1 ) e. ( ZZ>= ` x ) ) )
379	332, 377, 378	sylanbrc 698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... ( n - 1 ) ) )
380	230	simp3d 1075	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
381	380	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( 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 ) ) ) ) )
382		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( i = x -> ( g ` i ) = ( g ` x ) )
383	382	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( i = x -> ( 2nd ` ( g ` i ) ) = ( 2nd ` ( g ` x ) ) )
384	383	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( i = x -> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 2nd ` ( g ` x ) ) ) )
385		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( i = x -> ( i + 1 ) = ( x + 1 ) )
386	385	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( i = x -> ( g ` ( i + 1 ) ) = ( g ` ( x + 1 ) ) )
387	386	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( i = x -> ( 1st ` ( g ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) )
388	387	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( i = x -> ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) )
389	384, 388	eqeq12d 2637	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( i = x -> ( ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) ) )
390	389	rspcv 3305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. ( 1 ... ( n - 1 ) ) -> ( A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) -> ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) ) )
391	379, 381, 390	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( F ` ( 2nd ` ( g ` x ) ) ) = ( F ` ( 1st ` ( g ` ( x + 1 ) ) ) ) )
392	234	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> F : V -1-1-> B )
393		xp1st 7198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 1st ` ( g ` ( x + 1 ) ) ) e. V )
394	363, 393	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1st ` ( g ` ( x + 1 ) ) ) e. V )
395		f1fveq 6519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( 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 ) ) ) ) )
396	392, 343, 394, 395	syl12anc 1324	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( 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 ) ) ) ) )
397	391, 396	mpbid 222	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) = ( 1st ` ( g ` ( x + 1 ) ) ) )
398	397	opeq1d 4408	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( 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 ) ) ) >. )
399	373, 398	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( 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 ) ) ) >. )
400	399	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) ) >. ) )
401		df-ov 6653	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) = ( E ` <. ( 2nd ` ( g ` x ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
402	400, 401	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) ) ) )
403	402	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) ) ) )
404	371, 403	breqtrrd 4681	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 ) ) ) ) )
405		xmetcl 22136	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` ( x + 1 ) ) ) e. V ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* )
406	338, 339, 369, 405	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* )
407	345, 364	xaddcld 12131	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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* )
408	361, 364	xaddcld 12131	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* )
409		xrletr 11989	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) e. RR* /\ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) e. RR* /\ ( ( W gsumg ( ( 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 gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
410	406, 407, 408, 409	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( 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 gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
411	404, 410	mpand 711	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( 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 gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
412	367, 411	syld 47	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( 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 + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
413		xrex 11829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- RR* e. _V
414	413, 27	ssexi 4803	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( RR* \ { -oo } ) e. _V
415	23, 22	ressplusg 15993	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( RR* \ { -oo } ) e. _V -> +e = ( +g ` W ) )
416	414, 415	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 |- +e = ( +g ` W )
417	44	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( 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 } ) )
418		fzelp1 12393	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j e. ( 1 ... x ) -> j e. ( 1 ... ( x + 1 ) ) )
419	50	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( 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 ) )
420	354	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) /\ j e. ( 1 ... ( x + 1 ) ) ) -> j e. ( 1 ... n ) )
421	419, 420	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( 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 ) )
422	418, 421	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( 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 ) )
423	417, 422	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( 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 } ) )
424		fzp1disj 12399	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/)
425	424	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/) )
426		disjsn 4246	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( 1 ... x ) i^i { ( x + 1 ) } ) = (/) <-> -. ( x + 1 ) e. ( 1 ... x ) )
427	425, 426	sylib 208	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> -. ( x + 1 ) e. ( 1 ... x ) )
428	44	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
429	428, 363	ffvelrnd 6360	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. ( RR* \ { -oo } ) )
430		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = ( x + 1 ) -> ( g ` j ) = ( g ` ( x + 1 ) ) )
431	430	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = ( x + 1 ) -> ( E ` ( g ` j ) ) = ( E ` ( g ` ( x + 1 ) ) ) )
432	65, 416, 346, 347, 423, 333, 427, 429, 431	gsumunsn 18359	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) ) = ( ( W gsumg ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
433	309	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) ) )
434	433, 350	reseq12d 5397	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) } ) ) )
435	355	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) ) )
436	434, 435	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( 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 ) ) ) )
437	436	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) = ( W gsumg ( j e. ( ( 1 ... x ) u. { ( x + 1 ) } ) |-> ( E ` ( g ` j ) ) ) ) )
438	433	reseq1d 5395	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) )
439	356	resmptd 5452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( 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 ) ) ) )
440	438, 439	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( 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 ) ) ) )
441	440	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) = ( W gsumg ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) )
442	441	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) = ( ( W gsumg ( j e. ( 1 ... x ) |-> ( E ` ( g ` j ) ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
443	432, 437, 442	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) = ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
444	443	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) <-> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
445	412, 444	sylibrd 249	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( 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 + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) )
446	445	expr 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
447	446	a2d 29	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( 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 + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
448	337, 447	syld 47	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( 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 + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
449	448	expcom 451	. . . . . . . . . . . . . . . 16 |- ( x e. NN -> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( 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 + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) ) )
450	449	a2d 29	. . . . . . . . . . . . . . 15 |- ( x e. NN -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) -> ( ( ( 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 ) ) ) ) ) ) ) )
451	256, 266, 276, 286, 330, 450	nnind 11038	. . . . . . . . . . . . . 14 |- ( n e. NN -> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) )
452	235, 451	mpcom 38	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) )
453	237, 452	mpd 15	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
454	245, 453	eqbrtrrd 4677	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E Y ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
455		ffn 6045	. . . . . . . . . . . . . 14 |- ( ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) -> ( E o. g ) Fn ( 1 ... n ) )
456		fnresdm 6000	. . . . . . . . . . . . . 14 |- ( ( E o. g ) Fn ( 1 ... n ) -> ( ( E o. g ) |` ( 1 ... n ) ) = ( E o. g ) )
457	52, 455, 456	3syl 18	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` ( 1 ... n ) ) = ( E o. g ) )
458	457	oveq2d 6666	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) = ( W gsumg ( E o. g ) ) )
459	63, 458	eqtr4d 2659	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
460	454, 459	breqtrrd 4681	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E Y ) <_ ( RR*s gsumg ( E o. g ) ) )
461		breq2 4657	. . . . . . . . . 10 |- ( p = ( RR*s gsumg ( E o. g ) ) -> ( ( X E Y ) <_ p <-> ( X E Y ) <_ ( RR*s gsumg ( E o. g ) ) ) )
462	460, 461	syl5ibrcom 237	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( p = ( RR*s gsumg ( E o. g ) ) -> ( X E Y ) <_ p ) )
463	462	rexlimdva 3031	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( E. g e. S p = ( RR*s gsumg ( E o. g ) ) -> ( X E Y ) <_ p ) )
464	227, 463	syl5bi 232	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) -> ( X E Y ) <_ p ) )
465	464	rexlimdva 3031	. . . . . 6 |- ( ph -> ( E. n e. NN p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) -> ( X E Y ) <_ p ) )
466	224, 465	syl5bi 232	. . . . 5 |- ( ph -> ( p e. T -> ( X E Y ) <_ p ) )
467	466	ralrimiv 2965	. . . 4 |- ( ph -> A. p e. T ( X E Y ) <_ p )
468		infxrgelb 12165	. . . . 5 |- ( ( T C_ RR* /\ ( X E Y ) e. RR* ) -> ( ( X E Y ) <_ inf ( T , RR* , < ) <-> A. p e. T ( X E Y ) <_ p ) )
469	82, 86, 468	syl2anc 693	. . . 4 |- ( ph -> ( ( X E Y ) <_ inf ( T , RR* , < ) <-> A. p e. T ( X E Y ) <_ p ) )
470	467, 469	mpbird 247	. . 3 |- ( ph -> ( X E Y ) <_ inf ( T , RR* , < ) )
471	84, 86, 221, 470	xrletrid 11986	. 2 |- ( ph -> inf ( T , RR* , < ) = ( X E Y ) )
472	20, 471	eqtrd 2656	1 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   {crab 2916   _Vcvv 3200   \ cdif 3571   u. cun 3572   i^i cin 3573   C_ wss 3574   (/)c0 3915   {csn 4177   <.cop 4183   U_ciun 4520   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   ran crn 5115   |` cres 5116   o. ccom 5118   Fn wfn 5883   -->wf 5884   -1-1->wf1 5885   -onto->wfo 5886   -1-1-onto->wf1o 5887   ` cfv 5888  (class class class)co 6650   1stc1st 7166   2ndc2nd 7167   ^m cmap 7857   Fincfn 7955  infcinf 8347   RRcr 9935   0cc0 9936   1c1 9937   + caddc 9939   -oocmnf 10072   RR*cxr 10073   < clt 10074   <_ cle 10075   - cmin 10266   NNcn 11020   ZZcz 11377   ZZ>=cuz 11687   +ecxad 11944   ...cfz 12326   Basecbs 15857   ↾_s cress 15858   +g cplusg 15941   distcds 15950   gsum_g cgsu 16101   RR*scxrs 16160   "_s cimas 16164   Mndcmnd 17294  CMndccmn 18193   *Metcxmt 19731

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-pre-sup 10014

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-oadd 7564  df-er 7742  df-map 7859  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-inf 8349  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-xneg 11946  df-xadd 11947  df-xmul 11948  df-fz 12327  df-fzo 12466  df-seq 12802  df-hash 13118  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-0g 16102  df-gsum 16103  df-xrs 16162  df-imas 16168  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-submnd 17336  df-mulg 17541  df-cntz 17750  df-cmn 18195  df-xmet 19739

This theorem is referenced by:  imasdsf1o  22179