Theorem imasdsf1olem 21002

Description: Lemma for imasdsf1o 21003. (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 5829	. . . . 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 2457	. . . 4 |- ( dist ` R ) = ( dist ` R )
8		imasdsf1o.d	. . . 4 |- D = ( dist ` U )
9		f1of 5822	. . . . . 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 6033	. . . 4 |- ( ph -> ( F ` X ) e. B )
13		imasdsf1o.y	. . . . 5 |- ( ph -> Y e. V )
14	10, 13	ffvelrnd 6033	. . . 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 14933	. . 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 7924	. . 3 |- sup ( T , RR* , `' < ) = sup ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , `' < )
20	17, 19	syl6eqr 2516	. 2 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = sup ( T , RR* , `' < ) )
21		xrsbas 18561	. . . . . . . . . . . 12 |- RR* = ( Base ` RR*s )
22		xrsadd 18562	. . . . . . . . . . . 12 |- +e = ( +g ` RR*s )
23		imasdsf1o.w	. . . . . . . . . . . 12 |- W = ( RR*s ↾s ( RR* \ { -oo } ) )
24		xrsex 18560	. . . . . . . . . . . . 13 |- RR*s e. _V
25	24	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR*s e. _V )
26		fzfid 12086	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
27		difss 3627	. . . . . . . . . . . . 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 20958	. . . . . . . . . . . . . . . 16 |- ( E e. ( *Met ` V ) -> E : ( V X. V ) --> RR* )
31		ffn 5737	. . . . . . . . . . . . . . . 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 20960	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34		xmetge0 20973	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35		ge0nemnf 11399	. . . . . . . . . . . . . . . . . . . 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 4157	. . . . . . . . . . . . . . . . . . 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 1197	. . . . . . . . . . . . . . . . 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 2878	. . . . . . . . . . . . . . 15 |- ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42		ffnov 6405	. . . . . . . . . . . . . . 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 3581	. . . . . . . . . . . . . . . . 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 3529	. . . . . . . . . . . . . . . 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 3499	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
49		elmapi 7459	. . . . . . . . . . . . . 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 5747	. . . . . . . . . . . . 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 9613	. . . . . . . . . . . . 13 |- 0 e. RR
54		rexr 9656	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 e. RR* )
55		renemnf 9659	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 =/= -oo )
56		eldifsn 4157	. . . . . . . . . . . . . 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 11464	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( 0 +e x ) = x )
60		xaddid1 11463	. . . . . . . . . . . . . 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 16030	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) = ( W gsumg ( E o. g ) ) )
64	23, 21	ressbas2 14702	. . . . . . . . . . . . 13 |- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
65	27, 64	ax-mp 5	. . . . . . . . . . . 12 |- ( RR* \ { -oo } ) = ( Base ` W )
66	23	xrs10 18584	. . . . . . . . . . . 12 |- 0 = ( 0g ` W )
67	23	xrs1cmn 18585	. . . . . . . . . . . . 13 |- W e. CMnd
68	67	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
69		c0ex 9607	. . . . . . . . . . . . . 14 |- 0 e. _V
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. _V )
71	52, 26, 70	fdmfifsupp 7857	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) finSupp 0 )
72	65, 66, 68, 26, 52, 71	gsumcl 17050	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
73	63, 72	eqeltrd 2545	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
74	73	eldifad 3483	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. RR* )
75		eqid 2457	. . . . . . . . 9 |- ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
76	74, 75	fmptd 6056	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* )
77		frn 5743	. . . . . . . 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 2871	. . . . . 6 |- ( ph -> A. n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
80		iunss 4373	. . . . . 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 3543	. . . 4 |- ( ph -> T C_ RR* )
83		1nn 10567	. . . . . . 7 |- 1 e. NN
84		1ex 9608	. . . . . . . . . . . 12 |- 1 e. _V
85		opex 4720	. . . . . . . . . . . 12 |- <. X , Y >. e. _V
86	84, 85	f1osn 5859	. . . . . . . . . . 11 |- { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
87		f1of 5822	. . . . . . . . . . 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 5040	. . . . . . . . . . . 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 4177	. . . . . . . . . 10 |- ( ph -> { <. X , Y >. } C_ ( V X. V ) )
92		fss 5745	. . . . . . . . . 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 5900	. . . . . . . . . . 11 |- ( ph -> V e. _V )
95		xpexg 6601	. . . . . . . . . . 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 4697	. . . . . . . . . 10 |- { 1 } e. _V
98		elmapg 7451	. . . . . . . . . 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 6811	. . . . . . . . . . 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 5876	. . . . . . . . 9 |- ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
104		op2ndg 6812	. . . . . . . . . . 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 5876	. . . . . . . . 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 7615	. . . . . . . . . . 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 20960	. . . . . . . . . . . . . 14 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
113	29, 11, 13, 112	syl3anc 1228	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) e. RR* )
114		xmetge0 20973	. . . . . . . . . . . . . . 15 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
115	29, 11, 13, 114	syl3anc 1228	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( X E Y ) )
116		ge0nemnf 11399	. . . . . . . . . . . . . 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 4157	. . . . . . . . . . . . 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 5780	. . . . . . . . . . . 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 6069	. . . . . . . . . . . . . 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 6074	. . . . . . . . . . . . . 14 |- ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
125	124	coeq2i 5173	. . . . . . . . . . . . 13 |- ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
126		df-ov 6299	. . . . . . . . . . . . . . . 16 |- ( X E Y ) = ( E ` <. X , Y >. )
127	126	eqcomi 2470	. . . . . . . . . . . . . . 15 |- ( E ` <. X , Y >. ) = ( X E Y )
128	127	sneqi 4043	. . . . . . . . . . . . . 14 |- { ( E ` <. X , Y >. ) } = { ( X E Y ) }
129	128	xpeq2i 5029	. . . . . . . . . . . . 13 |- ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
130	123, 125, 129	3eqtr3g 2521	. . . . . . . . . . . 12 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
131	130	feq1d 5723	. . . . . . . . . . 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 16030	. . . . . . . . 9 |- ( ph -> ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
136		fconstmpt 5052	. . . . . . . . . . 11 |- ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
137	130, 136	syl6eq 2514	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
138	137	oveq2d 6312	. . . . . . . . 9 |- ( ph -> ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
139		cmnmnd 16940	. . . . . . . . . . 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 2458	. . . . . . . . . . 11 |- ( j = 1 -> ( X E Y ) = ( X E Y ) )
143	65, 142	gsumsn 17108	. . . . . . . . . 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 1228	. . . . . . . . 9 |- ( ph -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
145	135, 138, 144	3eqtrrd 2503	. . . . . . . 8 |- ( ph -> ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
146		fveq1 5871	. . . . . . . . . . . . . . 15 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
147	84, 85	fvsn 6105	. . . . . . . . . . . . . . 15 |- ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
148	146, 147	syl6eq 2514	. . . . . . . . . . . . . 14 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
149	148	fveq2d 5876	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
150	149	fveq2d 5876	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
151	150	eqeq1d 2459	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
152	148	fveq2d 5876	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
153	152	fveq2d 5876	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
154	153	eqeq1d 2459	. . . . . . . . . . 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 5171	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
157	156	oveq2d 6312	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( RR*s gsumg ( E o. g ) ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
158	157	eqeq2d 2471	. . . . . . . . . 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 3210	. . . . . . . 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 1226	. . . . . . 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 6324	. . . . . . . . . 10 |- ( X E Y ) e. _V
163	75	elrnmpt 5259	. . . . . . . . . 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 3059	. . . . . . . . . . 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 5871	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
167	166	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
168	167	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( g ` 1 ) ) ) )
169	168	eqeq1d 2459	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
170		fveq1 5871	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` n ) = ( g ` n ) )
171	170	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
172	171	fveq2d 5876	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( g ` n ) ) ) )
173	172	eqeq1d 2459	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
174		fveq1 5871	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` i ) = ( g ` i ) )
175	174	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
176	175	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
177		fveq1 5871	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
178	177	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
179	178	fveq2d 5876	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
180	176, 179	eqeq12d 2479	. . . . . . . . . . . . . 14 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
181	180	ralbidv 2896	. . . . . . . . . . . . 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 1299	. . . . . . . . . . . 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 3263	. . . . . . . . . . 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 6304	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
186		1z 10915	. . . . . . . . . . . . . 14 |- 1 e. ZZ
187		fzsn 11751	. . . . . . . . . . . . . 14 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
188	186, 187	ax-mp 5	. . . . . . . . . . . . 13 |- ( 1 ... 1 ) = { 1 }
189	185, 188	syl6eq 2514	. . . . . . . . . . . 12 |- ( n = 1 -> ( 1 ... n ) = { 1 } )
190	189	oveq2d 6312	. . . . . . . . . . 11 |- ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
191		df-3an 975	. . . . . . . . . . . . 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 3937	. . . . . . . . . . . . . . . 16 |- A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
193		oveq1 6303	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
194		1m1e0 10625	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 - 1 ) = 0
195	193, 194	syl6eq 2514	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = 0 )
196	195	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
197		fz10 11731	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... 0 ) = (/)
198	196, 197	syl6eq 2514	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
199	198	raleqdv 3060	. . . . . . . . . . . . . . . 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 5872	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( g ` n ) = ( g ` 1 ) )
203	202	fveq2d 5876	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
204	203	fveq2d 5876	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` ( 2nd ` ( g ` 1 ) ) ) )
205	204	eqeq1d 2459	. . . . . . . . . . . . . . 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 3069	. . . . . . . . . 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 3210	. . . . . . 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 4337	. . . . . 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 2556	. . . 4 |- ( ph -> ( X E Y ) e. T )
218		infmxrlb 11550	. . . 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 2535	. . . . . . 7 |- ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
221		eliun 4337	. . . . . . 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 3112	. . . . . . . . 9 |- p e. _V
224	75	elrnmpt 5259	. . . . . . . . 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 3259	. . . . . . . . . . . . . . . . 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 1009	. . . . . . . . . . . . . 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 5821	. . . . . . . . . . . . . . . 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 755	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
234		elfz1end 11740	. . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
237		xp2nd 6830	. . . . . . . . . . . . . . . 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 6171	. . . . . . . . . . . . . . 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 1226	. . . . . . . . . . . . . 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 6312	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
244		eleq1 2529	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
245		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( g ` m ) = ( g ` 1 ) )
246	245	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
247	246	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
248		oveq2 6304	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
249	248, 188	syl6eq 2514	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
250	249	reseq2d 5283	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
251	250	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
252	247, 251	breq12d 4469	. . . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
256		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( g ` m ) = ( g ` x ) )
257	256	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
258	257	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
259		oveq2 6304	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
260	259	reseq2d 5283	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
261	260	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) )
262	258, 261	breq12d 4469	. . . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
266		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( g ` m ) = ( g ` ( x + 1 ) ) )
267	266	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
268	267	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
269		oveq2 6304	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
270	269	reseq2d 5283	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
271	270	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
272	268, 271	breq12d 4469	. . . . . . . . . . . . . . . . 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 2529	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
276		fveq2 5872	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( g ` m ) = ( g ` n ) )
277	276	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
278	277	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
279		oveq2 6304	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
280	279	reseq2d 5283	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
281	280	oveq2d 6312	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
282	278, 281	breq12d 4469	. . . . . . . . . . . . . . . . 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 11141	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN = ( ZZ>= ` 1 )
288	233, 287	syl6eleq 2555	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
289		eluzfz1 11718	. . . . . . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
292		xp2nd 6830	. . . . . . . . . . . . . . . . . . . 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 20960	. . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
296		xrleid 11381	. . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
301		fveq2 5872	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = 1 -> ( g ` j ) = ( g ` 1 ) )
302	301	fveq2d 5876	. . . . . . . . . . . . . . . . . . . 20 |- ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
303	65, 302	gsumsn 17108	. . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . 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 6068	. . . . . . . . . . . . . . . . . . . . . 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 5282	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
309	290	snssd 4177	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
310	309	resmptd 5335	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
311	308, 310	eqtrd 2498	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
312	311	oveq2d 6312	. . . . . . . . . . . . . . . . . 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 6299	. . . . . . . . . . . . . . . . . . 19 |- ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
314		1st2nd2 6836	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
315	291, 314	syl 16	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
316	228	simp1d 1008	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
317		xp1st 6829	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
318	291, 317	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
319		f1fveq 6171	. . . . . . . . . . . . . . . . . . . . . . . 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	232, 318, 286, 319	syl12anc 1226	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
321	316, 320	mpbid 210	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
322	321	opeq1d 4225	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
323	315, 322	eqtr2d 2499	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
324	323	fveq2d 5876	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
325	313, 324	syl5eq 2510	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
326	304, 312, 325	3eqtr4d 2508	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
327	297, 326	breqtrrd 4482	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
328	327	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 } ) ) ) )
329		simprl 756	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
330	329, 287	syl6eleq 2555	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
331		simprr 757	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
332		peano2fzr 11724	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
333	330, 331, 332	syl2anc 661	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
334	333	expr 615	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
335	334	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 ) ) ) ) ) )
336	285	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( *Met ` V ) )
337	286	adantr 465	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
338	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 ) )
339	338, 333	ffvelrnd 6033	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
340		xp2nd 6830	. . . . . . . . . . . . . . . . . . . . . . . . 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 20960	. . . . . . . . . . . . . . . . . . . . . . . 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 1228	. . . . . . . . . . . . . . . . . . . . . . 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 12086	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
346	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 } ) )
347		fzsuc 11753	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 11710	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
350	349	ad2antll 728	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
351		fzss2 11749	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 3534	. . . . . . . . . . . . . . . . . . . . . . . . . . 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 3677	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
355	346, 354	fssresd 5758	. . . . . . . . . . . . . . . . . . . . . . . . 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 } ) )
356	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> 0 e. _V )
357	355, 345, 356	fdmfifsupp 7857	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) finSupp 0 )
358	65, 66, 344, 345, 355, 357	gsumcl 17050	. . . . . . . . . . . . . . . . . . . . . . . 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 3483	. . . . . . . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . . . . . . 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 6033	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
363		xleadd1a 11470	. . . . . . . . . . . . . . . . . . . . . . . 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 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 ) ) ) ) ) )
365	343, 359, 362, 364	syl3anc 1228	. . . . . . . . . . . . . . . . . . . . . 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 6830	. . . . . . . . . . . . . . . . . . . . . . . . . 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 20980	. . . . . . . . . . . . . . . . . . . . . . . . 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 1230	. . . . . . . . . . . . . . . . . . . . . . . 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 6836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 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 10907	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. NN -> x e. ZZ )
373	372	ad2antrl 727	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
374		eluzp1m1 11129	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
375	373, 350, 374	syl2anc 661	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
376		elfzuzb 11707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. ( 1 ... ( n - 1 ) ) <-> ( x e. ( ZZ>= ` 1 ) /\ ( n - 1 ) e. ( ZZ>= ` x ) ) )
377	330, 375, 376	sylanbrc 664	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1