Theorem imasdsf1olem 18356

Description: Lemma for imasdsf1o 18357. (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 5640	. . . . 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 2404	. . . 4 |- ( dist ` R ) = ( dist ` R )
8		imasdsf1o.d	. . . 4 |- D = ( dist ` U )
9		f1of 5633	. . . . . 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 5830	. . . 4 |- ( ph -> ( F ` X ) e. B )
13		imasdsf1o.y	. . . . 5 |- ( ph -> Y e. V )
14	10, 13	ffvelrnd 5830	. . . 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 13697	. . 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 7410	. . 3 |- sup ( T , RR* , `' < ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) , RR* , `' < )
20	17, 19	syl6eqr 2454	. 2 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = sup ( T , RR* , `' < ) )
21		xrsbas 16672	. . . . . . . . . . . 12 |- RR* = ( Base ` RR* s )
22		xrsadd 16673	. . . . . . . . . . . 12 |- + e = ( +g ` RR* s )
23		imasdsf1o.w	. . . . . . . . . . . 12 |- W = ( RR* s ↾s ( RR* \ { -oo } ) )
24		xrsex 16671	. . . . . . . . . . . . 13 |- RR* s e. _V
25	24	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR* s e. _V )
26		fzfid 11267	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
27		difss 3434	. . . . . . . . . . . . 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 18312	. . . . . . . . . . . . . . . 16 |- ( E e. ( * Met ` V ) -> E : ( V X. V ) --> RR* )
31		ffn 5550	. . . . . . . . . . . . . . . 16 |- ( E : ( V X. V ) --> RR* -> E Fn ( V X. V ) )
32	29, 30, 31	3syl 19	. . . . . . . . . . . . . . 15 |- ( ph -> E Fn ( V X. V ) )
33		xmetcl 18314	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( * Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34		xmetge0 18327	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E e. ( * Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35		ge0nemnf 10717	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f E g ) e. RR* /\ 0 <_ ( f E g ) ) -> ( f E g ) =/= -oo )
36	33, 34, 35	syl2anc 643	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( * Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) =/= -oo )
37		eldifsn 3887	. . . . . . . . . . . . . . . . . . 19 |- ( ( f E g ) e. ( RR* \ { -oo } ) <-> ( ( f E g ) e. RR* /\ ( f E g ) =/= -oo ) )
38	33, 36, 37	sylanbrc 646	. . . . . . . . . . . . . . . . . 18 |- ( ( E e. ( * Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. ( RR* \ { -oo } ) )
39	38	3expb 1154	. . . . . . . . . . . . . . . . 17 |- ( ( E e. ( * Met ` V ) /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
40	29, 39	sylan 458	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
41	40	ralrimivva 2758	. . . . . . . . . . . . . . 15 |- ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42		ffnov 6133	. . . . . . . . . . . . . . 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 646	. . . . . . . . . . . . . 14 |- ( ph -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
44	43	ad2antrr 707	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
45		ssrab2 3388	. . . . . . . . . . . . . . . . 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 3338	. . . . . . . . . . . . . . . 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 3308	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
49		elmapi 6997	. . . . . . . . . . . . . 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 5559	. . . . . . . . . . . . 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 643	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
53		0re 9047	. . . . . . . . . . . . 13 |- 0 e. RR
54		rexr 9086	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 e. RR* )
55		renemnf 9089	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 =/= -oo )
56		eldifsn 3887	. . . . . . . . . . . . . 14 |- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
57	54, 55, 56	sylanbrc 646	. . . . . . . . . . . . 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 10782	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( 0 + e x ) = x )
60		xaddid1 10781	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( x + e 0 ) = x )
61	59, 60	jca 519	. . . . . . . . . . . . 13 |- ( x e. RR* -> ( ( 0 + e x ) = x /\ ( x + e 0 ) = x ) )
62	61	adantl 453	. . . . . . . . . . . 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 14732	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR* s gsumg ( E o. g ) ) = ( W gsumg ( E o. g ) ) )
64	23, 21	ressbas2 13475	. . . . . . . . . . . . 13 |- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
65	27, 64	ax-mp 8	. . . . . . . . . . . 12 |- ( RR* \ { -oo } ) = ( Base ` W )
66	23	xrs10 16692	. . . . . . . . . . . 12 |- 0 = ( 0g ` W )
67	23	xrs1cmn 16693	. . . . . . . . . . . . 13 |- W e. CMnd
68	67	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
69	26, 52	fisuppfi 14728	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( `' ( E o. g ) " ( _V \ { 0 } ) ) e. Fin )
70	65, 66, 68, 26, 52, 69	gsumcl 15476	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
71	63, 70	eqeltrd 2478	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR* s gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
72	71	eldifad 3292	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR* s gsumg ( E o. g ) ) e. RR* )
73		eqid 2404	. . . . . . . . 9 |- ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) = ( g e. S |-> ( RR* s gsumg ( E o. g ) ) )
74	72, 73	fmptd 5852	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) : S --> RR* )
75		frn 5556	. . . . . . . 8 |- ( ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) : S --> RR* -> ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) C_ RR* )
76	74, 75	syl 16	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) C_ RR* )
77	76	ralrimiva 2749	. . . . . 6 |- ( ph -> A. n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) C_ RR* )
78		iunss 4092	. . . . . 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* )
79	77, 78	sylibr 204	. . . . 5 |- ( ph -> U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) C_ RR* )
80	18, 79	syl5eqss 3352	. . . 4 |- ( ph -> T C_ RR* )
81		1nn 9967	. . . . . . 7 |- 1 e. NN
82		1ex 9042	. . . . . . . . . . . 12 |- 1 e. _V
83		opex 4387	. . . . . . . . . . . 12 |- <. X , Y >. e. _V
84	82, 83	f1osn 5674	. . . . . . . . . . 11 |- { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
85		f1of 5633	. . . . . . . . . . 11 |- ( { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. } -> { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } )
86	84, 85	ax-mp 8	. . . . . . . . . 10 |- { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. }
87		opelxpi 4869	. . . . . . . . . . . 12 |- ( ( X e. V /\ Y e. V ) -> <. X , Y >. e. ( V X. V ) )
88	11, 13, 87	syl2anc 643	. . . . . . . . . . 11 |- ( ph -> <. X , Y >. e. ( V X. V ) )
89	88	snssd 3903	. . . . . . . . . 10 |- ( ph -> { <. X , Y >. } C_ ( V X. V ) )
90		fss 5558	. . . . . . . . . 10 |- ( ( { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } /\ { <. X , Y >. } C_ ( V X. V ) ) -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
91	86, 89, 90	sylancr 645	. . . . . . . . 9 |- ( ph -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
92	29	elfvexd 5718	. . . . . . . . . . 11 |- ( ph -> V e. _V )
93		xpexg 4948	. . . . . . . . . . 11 |- ( ( V e. _V /\ V e. _V ) -> ( V X. V ) e. _V )
94	92, 92, 93	syl2anc 643	. . . . . . . . . 10 |- ( ph -> ( V X. V ) e. _V )
95		snex 4365	. . . . . . . . . 10 |- { 1 } e. _V
96		elmapg 6990	. . . . . . . . . 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 ) ) )
97	94, 95, 96	sylancl 644	. . . . . . . . 9 |- ( ph -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
98	91, 97	mpbird 224	. . . . . . . 8 |- ( ph -> { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) )
99		op1stg 6318	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 1st ` <. X , Y >. ) = X )
100	11, 13, 99	syl2anc 643	. . . . . . . . . 10 |- ( ph -> ( 1st ` <. X , Y >. ) = X )
101	100	fveq2d 5691	. . . . . . . . 9 |- ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
102		op2ndg 6319	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 2nd ` <. X , Y >. ) = Y )
103	11, 13, 102	syl2anc 643	. . . . . . . . . 10 |- ( ph -> ( 2nd ` <. X , Y >. ) = Y )
104	103	fveq2d 5691	. . . . . . . . 9 |- ( ph -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
105	101, 104	jca 519	. . . . . . . 8 |- ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
106	24	a1i 11	. . . . . . . . . . 11 |- ( ph -> RR* s e. _V )
107		snfi 7146	. . . . . . . . . . . 12 |- { 1 } e. Fin
108	107	a1i 11	. . . . . . . . . . 11 |- ( ph -> { 1 } e. Fin )
109	27	a1i 11	. . . . . . . . . . 11 |- ( ph -> ( RR* \ { -oo } ) C_ RR* )
110		xmetcl 18314	. . . . . . . . . . . . . . 15 |- ( ( E e. ( * Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
111	29, 11, 13, 110	syl3anc 1184	. . . . . . . . . . . . . 14 |- ( ph -> ( X E Y ) e. RR* )
112		xmetge0 18327	. . . . . . . . . . . . . . . 16 |- ( ( E e. ( * Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
113	29, 11, 13, 112	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ph -> 0 <_ ( X E Y ) )
114		ge0nemnf 10717	. . . . . . . . . . . . . . 15 |- ( ( ( X E Y ) e. RR* /\ 0 <_ ( X E Y ) ) -> ( X E Y ) =/= -oo )
115	111, 113, 114	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ph -> ( X E Y ) =/= -oo )
116		eldifsn 3887	. . . . . . . . . . . . . 14 |- ( ( X E Y ) e. ( RR* \ { -oo } ) <-> ( ( X E Y ) e. RR* /\ ( X E Y ) =/= -oo ) )
117	111, 115, 116	sylanbrc 646	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) e. ( RR* \ { -oo } ) )
118		fconst6g 5591	. . . . . . . . . . . . 13 |- ( ( X E Y ) e. ( RR* \ { -oo } ) -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
119	117, 118	syl 16	. . . . . . . . . . . 12 |- ( ph -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
120		fcoconst 5864	. . . . . . . . . . . . . . 15 |- ( ( E Fn ( V X. V ) /\ <. X , Y >. e. ( V X. V ) ) -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
121	32, 88, 120	syl2anc 643	. . . . . . . . . . . . . 14 |- ( ph -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
122	82, 83	xpsn 5869	. . . . . . . . . . . . . . 15 |- ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
123	122	coeq2i 4992	. . . . . . . . . . . . . 14 |- ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
124		df-ov 6043	. . . . . . . . . . . . . . . . 17 |- ( X E Y ) = ( E ` <. X , Y >. )
125	124	eqcomi 2408	. . . . . . . . . . . . . . . 16 |- ( E ` <. X , Y >. ) = ( X E Y )
126	125	sneqi 3786	. . . . . . . . . . . . . . 15 |- { ( E ` <. X , Y >. ) } = { ( X E Y ) }
127	126	xpeq2i 4858	. . . . . . . . . . . . . 14 |- ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
128	121, 123, 127	3eqtr3g 2459	. . . . . . . . . . . . 13 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
129	128	feq1d 5539	. . . . . . . . . . . 12 |- ( ph -> ( ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) <-> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) ) )
130	119, 129	mpbird 224	. . . . . . . . . . 11 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) )
131	53, 57	mp1i 12	. . . . . . . . . . 11 |- ( ph -> 0 e. ( RR* \ { -oo } ) )
132	61	adantl 453	. . . . . . . . . . 11 |- ( ( ph /\ x e. RR* ) -> ( ( 0 + e x ) = x /\ ( x + e 0 ) = x ) )
133	21, 22, 23, 106, 108, 109, 130, 131, 132	gsumress 14732	. . . . . . . . . 10 |- ( ph -> ( RR* s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
134		fconstmpt 4880	. . . . . . . . . . . 12 |- ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
135	128, 134	syl6eq 2452	. . . . . . . . . . 11 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
136	135	oveq2d 6056	. . . . . . . . . 10 |- ( ph -> ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
137	133, 136	eqtrd 2436	. . . . . . . . 9 |- ( ph -> ( RR* s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
138		cmnmnd 15382	. . . . . . . . . . 11 |- ( W e. CMnd -> W e. Mnd )
139	67, 138	mp1i 12	. . . . . . . . . 10 |- ( ph -> W e. Mnd )
140	81	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN )
141		eqidd 2405	. . . . . . . . . . 11 |- ( j = 1 -> ( X E Y ) = ( X E Y ) )
142	65, 141	gsumsn 15498	. . . . . . . . . 10 |- ( ( W e. Mnd /\ 1 e. NN /\ ( X E Y ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
143	139, 140, 117, 142	syl3anc 1184	. . . . . . . . 9 |- ( ph -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
144	137, 143	eqtr2d 2437	. . . . . . . 8 |- ( ph -> ( X E Y ) = ( RR* s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
145		fveq1 5686	. . . . . . . . . . . . . . 15 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
146	82, 83	fvsn 5885	. . . . . . . . . . . . . . 15 |- ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
147	145, 146	syl6eq 2452	. . . . . . . . . . . . . 14 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
148	147	fveq2d 5691	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
149	148	fveq2d 5691	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
150	149	eqeq1d 2412	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
151	147	fveq2d 5691	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
152	151	fveq2d 5691	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
153	152	eqeq1d 2412	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
154	150, 153	anbi12d 692	. . . . . . . . . 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 ) ) ) )
155		coeq2 4990	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
156	155	oveq2d 6056	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( RR* s gsumg ( E o. g ) ) = ( RR* s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
157	156	eqeq2d 2415	. . . . . . . . . 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 >. >. } ) ) ) )
158	154, 157	anbi12d 692	. . . . . . . . 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 >. >. } ) ) ) ) )
159	158	rspcev 3012	. . . . . . . 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 ) ) ) )
160	98, 105, 144, 159	syl12anc 1182	. . . . . . 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 ) ) ) )
161		ovex 6065	. . . . . . . . . 10 |- ( X E Y ) e. _V
162	73	elrnmpt 5076	. . . . . . . . . 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 ) ) ) )
163	161, 162	ax-mp 8	. . . . . . . . 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 ) ) )
164	15	rexeqi 2869	. . . . . . . . . . 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 ) ) )
165		fveq1 5686	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
166	165	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
167	166	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( g ` 1 ) ) ) )
168	167	eqeq1d 2412	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
169		fveq1 5686	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` n ) = ( g ` n ) )
170	169	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
171	170	fveq2d 5691	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( g ` n ) ) ) )
172	171	eqeq1d 2412	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
173		fveq1 5686	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` i ) = ( g ` i ) )
174	173	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
175	174	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
176		fveq1 5686	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
177	176	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
178	177	fveq2d 5691	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
179	175, 178	eqeq12d 2418	. . . . . . . . . . . . . 14 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
180	179	ralbidv 2686	. . . . . . . . . . . . 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 ) ) ) ) ) )
181	168, 172, 180	3anbi123d 1254	. . . . . . . . . . . 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 ) ) ) ) ) ) )
182	181	rexrab 3058	. . . . . . . . . . 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 ) ) ) )
183	164, 182	bitri 241	. . . . . . . . . 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 ) ) ) )
184		oveq2 6048	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
185		1z 10267	. . . . . . . . . . . . . 14 |- 1 e. ZZ
186		fzsn 11050	. . . . . . . . . . . . . 14 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
187	185, 186	ax-mp 8	. . . . . . . . . . . . 13 |- ( 1 ... 1 ) = { 1 }
188	184, 187	syl6eq 2452	. . . . . . . . . . . 12 |- ( n = 1 -> ( 1 ... n ) = { 1 } )
189	188	oveq2d 6056	. . . . . . . . . . 11 |- ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
190		df-3an 938	. . . . . . . . . . . . 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 ) ) ) ) ) )
191		ral0 3692	. . . . . . . . . . . . . . . 16 |- A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
192		oveq1 6047	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
193		1m1e0 10024	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 - 1 ) = 0
194	192, 193	syl6eq 2452	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = 0 )
195	194	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
196		fz10 11031	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... 0 ) = (/)
197	195, 196	syl6eq 2452	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
198	197	raleqdv 2870	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
199	191, 198	mpbiri 225	. . . . . . . . . . . . . . 15 |- ( n = 1 -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
200	199	biantrud 494	. . . . . . . . . . . . . 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 ) ) ) ) ) ) )
201		fveq2 5687	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( g ` n ) = ( g ` 1 ) )
202	201	fveq2d 5691	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
203	202	fveq2d 5691	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` ( 2nd ` ( g ` 1 ) ) ) )
204	203	eqeq1d 2412	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) )
205	204	anbi2d 685	. . . . . . . . . . . . . 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 ) ) ) )
206	200, 205	bitr3d 247	. . . . . . . . . . . . 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 ) ) ) )
207	190, 206	syl5bb 249	. . . . . . . . . . . 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 ) ) ) )
208	207	anbi1d 686	. . . . . . . . . . 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 ) ) ) ) )
209	189, 208	rexeqbidv 2877	. . . . . . . . . 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 ) ) ) ) )
210	183, 209	syl5bb 249	. . . . . . . . 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 ) ) ) ) )
211	163, 210	syl5bb 249	. . . . . . . 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 ) ) ) ) )
212	211	rspcev 3012	. . . . . . 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 ) ) ) )
213	81, 160, 212	sylancr 645	. . . . . 6 |- ( ph -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) )
214		eliun 4057	. . . . . 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 ) ) ) )
215	213, 214	sylibr 204	. . . . 5 |- ( ph -> ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) )
216	215, 18	syl6eleqr 2495	. . . 4 |- ( ph -> ( X E Y ) e. T )
217		infmxrlb 10868	. . . 4 |- ( ( T C_ RR* /\ ( X E Y ) e. T ) -> sup ( T , RR* , `' < ) <_ ( X E Y ) )
218	80, 216, 217	syl2anc 643	. . 3 |- ( ph -> sup ( T , RR* , `' < ) <_ ( X E Y ) )
219	18	eleq2i 2468	. . . . . . 7 |- ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) )
220		eliun 4057	. . . . . . 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 ) ) ) )
221	219, 220	bitri 241	. . . . . 6 |- ( p e. T <-> E. n e. NN p e. ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) )
222		vex 2919	. . . . . . . . 9 |- p e. _V
223	73	elrnmpt 5076	. . . . . . . . 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 ) ) ) )
224	222, 223	ax-mp 8	. . . . . . . 8 |- ( p e. ran ( g e. S |-> ( RR* s gsumg ( E o. g ) ) ) <-> E. g e. S p = ( RR* s gsumg ( E o. g ) ) )
225	181, 15	elrab2 3054	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
226	225	simprbi 451	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
227	226	adantl 453	. . . . . . . . . . . . . . 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 ) ) ) ) ) )
228	227	simp2d 970	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) )
229	3	ad2antrr 707	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-onto-> B )
230		f1of1 5632	. . . . . . . . . . . . . . . 16 |- ( F : V -1-1-onto-> B -> F : V -1-1-> B )
231	229, 230	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-> B )
232		simplr 732	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
233		elfz1end 11037	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN <-> n e. ( 1 ... n ) )
234	232, 233	sylib 189	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( 1 ... n ) )
235	50, 234	ffvelrnd 5830	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
236		xp2nd 6336	. . . . . . . . . . . . . . . 16 |- ( ( g ` n ) e. ( V X. V ) -> ( 2nd ` ( g ` n ) ) e. V )
237	235, 236	syl 16	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) e. V )
238	13	ad2antrr 707	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> Y e. V )
239		f1fveq 5967	. . . . . . . . . . . . . . 15 |- ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` n ) ) e. V /\ Y e. V ) ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
240	231, 237, 238, 239	syl12anc 1182	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
241	228, 240	mpbid 202	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) = Y )
242	241	oveq2d 6056	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
243		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
244		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( g ` m ) = ( g ` 1 ) )
245	244	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
246	245	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
247		oveq2 6048	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
248	247, 187	syl6eq 2452	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
249	248	reseq2d 5105	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
250	249	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
251	246, 250	breq12d 4185	. . . . . . . . . . . . . . . . 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 } ) ) ) )
252	243, 251	imbi12d 312	. . . . . . . . . . . . . . . 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 } ) ) ) ) )
253	252	imbi2d 308	. . . . . . . . . . . . . . 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 } ) ) ) ) ) )
254		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
255		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( g ` m ) = ( g ` x ) )
256	255	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
257	256	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
258		oveq2 6048	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
259	258	reseq2d 5105	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
260	259	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) )
261	257, 260	breq12d 4185	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
262	254, 261	imbi12d 312	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
263	262	imbi2d 308	. . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
264		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
265		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( g ` m ) = ( g ` ( x + 1 ) ) )
266	265	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
267	266	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
268		oveq2 6048	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
269	268	reseq2d 5105	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
270	269	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
271	267, 270	breq12d 4185	. . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
272	264, 271	imbi12d 312	. . . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
273	272	imbi2d 308	. . . . . . . . . . . . . . 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 ) ) ) ) ) ) ) )
274		eleq1 2464	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
275		fveq2 5687	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( g ` m ) = ( g ` n ) )
276	275	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
277	276	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
278		oveq2 6048	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
279	278	reseq2d 5105	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
280	279	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
281	277, 280	breq12d 4185	. . . . . . . . . . . . . . . . 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 ) ) ) ) )
282	274, 281	imbi12d 312	. . . . . . . . . . . . . . . 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 ) ) ) ) ) )
283	282	imbi2d 308	. . . . . . . . . . . . . . 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 ) ) ) ) ) ) )
284	29	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E e. ( * Met ` V ) )
285	11	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> X e. V )
286		nnuz 10477	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN = ( ZZ>= ` 1 )
287	232, 286	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
288		eluzfz1 11020	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
289	287, 288	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. ( 1 ... n ) )
290	50, 289	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
291		xp2nd 6336	. . . . . . . . . . . . . . . . . . . 20 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 2nd ` ( g ` 1 ) ) e. V )
292	290, 291	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` 1 ) ) e. V )
293		xmetcl 18314	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( * Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` 1 ) ) e. V ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
294	284, 285, 292, 293	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
295		xrleid 10699	. . . . . . . . . . . . . . . . . 18 |- ( ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
296	294, 295	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
297	139	ad2antrr 707	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. Mnd )
298	81	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. NN )
299	44, 290	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
300		fveq2 5687	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = 1 -> ( g ` j ) = ( g ` 1 ) )
301	300	fveq2d 5691	. . . . . . . . . . . . . . . . . . . 20 |- ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
302	65, 301	gsumsn 15498	. . . . . . . . . . . . . . . . . . 19 |- ( ( W e. Mnd /\ 1 e. NN /\ ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
303	297, 298, 299, 302	syl3anc 1184	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
304	284, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> RR* )
305		fcompt 5863	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( E : ( V X. V ) --> RR* /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
306	304, 50, 305	syl2anc 643	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
307	306	reseq1d 5104	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
308	289	snssd 3903	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
309		resmpt 5150	. . . . . . . . . . . . . . . . . . . . 21 |- ( { 1 } C_ ( 1 ... n ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
310	308, 309	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
311	307, 310	eqtrd 2436	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
312	311	oveq2d 6056	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) )
313		df-ov 6043	. . . . . . . . . . . . . . . . . . 19 |- ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
314		1st2nd2 6345	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
315	290, 314	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
316	227	simp1d 969	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
317		xp1st 6335	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
318	290, 317	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
319		f1fveq 5967	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : V -1-1-> B /\ ( ( 1st ` ( g ` 1 ) ) e. V /\ X e. V ) ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
320	231, 318, 285, 319	syl12anc 1182	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
321	316, 320	mpbid 202	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
322	321	opeq1d 3950	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
323	315, 322	eqtr2d 2437	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
324	323	fveq2d 5691	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
325	313, 324	syl5eq 2448	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
326	303, 312, 325	3eqtr4d 2446	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
327	296, 326	breqtrrd 4198	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
328	327	a1d 23	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) )
329		simprl 733	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
330	329, 286	syl6eleq 2494	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
331		simprr 734	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
332		peano2fzr 11025	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
333	330, 331, 332	syl2anc 643	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
334	333	expr 599	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
335	334	imim1d 71	. . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
336	284	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( * Met ` V ) )
337	285	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
338	50	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
339	338, 333	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
340		xp2nd 6336	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` x ) e. ( V X. V ) -> ( 2nd ` ( g ` x ) ) e. V )
341	339, 340	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) e. V )
342		xmetcl 18314	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( E e. ( * Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` x ) ) e. V ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
343	336, 337, 341, 342	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
344	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> W e. CMnd )
345		fzfid 11267	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
346	52	adantr 452	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
347		fzsuc 11052	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( ZZ>= ` 1 ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
348	330, 347	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 ) } ) )
349		elfzuz3 11012	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
350	349	ad2antll 710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
351		fzss2 11048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n e. ( ZZ>= ` ( x + 1 ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
352	350, 351	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
353	348, 352	eqsstr3d 3343	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) u. { ( x + 1 ) } ) C_ ( 1 ... n ) )
354	353	unssad 3484	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
355		fssres 5569	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) /\ ( 1 ... x ) C_ ( 1 ... n ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) : ( 1 ... x ) --> ( RR* \ { -oo } ) )
356	346, 354, 355	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
357	345, 356	fisuppfi 14728	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( `' ( ( E o. g ) |` ( 1 ... x ) ) " ( _V \ { 0 } ) ) e. Fin )
358	65, 66, 344, 345, 356, 357	gsumcl 15476	. . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
359	358	eldifad 3292	. . . . . . . . . . . . . . . . . . . . . . 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* )
360	336, 30	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> RR* )
361	338, 331	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) e. ( V X. V ) )
362	360, 361	ffvelrnd 5830	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
363		xleadd1a 10788	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) )
364	363	ex 424	. . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
365	343, 359, 362, 364	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
366		xp2nd 6336	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
367	361, 366	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
368		xmettri 18334	. . . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
369	336, 337, 367, 341, 368	syl13anc 1186	. . . . . . . . . . . . . . . . . . . . . . . 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 ) ) ) ) ) )
370		1st2nd2 6345	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
371	361, 370	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 ) ) ) >. )
372		nnz 10259	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. NN -> x e. ZZ )
373	372	ad2antrl 709	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
374		eluzp1m1 10465	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
375	373, 350, 374	syl2anc 64