Theorem imasdsf1olem 19953

Description: Lemma for imasdsf1o 19954. (Contributed by Mario Carneiro, 21-Aug-2015.)

Hypotheses

Ref	Expression
imasdsf1o.u	|- ( ph -> U = ( F "s R ) )
imasdsf1o.v	|- ( ph -> V = ( Base ` R ) )
imasdsf1o.f	|- ( ph -> F : V -1-1-onto-> B )
imasdsf1o.r	|- ( ph -> R e. Z )
imasdsf1o.e	|- E = ( ( dist ` R ) |` ( V X. V ) )
imasdsf1o.d	|- D = ( dist ` U )
imasdsf1o.m	|- ( ph -> E e. ( *Met ` V ) )
imasdsf1o.x	|- ( ph -> X e. V )
imasdsf1o.y	|- ( ph -> Y e. V )
imasdsf1o.w	|- W = ( RR*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 5653	. . . . 5 |- ( F : V -1-1-onto-> B -> F : V -onto-> B )
5	3, 4	syl 16	. . . 4 |- ( ph -> F : V -onto-> B )
6		imasdsf1o.r	. . . 4 |- ( ph -> R e. Z )
7		eqid 2443	. . . 4 |- ( dist ` R ) = ( dist ` R )
8		imasdsf1o.d	. . . 4 |- D = ( dist ` U )
9		f1of 5646	. . . . . 6 |- ( F : V -1-1-onto-> B -> F : V --> B )
10	3, 9	syl 16	. . . . 5 |- ( ph -> F : V --> B )
11		imasdsf1o.x	. . . . 5 |- ( ph -> X e. V )
12	10, 11	ffvelrnd 5849	. . . 4 |- ( ph -> ( F ` X ) e. B )
13		imasdsf1o.y	. . . . 5 |- ( ph -> Y e. V )
14	10, 13	ffvelrnd 5849	. . . 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 14459	. . 3 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < ) )
18		imasdsf1o.t	. . . 4 |- T = U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
19	18	supeq1i 7702	. . 3 |- sup ( T , RR* , `' < ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < )
20	17, 19	syl6eqr 2493	. 2 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = sup ( T , RR* , `' < ) )
21		xrsbas 17837	. . . . . . . . . . . 12 |- RR* = ( Base ` RR*s )
22		xrsadd 17838	. . . . . . . . . . . 12 |- +e = ( +g ` RR*s )
23		imasdsf1o.w	. . . . . . . . . . . 12 |- W = ( RR*s ↾s ( RR* \ { -oo } ) )
24		xrsex 17836	. . . . . . . . . . . . 13 |- RR*s e. _V
25	24	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR*s e. _V )
26		fzfid 11800	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
27		difss 3488	. . . . . . . . . . . . 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 19909	. . . . . . . . . . . . . . . 16 |- ( E e. ( *Met ` V ) -> E : ( V X. V ) --> RR* )
31		ffn 5564	. . . . . . . . . . . . . . . 16 |- ( E : ( V X. V ) --> RR* -> E Fn ( V X. V ) )
32	29, 30, 31	3syl 20	. . . . . . . . . . . . . . 15 |- ( ph -> E Fn ( V X. V ) )
33		xmetcl 19911	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34		xmetge0 19924	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35		ge0nemnf 11150	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f E g ) e. RR* /\ 0 <_ ( f E g ) ) -> ( f E g ) =/= -oo )
36	33, 34, 35	syl2anc 661	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) =/= -oo )
37		eldifsn 4005	. . . . . . . . . . . . . . . . . . 19 |- ( ( f E g ) e. ( RR* \ { -oo } ) <-> ( ( f E g ) e. RR* /\ ( f E g ) =/= -oo ) )
38	33, 36, 37	sylanbrc 664	. . . . . . . . . . . . . . . . . 18 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. ( RR* \ { -oo } ) )
39	38	3expb 1188	. . . . . . . . . . . . . . . . 17 |- ( ( E e. ( *Met ` V ) /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
40	29, 39	sylan 471	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
41	40	ralrimivva 2813	. . . . . . . . . . . . . . 15 |- ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42		ffnov 6199	. . . . . . . . . . . . . . 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 664	. . . . . . . . . . . . . 14 |- ( ph -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
44	43	ad2antrr 725	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
45		ssrab2 3442	. . . . . . . . . . . . . . . . 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 3391	. . . . . . . . . . . . . . . 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 3361	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
49		elmapi 7239	. . . . . . . . . . . . . 14 |- ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
50	48, 49	syl 16	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g : ( 1 ... n ) --> ( V X. V ) )
51		fco 5573	. . . . . . . . . . . . 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 661	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
53		0re 9391	. . . . . . . . . . . . 13 |- 0 e. RR
54		rexr 9434	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 e. RR* )
55		renemnf 9437	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 =/= -oo )
56		eldifsn 4005	. . . . . . . . . . . . . 14 |- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
57	54, 55, 56	sylanbrc 664	. . . . . . . . . . . . 13 |- ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
58	53, 57	mp1i 12	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. ( RR* \ { -oo } ) )
59		xaddid2 11215	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( 0 +e x ) = x )
60		xaddid1 11214	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( x +e 0 ) = x )
61	59, 60	jca 532	. . . . . . . . . . . . 13 |- ( x e. RR* -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
62	61	adantl 466	. . . . . . . . . . . 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 15512	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) = ( W gsumg ( E o. g ) ) )
64	23, 21	ressbas2 14234	. . . . . . . . . . . . 13 |- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
65	27, 64	ax-mp 5	. . . . . . . . . . . 12 |- ( RR* \ { -oo } ) = ( Base ` W )
66	23	xrs10 17857	. . . . . . . . . . . 12 |- 0 = ( 0g ` W )
67	23	xrs1cmn 17858	. . . . . . . . . . . . 13 |- W e. CMnd
68	67	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
69		c0ex 9385	. . . . . . . . . . . . . 14 |- 0 e. _V
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. _V )
71	52, 26, 70	fdmfifsupp 7635	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) finSupp 0 )
72	65, 66, 68, 26, 52, 71	gsumcl 16402	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
73	63, 72	eqeltrd 2517	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
74	73	eldifad 3345	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. RR* )
75		eqid 2443	. . . . . . . . 9 |- ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
76	74, 75	fmptd 5872	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* )
77		frn 5570	. . . . . . . 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 16	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
79	78	ralrimiva 2804	. . . . . 6 |- ( ph -> A. n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
80		iunss 4216	. . . . . 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 212	. . . . 5 |- ( ph -> U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
82	18, 81	syl5eqss 3405	. . . 4 |- ( ph -> T C_ RR* )
83		1nn 10338	. . . . . . 7 |- 1 e. NN
84		1ex 9386	. . . . . . . . . . . 12 |- 1 e. _V
85		opex 4561	. . . . . . . . . . . 12 |- <. X , Y >. e. _V
86	84, 85	f1osn 5683	. . . . . . . . . . 11 |- { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
87		f1of 5646	. . . . . . . . . . 11 |- ( { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. } -> { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } )
88	86, 87	ax-mp 5	. . . . . . . . . 10 |- { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. }
89		opelxpi 4876	. . . . . . . . . . . 12 |- ( ( X e. V /\ Y e. V ) -> <. X , Y >. e. ( V X. V ) )
90	11, 13, 89	syl2anc 661	. . . . . . . . . . 11 |- ( ph -> <. X , Y >. e. ( V X. V ) )
91	90	snssd 4023	. . . . . . . . . 10 |- ( ph -> { <. X , Y >. } C_ ( V X. V ) )
92		fss 5572	. . . . . . . . . 10 |- ( ( { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } /\ { <. X , Y >. } C_ ( V X. V ) ) -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
93	88, 91, 92	sylancr 663	. . . . . . . . 9 |- ( ph -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
94	29	elfvexd 5723	. . . . . . . . . . 11 |- ( ph -> V e. _V )
95		xpexg 6512	. . . . . . . . . . 11 |- ( ( V e. _V /\ V e. _V ) -> ( V X. V ) e. _V )
96	94, 94, 95	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( V X. V ) e. _V )
97		snex 4538	. . . . . . . . . 10 |- { 1 } e. _V
98		elmapg 7232	. . . . . . . . . 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 ) ) )
99	96, 97, 98	sylancl 662	. . . . . . . . 9 |- ( ph -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
100	93, 99	mpbird 232	. . . . . . . 8 |- ( ph -> { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) )
101		op1stg 6594	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 1st ` <. X , Y >. ) = X )
102	11, 13, 101	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( 1st ` <. X , Y >. ) = X )
103	102	fveq2d 5700	. . . . . . . . 9 |- ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
104		op2ndg 6595	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 2nd ` <. X , Y >. ) = Y )
105	11, 13, 104	syl2anc 661	. . . . . . . . . 10 |- ( ph -> ( 2nd ` <. X , Y >. ) = Y )
106	105	fveq2d 5700	. . . . . . . . 9 |- ( ph -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
107	103, 106	jca 532	. . . . . . . 8 |- ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
108	24	a1i 11	. . . . . . . . . 10 |- ( ph -> RR*s e. _V )
109		snfi 7395	. . . . . . . . . . 11 |- { 1 } e. Fin
110	109	a1i 11	. . . . . . . . . 10 |- ( ph -> { 1 } e. Fin )
111	27	a1i 11	. . . . . . . . . 10 |- ( ph -> ( RR* \ { -oo } ) C_ RR* )
112		xmetcl 19911	. . . . . . . . . . . . . 14 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
113	29, 11, 13, 112	syl3anc 1218	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) e. RR* )
114		xmetge0 19924	. . . . . . . . . . . . . . 15 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
115	29, 11, 13, 114	syl3anc 1218	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( X E Y ) )
116		ge0nemnf 11150	. . . . . . . . . . . . . 14 |- ( ( ( X E Y ) e. RR* /\ 0 <_ ( X E Y ) ) -> ( X E Y ) =/= -oo )
117	113, 115, 116	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) =/= -oo )
118		eldifsn 4005	. . . . . . . . . . . . 13 |- ( ( X E Y ) e. ( RR* \ { -oo } ) <-> ( ( X E Y ) e. RR* /\ ( X E Y ) =/= -oo ) )
119	113, 117, 118	sylanbrc 664	. . . . . . . . . . . 12 |- ( ph -> ( X E Y ) e. ( RR* \ { -oo } ) )
120		fconst6g 5604	. . . . . . . . . . . 12 |- ( ( X E Y ) e. ( RR* \ { -oo } ) -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
121	119, 120	syl 16	. . . . . . . . . . 11 |- ( ph -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
122		fcoconst 5885	. . . . . . . . . . . . . 14 |- ( ( E Fn ( V X. V ) /\ <. X , Y >. e. ( V X. V ) ) -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
123	32, 90, 122	syl2anc 661	. . . . . . . . . . . . 13 |- ( ph -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
124	84, 85	xpsn 5890	. . . . . . . . . . . . . 14 |- ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
125	124	coeq2i 5005	. . . . . . . . . . . . 13 |- ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
126		df-ov 6099	. . . . . . . . . . . . . . . 16 |- ( X E Y ) = ( E ` <. X , Y >. )
127	126	eqcomi 2447	. . . . . . . . . . . . . . 15 |- ( E ` <. X , Y >. ) = ( X E Y )
128	127	sneqi 3893	. . . . . . . . . . . . . 14 |- { ( E ` <. X , Y >. ) } = { ( X E Y ) }
129	128	xpeq2i 4866	. . . . . . . . . . . . 13 |- ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
130	123, 125, 129	3eqtr3g 2498	. . . . . . . . . . . 12 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
131	130	feq1d 5551	. . . . . . . . . . 11 |- ( ph -> ( ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) <-> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) ) )
132	121, 131	mpbird 232	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) )
133	53, 57	mp1i 12	. . . . . . . . . 10 |- ( ph -> 0 e. ( RR* \ { -oo } ) )
134	61	adantl 466	. . . . . . . . . 10 |- ( ( ph /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
135	21, 22, 23, 108, 110, 111, 132, 133, 134	gsumress 15512	. . . . . . . . 9 |- ( ph -> ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
136		fconstmpt 4887	. . . . . . . . . . 11 |- ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
137	130, 136	syl6eq 2491	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
138	137	oveq2d 6112	. . . . . . . . 9 |- ( ph -> ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
139		cmnmnd 16297	. . . . . . . . . . 11 |- ( W e. CMnd -> W e. Mnd )
140	67, 139	mp1i 12	. . . . . . . . . 10 |- ( ph -> W e. Mnd )
141	83	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN )
142		eqidd 2444	. . . . . . . . . . 11 |- ( j = 1 -> ( X E Y ) = ( X E Y ) )
143	65, 142	gsumsn 16454	. . . . . . . . . 10 |- ( ( W e. Mnd /\ 1 e. NN /\ ( X E Y ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
144	140, 141, 119, 143	syl3anc 1218	. . . . . . . . 9 |- ( ph -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
145	135, 138, 144	3eqtrrd 2480	. . . . . . . 8 |- ( ph -> ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
146		fveq1 5695	. . . . . . . . . . . . . . 15 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
147	84, 85	fvsn 5916	. . . . . . . . . . . . . . 15 |- ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
148	146, 147	syl6eq 2491	. . . . . . . . . . . . . 14 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
149	148	fveq2d 5700	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
150	149	fveq2d 5700	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
151	150	eqeq1d 2451	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
152	148	fveq2d 5700	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
153	152	fveq2d 5700	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
154	153	eqeq1d 2451	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
155	151, 154	anbi12d 710	. . . . . . . . . 10 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) <-> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) ) )
156		coeq2 5003	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
157	156	oveq2d 6112	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( RR*s gsumg ( E o. g ) ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
158	157	eqeq2d 2454	. . . . . . . . . 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 >. >. } ) ) ) )
159	155, 158	anbi12d 710	. . . . . . . . 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 >. >. } ) ) ) ) )
160	159	rspcev 3078	. . . . . . . 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 ) ) ) )
161	100, 107, 145, 160	syl12anc 1216	. . . . . . 7 |- ( ph -> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
162		ovex 6121	. . . . . . . . . 10 |- ( X E Y ) e. _V
163	75	elrnmpt 5091	. . . . . . . . . 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 ) ) ) )
164	162, 163	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 ) ) )
165	15	rexeqi 2927	. . . . . . . . . . 11 |- ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } ( X E Y ) = ( RR*s gsumg ( E o. g ) ) )
166		fveq1 5695	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
167	166	fveq2d 5700	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
168	167	fveq2d 5700	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( g ` 1 ) ) ) )
169	168	eqeq1d 2451	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
170		fveq1 5695	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` n ) = ( g ` n ) )
171	170	fveq2d 5700	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
172	171	fveq2d 5700	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( g ` n ) ) ) )
173	172	eqeq1d 2451	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
174		fveq1 5695	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` i ) = ( g ` i ) )
175	174	fveq2d 5700	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
176	175	fveq2d 5700	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
177		fveq1 5695	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
178	177	fveq2d 5700	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
179	178	fveq2d 5700	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
180	176, 179	eqeq12d 2457	. . . . . . . . . . . . . 14 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
181	180	ralbidv 2740	. . . . . . . . . . . . 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 ) ) ) ) ) )
182	169, 173, 181	3anbi123d 1289	. . . . . . . . . . . 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 ) ) ) ) ) ) )
183	182	rexrab 3128	. . . . . . . . . . 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 ) ) ) )
184	165, 183	bitri 249	. . . . . . . . . 10 |- ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. ( ( V X. V ) ^m ( 1 ... n ) ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
185		oveq2 6104	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
186		1z 10681	. . . . . . . . . . . . . 14 |- 1 e. ZZ
187		fzsn 11505	. . . . . . . . . . . . . 14 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
188	186, 187	ax-mp 5	. . . . . . . . . . . . 13 |- ( 1 ... 1 ) = { 1 }
189	185, 188	syl6eq 2491	. . . . . . . . . . . 12 |- ( n = 1 -> ( 1 ... n ) = { 1 } )
190	189	oveq2d 6112	. . . . . . . . . . 11 |- ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
191		df-3an 967	. . . . . . . . . . . . 13 |- ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
192		ral0 3789	. . . . . . . . . . . . . . . 16 |- A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
193		oveq1 6103	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
194		1m1e0 10395	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 - 1 ) = 0
195	193, 194	syl6eq 2491	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = 0 )
196	195	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
197		fz10 11475	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... 0 ) = (/)
198	196, 197	syl6eq 2491	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
199	198	raleqdv 2928	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
200	192, 199	mpbiri 233	. . . . . . . . . . . . . . 15 |- ( n = 1 -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
201	200	biantrud 507	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) ) )
202		fveq2 5696	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( g ` n ) = ( g ` 1 ) )
203	202	fveq2d 5700	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
204	203	fveq2d 5700	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` ( 2nd ` ( g ` 1 ) ) ) )
205	204	eqeq1d 2451	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) )
206	205	anbi2d 703	. . . . . . . . . . . . . 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 ) ) ) )
207	201, 206	bitr3d 255	. . . . . . . . . . . . 13 |- ( n = 1 -> ( ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) ) )
208	191, 207	syl5bb 257	. . . . . . . . . . . 12 |- ( n = 1 -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) ) )
209	208	anbi1d 704	. . . . . . . . . . 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 ) ) ) ) )
210	190, 209	rexeqbidv 2937	. . . . . . . . . 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 ) ) ) ) )
211	184, 210	syl5bb 257	. . . . . . . . 9 |- ( n = 1 -> ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
212	164, 211	syl5bb 257	. . . . . . . 8 |- ( n = 1 -> ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
213	212	rspcev 3078	. . . . . . 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 ) ) ) )
214	83, 161, 213	sylancr 663	. . . . . 6 |- ( ph -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
215		eliun 4180	. . . . . 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 ) ) ) )
216	214, 215	sylibr 212	. . . . 5 |- ( ph -> ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
217	216, 18	syl6eleqr 2534	. . . 4 |- ( ph -> ( X E Y ) e. T )
218		infmxrlb 11301	. . . 4 |- ( ( T C_ RR* /\ ( X E Y ) e. T ) -> sup ( T , RR* , `' < ) <_ ( X E Y ) )
219	82, 217, 218	syl2anc 661	. . 3 |- ( ph -> sup ( T , RR* , `' < ) <_ ( X E Y ) )
220	18	eleq2i 2507	. . . . . . 7 |- ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
221		eliun 4180	. . . . . . 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 ) ) ) )
222	220, 221	bitri 249	. . . . . 6 |- ( p e. T <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
223		vex 2980	. . . . . . . . 9 |- p e. _V
224	75	elrnmpt 5091	. . . . . . . . 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 ) ) ) )
225	223, 224	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 ) ) )
226	182, 15	elrab2 3124	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
227	226	simprbi 464	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
228	227	adantl 466	. . . . . . . . . . . . . . 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 ) ) ) ) ) )
229	228	simp2d 1001	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) )
230	3	ad2antrr 725	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-onto-> B )
231		f1of1 5645	. . . . . . . . . . . . . . . 16 |- ( F : V -1-1-onto-> B -> F : V -1-1-> B )
232	230, 231	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-> B )
233		simplr 754	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
234		elfz1end 11484	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN <-> n e. ( 1 ... n ) )
235	233, 234	sylib 196	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( 1 ... n ) )
236	50, 235	ffvelrnd 5849	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
237		xp2nd 6612	. . . . . . . . . . . . . . . 16 |- ( ( g ` n ) e. ( V X. V ) -> ( 2nd ` ( g ` n ) ) e. V )
238	236, 237	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) e. V )
239	13	ad2antrr 725	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> Y e. V )
240		f1fveq 5980	. . . . . . . . . . . . . . 15 |- ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` n ) ) e. V /\ Y e. V ) ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
241	232, 238, 239, 240	syl12anc 1216	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
242	229, 241	mpbid 210	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) = Y )
243	242	oveq2d 6112	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
244		eleq1 2503	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
245		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( g ` m ) = ( g ` 1 ) )
246	245	fveq2d 5700	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
247	246	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
248		oveq2 6104	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
249	248, 188	syl6eq 2491	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
250	249	reseq2d 5115	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
251	250	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
252	247, 251	breq12d 4310	. . . . . . . . . . . . . . . . 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 } ) ) ) )
253	244, 252	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) ) )
254	253	imbi2d 316	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) ) ) )
255		eleq1 2503	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
256		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( g ` m ) = ( g ` x ) )
257	256	fveq2d 5700	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
258	257	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
259		oveq2 6104	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
260	259	reseq2d 5115	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
261	260	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) )
262	258, 261	breq12d 4310	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
263	255, 262	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( m = x -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
264	263	imbi2d 316	. . . . . . . . . . . . . . 15 |- ( m = x -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) ) )
265		eleq1 2503	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
266		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( g ` m ) = ( g ` ( x + 1 ) ) )
267	266	fveq2d 5700	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
268	267	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
269		oveq2 6104	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
270	269	reseq2d 5115	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
271	270	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
272	268, 271	breq12d 4310	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
273	265, 272	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( m = ( x + 1 ) -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
274	273	imbi2d 316	. . . . . . . . . . . . . . 15 |- ( m = ( x + 1 ) -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) ) )
275		eleq1 2503	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
276		fveq2 5696	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( g ` m ) = ( g ` n ) )
277	276	fveq2d 5700	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
278	277	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
279		oveq2 6104	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
280	279	reseq2d 5115	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
281	280	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
282	278, 281	breq12d 4310	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
283	275, 282	imbi12d 320	. . . . . . . . . . . . . . . 16 |- ( m = n -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) )
284	283	imbi2d 316	. . . . . . . . . . . . . . 15 |- ( m = n -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) ) )
285	29	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E e. ( *Met ` V ) )
286	11	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> X e. V )
287		nnuz 10901	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN = ( ZZ>= ` 1 )
288	233, 287	syl6eleq 2533	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
289		eluzfz1 11463	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
290	288, 289	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. ( 1 ... n ) )
291	50, 290	ffvelrnd 5849	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
292		xp2nd 6612	. . . . . . . . . . . . . . . . . . . 20 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 2nd ` ( g ` 1 ) ) e. V )
293	291, 292	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` 1 ) ) e. V )
294		xmetcl 19911	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` 1 ) ) e. V ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
295	285, 286, 293, 294	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
296		xrleid 11132	. . . . . . . . . . . . . . . . . 18 |- ( ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
297	295, 296	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
298	140	ad2antrr 725	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. Mnd )
299	83	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. NN )
300	44, 291	ffvelrnd 5849	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
301		fveq2 5696	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = 1 -> ( g ` j ) = ( g ` 1 ) )
302	301	fveq2d 5700	. . . . . . . . . . . . . . . . . . . 20 |- ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
303	65, 302	gsumsn 16454	. . . . . . . . . . . . . . . . . . 19 |- ( ( W e. Mnd /\ 1 e. NN /\ ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
304	298, 299, 300, 303	syl3anc 1218	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
305	285, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> RR* )
306		fcompt 5884	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( E : ( V X. V ) --> RR* /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
307	305, 50, 306	syl2anc 661	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
308	307	reseq1d 5114	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
309	290	snssd 4023	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
310		resmpt 5161	. . . . . . . . . . . . . . . . . . . . 21 |- ( { 1 } C_ ( 1 ... n ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
311	309, 310	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
312	308, 311	eqtrd 2475	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
313	312	oveq2d 6112	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) )
314		df-ov 6099	. . . . . . . . . . . . . . . . . . 19 |- ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
315		1st2nd2 6618	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
316	291, 315	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
317	228	simp1d 1000	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
318		xp1st 6611	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
319	291, 318	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
320		f1fveq 5980	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : V -1-1-> B /\ ( ( 1st ` ( g ` 1 ) ) e. V /\ X e. V ) ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
321	232, 319, 286, 320	syl12anc 1216	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
322	317, 321	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
323	322	opeq1d 4070	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
324	316, 323	eqtr2d 2476	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
325	324	fveq2d 5700	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
326	314, 325	syl5eq 2487	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
327	304, 313, 326	3eqtr4d 2485	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
328	297, 327	breqtrrd 4323	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
329	328	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 } ) ) ) )
330		simprl 755	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
331	330, 287	syl6eleq 2533	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
332		simprr 756	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
333		peano2fzr 11468	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
334	331, 332, 333	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
335	334	expr 615	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
336	335	imim1d 75	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
337	285	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( *Met ` V ) )
338	286	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
339	50	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
340	339, 334	ffvelrnd 5849	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
341		xp2nd 6612	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` x ) e. ( V X. V ) -> ( 2nd ` ( g ` x ) ) e. V )
342	340, 341	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) e. V )
343		xmetcl 19911	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` x ) ) e. V ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
344	337, 338, 342, 343	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
345	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> W e. CMnd )
346		fzfid 11800	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
347	52	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
348		fzsuc 11507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( ZZ>= ` 1 ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
349	331, 348	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
350		elfzuz3 11455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
351	350	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
352		fzss2 11503	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n e. ( ZZ>= ` ( x + 1 ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
353	351, 352	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
354	349, 353	eqsstr3d 3396	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) u. { ( x + 1 ) } ) C_ ( 1 ... n ) )
355	354	unssad 3538	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
356		fssres 5583	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) /\ ( 1 ... x ) C_ ( 1 ... n ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) : ( 1 ... x ) --> ( RR* \ { -oo } ) )
357	347, 355, 356	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . 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, 346, 358	fdmfifsupp 7635	. . . . . . . . . . . . . . . . . . . . . . . . 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, 345, 346, 357, 359	gsumcl 16402	. . . . . . . . . . . . . . . . . . . . . . . 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 3345	. . . . . . . . . . . . . . . . . . . . . . 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	337, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> RR* )
363	339, 332	ffvelrnd 5849	. . . . . . . . . . . . . . . . . . . . . . . 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 5849	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
365		xleadd1a 11221	. . . . . . . . . . . . . . . . . . . . . . . 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 434	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( X E ( 2nd ` ( g ` x ) ) ) e. RR* /\ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* /\ ( E ` ( g ` ( x + 1 ) ) ) e. RR* ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
367	344, 361, 364, 366	syl3anc 1218	. . . . . . . . . . . . . . . . . . . . . 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 6612	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
369	363, 368	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
370		xmettri 19931	. . . . . . . . . . . . . . . . . . . . . . . . 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	337, 338, 369, 342, 370	syl13anc 1220	. . . . . . . . . . . . . . . . . . . . . . . 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 6618	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
373	363, 372	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
374		nnz 10673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. NN -> x e. ZZ )
375	374	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
376		eluzp1m1 10889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= `