Theorem imasdsf1olem 21466

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

Hypotheses

Ref	Expression
imasdsf1o.u	|- ( ph -> U = ( F "s R ) )
imasdsf1o.v	|- ( ph -> V = ( Base ` R ) )
imasdsf1o.f	|- ( ph -> F : V -1-1-onto-> B )
imasdsf1o.r	|- ( ph -> R e. Z )
imasdsf1o.e	|- E = ( ( dist ` R ) |` ( V X. V ) )
imasdsf1o.d	|- D = ( dist ` U )
imasdsf1o.m	|- ( ph -> E e. ( *Met ` V ) )
imasdsf1o.x	|- ( ph -> X e. V )
imasdsf1o.y	|- ( ph -> Y e. V )
imasdsf1o.w	|- W = ( RR*s ↾s ( RR* \ { -oo } ) )
imasdsf1o.s	|- S = { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) }
imasdsf1o.t	|- T = U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )

Assertion

Ref	Expression
imasdsf1olem	|- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = ( X E Y ) )

Distinct variable groups:   g, h, i, n, F   ph, g, h, i, n   g, V, h, i, n   g, E, i, n   R, g, h, i, n   S, g   g, X, h, i, n   g, Y, h, i, n

Allowed substitution hints:   B( g, h, i, n)   D( g, h, i, n)   S( h, i, n)   T( g, h, i, n)   U( g, h, i, n)   E( h)   W( g, h, i, n)   Z( g, h, i, n)

Proof of Theorem imasdsf1olem

Dummy variables f j m p x are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		imasdsf1o.u	. . . 4 |- ( ph -> U = ( F "s R ) )
2		imasdsf1o.v	. . . 4 |- ( ph -> V = ( Base ` R ) )
3		imasdsf1o.f	. . . . 5 |- ( ph -> F : V -1-1-onto-> B )
4		f1ofo 5835	. . . . 5 |- ( F : V -1-1-onto-> B -> F : V -onto-> B )
5	3, 4	syl 17	. . . 4 |- ( ph -> F : V -onto-> B )
6		imasdsf1o.r	. . . 4 |- ( ph -> R e. Z )
7		eqid 2471	. . . 4 |- ( dist ` R ) = ( dist ` R )
8		imasdsf1o.d	. . . 4 |- D = ( dist ` U )
9		f1of 5828	. . . . . 6 |- ( F : V -1-1-onto-> B -> F : V --> B )
10	3, 9	syl 17	. . . . 5 |- ( ph -> F : V --> B )
11		imasdsf1o.x	. . . . 5 |- ( ph -> X e. V )
12	10, 11	ffvelrnd 6038	. . . 4 |- ( ph -> ( F ` X ) e. B )
13		imasdsf1o.y	. . . . 5 |- ( ph -> Y e. V )
14	10, 13	ffvelrnd 6038	. . . 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 15495	. . 3 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , < ) )
18		imasdsf1o.t	. . . 4 |- T = U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
19	18	infeq1i 8012	. . 3 |- inf ( T , RR* , < ) = inf ( U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) , RR* , < )
20	17, 19	syl6eqr 2523	. 2 |- ( ph -> ( ( F ` X ) D ( F ` Y ) ) = inf ( T , RR* , < ) )
21		xrsbas 19061	. . . . . . . . . . . 12 |- RR* = ( Base ` RR*s )
22		xrsadd 19062	. . . . . . . . . . . 12 |- +e = ( +g ` RR*s )
23		imasdsf1o.w	. . . . . . . . . . . 12 |- W = ( RR*s ↾s ( RR* \ { -oo } ) )
24		xrsex 19060	. . . . . . . . . . . . 13 |- RR*s e. _V
25	24	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> RR*s e. _V )
26		fzfid 12224	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 ... n ) e. Fin )
27		difss 3549	. . . . . . . . . . . . 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 21422	. . . . . . . . . . . . . . . 16 |- ( E e. ( *Met ` V ) -> E : ( V X. V ) --> RR* )
31		ffn 5739	. . . . . . . . . . . . . . . 16 |- ( E : ( V X. V ) --> RR* -> E Fn ( V X. V ) )
32	29, 30, 31	3syl 18	. . . . . . . . . . . . . . 15 |- ( ph -> E Fn ( V X. V ) )
33		xmetcl 21424	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. RR* )
34		xmetge0 21437	. . . . . . . . . . . . . . . . . . . 20 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> 0 <_ ( f E g ) )
35		ge0nemnf 11491	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( f E g ) e. RR* /\ 0 <_ ( f E g ) ) -> ( f E g ) =/= -oo )
36	33, 34, 35	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) =/= -oo )
37		eldifsn 4088	. . . . . . . . . . . . . . . . . . 19 |- ( ( f E g ) e. ( RR* \ { -oo } ) <-> ( ( f E g ) e. RR* /\ ( f E g ) =/= -oo ) )
38	33, 36, 37	sylanbrc 677	. . . . . . . . . . . . . . . . . 18 |- ( ( E e. ( *Met ` V ) /\ f e. V /\ g e. V ) -> ( f E g ) e. ( RR* \ { -oo } ) )
39	38	3expb 1232	. . . . . . . . . . . . . . . . 17 |- ( ( E e. ( *Met ` V ) /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
40	29, 39	sylan 479	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( f e. V /\ g e. V ) ) -> ( f E g ) e. ( RR* \ { -oo } ) )
41	40	ralrimivva 2814	. . . . . . . . . . . . . . 15 |- ( ph -> A. f e. V A. g e. V ( f E g ) e. ( RR* \ { -oo } ) )
42		ffnov 6419	. . . . . . . . . . . . . . 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 677	. . . . . . . . . . . . . 14 |- ( ph -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
44	43	ad2antrr 740	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> ( RR* \ { -oo } ) )
45		ssrab2 3500	. . . . . . . . . . . . . . . . 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 3448	. . . . . . . . . . . . . . . 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 3418	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g e. ( ( V X. V ) ^m ( 1 ... n ) ) )
49		elmapi 7511	. . . . . . . . . . . . . 14 |- ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
50	48, 49	syl 17	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> g : ( 1 ... n ) --> ( V X. V ) )
51		fco 5751	. . . . . . . . . . . . 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 673	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
53		0re 9661	. . . . . . . . . . . . 13 |- 0 e. RR
54		rexr 9704	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 e. RR* )
55		renemnf 9707	. . . . . . . . . . . . . 14 |- ( 0 e. RR -> 0 =/= -oo )
56		eldifsn 4088	. . . . . . . . . . . . . 14 |- ( 0 e. ( RR* \ { -oo } ) <-> ( 0 e. RR* /\ 0 =/= -oo ) )
57	54, 55, 56	sylanbrc 677	. . . . . . . . . . . . 13 |- ( 0 e. RR -> 0 e. ( RR* \ { -oo } ) )
58	53, 57	mp1i 13	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. ( RR* \ { -oo } ) )
59		xaddid2 11557	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( 0 +e x ) = x )
60		xaddid1 11556	. . . . . . . . . . . . . 14 |- ( x e. RR* -> ( x +e 0 ) = x )
61	59, 60	jca 541	. . . . . . . . . . . . 13 |- ( x e. RR* -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
62	61	adantl 473	. . . . . . . . . . . 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 16597	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) = ( W gsumg ( E o. g ) ) )
64	23, 21	ressbas2 15258	. . . . . . . . . . . . 13 |- ( ( RR* \ { -oo } ) C_ RR* -> ( RR* \ { -oo } ) = ( Base ` W ) )
65	27, 64	ax-mp 5	. . . . . . . . . . . 12 |- ( RR* \ { -oo } ) = ( Base ` W )
66	23	xrs10 19084	. . . . . . . . . . . 12 |- 0 = ( 0g ` W )
67	23	xrs1cmn 19085	. . . . . . . . . . . . 13 |- W e. CMnd
68	67	a1i 11	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. CMnd )
69		c0ex 9655	. . . . . . . . . . . . . 14 |- 0 e. _V
70	69	a1i 11	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 0 e. _V )
71	52, 26, 70	fdmfifsupp 7911	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) finSupp 0 )
72	65, 66, 68, 26, 52, 71	gsumcl 17627	. . . . . . . . . . 11 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
73	63, 72	eqeltrd 2549	. . . . . . . . . 10 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. ( RR* \ { -oo } ) )
74	73	eldifad 3402	. . . . . . . . 9 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( RR*s gsumg ( E o. g ) ) e. RR* )
75		eqid 2471	. . . . . . . . 9 |- ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) = ( g e. S |-> ( RR*s gsumg ( E o. g ) ) )
76	74, 75	fmptd 6061	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* )
77		frn 5747	. . . . . . . 8 |- ( ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) : S --> RR* -> ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
78	76, 77	syl 17	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
79	78	ralrimiva 2809	. . . . . 6 |- ( ph -> A. n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
80		iunss 4310	. . . . . 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 217	. . . . 5 |- ( ph -> U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) C_ RR* )
82	18, 81	syl5eqss 3462	. . . 4 |- ( ph -> T C_ RR* )
83		infxrcl 11644	. . . 4 |- ( T C_ RR* -> inf ( T , RR* , < ) e. RR* )
84	82, 83	syl 17	. . 3 |- ( ph -> inf ( T , RR* , < ) e. RR* )
85		xmetcl 21424	. . . 4 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> ( X E Y ) e. RR* )
86	29, 11, 13, 85	syl3anc 1292	. . 3 |- ( ph -> ( X E Y ) e. RR* )
87		1nn 10642	. . . . . . 7 |- 1 e. NN
88		1ex 9656	. . . . . . . . . . . 12 |- 1 e. _V
89		opex 4664	. . . . . . . . . . . 12 |- <. X , Y >. e. _V
90	88, 89	f1osn 5866	. . . . . . . . . . 11 |- { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. }
91		f1of 5828	. . . . . . . . . . 11 |- ( { <. 1 , <. X , Y >. >. } : { 1 } -1-1-onto-> { <. X , Y >. } -> { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } )
92	90, 91	ax-mp 5	. . . . . . . . . 10 |- { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. }
93		opelxpi 4871	. . . . . . . . . . . 12 |- ( ( X e. V /\ Y e. V ) -> <. X , Y >. e. ( V X. V ) )
94	11, 13, 93	syl2anc 673	. . . . . . . . . . 11 |- ( ph -> <. X , Y >. e. ( V X. V ) )
95	94	snssd 4108	. . . . . . . . . 10 |- ( ph -> { <. X , Y >. } C_ ( V X. V ) )
96		fss 5749	. . . . . . . . . 10 |- ( ( { <. 1 , <. X , Y >. >. } : { 1 } --> { <. X , Y >. } /\ { <. X , Y >. } C_ ( V X. V ) ) -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
97	92, 95, 96	sylancr 676	. . . . . . . . 9 |- ( ph -> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) )
98	29	elfvexd 5907	. . . . . . . . . . 11 |- ( ph -> V e. _V )
99		xpexg 6612	. . . . . . . . . . 11 |- ( ( V e. _V /\ V e. _V ) -> ( V X. V ) e. _V )
100	98, 98, 99	syl2anc 673	. . . . . . . . . 10 |- ( ph -> ( V X. V ) e. _V )
101		snex 4641	. . . . . . . . . 10 |- { 1 } e. _V
102		elmapg 7503	. . . . . . . . . 10 |- ( ( ( V X. V ) e. _V /\ { 1 } e. _V ) -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
103	100, 101, 102	sylancl 675	. . . . . . . . 9 |- ( ph -> ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) <-> { <. 1 , <. X , Y >. >. } : { 1 } --> ( V X. V ) ) )
104	97, 103	mpbird 240	. . . . . . . 8 |- ( ph -> { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) )
105		op1stg 6824	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 1st ` <. X , Y >. ) = X )
106	11, 13, 105	syl2anc 673	. . . . . . . . . 10 |- ( ph -> ( 1st ` <. X , Y >. ) = X )
107	106	fveq2d 5883	. . . . . . . . 9 |- ( ph -> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) )
108		op2ndg 6825	. . . . . . . . . . 11 |- ( ( X e. V /\ Y e. V ) -> ( 2nd ` <. X , Y >. ) = Y )
109	11, 13, 108	syl2anc 673	. . . . . . . . . 10 |- ( ph -> ( 2nd ` <. X , Y >. ) = Y )
110	109	fveq2d 5883	. . . . . . . . 9 |- ( ph -> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) )
111	107, 110	jca 541	. . . . . . . 8 |- ( ph -> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
112	24	a1i 11	. . . . . . . . . 10 |- ( ph -> RR*s e. _V )
113		snfi 7668	. . . . . . . . . . 11 |- { 1 } e. Fin
114	113	a1i 11	. . . . . . . . . 10 |- ( ph -> { 1 } e. Fin )
115	27	a1i 11	. . . . . . . . . 10 |- ( ph -> ( RR* \ { -oo } ) C_ RR* )
116		xmetge0 21437	. . . . . . . . . . . . . . 15 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ Y e. V ) -> 0 <_ ( X E Y ) )
117	29, 11, 13, 116	syl3anc 1292	. . . . . . . . . . . . . 14 |- ( ph -> 0 <_ ( X E Y ) )
118		ge0nemnf 11491	. . . . . . . . . . . . . 14 |- ( ( ( X E Y ) e. RR* /\ 0 <_ ( X E Y ) ) -> ( X E Y ) =/= -oo )
119	86, 117, 118	syl2anc 673	. . . . . . . . . . . . 13 |- ( ph -> ( X E Y ) =/= -oo )
120		eldifsn 4088	. . . . . . . . . . . . 13 |- ( ( X E Y ) e. ( RR* \ { -oo } ) <-> ( ( X E Y ) e. RR* /\ ( X E Y ) =/= -oo ) )
121	86, 119, 120	sylanbrc 677	. . . . . . . . . . . 12 |- ( ph -> ( X E Y ) e. ( RR* \ { -oo } ) )
122		fconst6g 5785	. . . . . . . . . . . 12 |- ( ( X E Y ) e. ( RR* \ { -oo } ) -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
123	121, 122	syl 17	. . . . . . . . . . 11 |- ( ph -> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) )
124		fcoconst 6076	. . . . . . . . . . . . . 14 |- ( ( E Fn ( V X. V ) /\ <. X , Y >. e. ( V X. V ) ) -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
125	32, 94, 124	syl2anc 673	. . . . . . . . . . . . 13 |- ( ph -> ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( { 1 } X. { ( E ` <. X , Y >. ) } ) )
126	88, 89	xpsn 6082	. . . . . . . . . . . . . 14 |- ( { 1 } X. { <. X , Y >. } ) = { <. 1 , <. X , Y >. >. }
127	126	coeq2i 5000	. . . . . . . . . . . . 13 |- ( E o. ( { 1 } X. { <. X , Y >. } ) ) = ( E o. { <. 1 , <. X , Y >. >. } )
128		df-ov 6311	. . . . . . . . . . . . . . . 16 |- ( X E Y ) = ( E ` <. X , Y >. )
129	128	eqcomi 2480	. . . . . . . . . . . . . . 15 |- ( E ` <. X , Y >. ) = ( X E Y )
130	129	sneqi 3970	. . . . . . . . . . . . . 14 |- { ( E ` <. X , Y >. ) } = { ( X E Y ) }
131	130	xpeq2i 4860	. . . . . . . . . . . . 13 |- ( { 1 } X. { ( E ` <. X , Y >. ) } ) = ( { 1 } X. { ( X E Y ) } )
132	125, 127, 131	3eqtr3g 2528	. . . . . . . . . . . 12 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( { 1 } X. { ( X E Y ) } ) )
133	132	feq1d 5724	. . . . . . . . . . 11 |- ( ph -> ( ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) <-> ( { 1 } X. { ( X E Y ) } ) : { 1 } --> ( RR* \ { -oo } ) ) )
134	123, 133	mpbird 240	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) : { 1 } --> ( RR* \ { -oo } ) )
135	53, 57	mp1i 13	. . . . . . . . . 10 |- ( ph -> 0 e. ( RR* \ { -oo } ) )
136	61	adantl 473	. . . . . . . . . 10 |- ( ( ph /\ x e. RR* ) -> ( ( 0 +e x ) = x /\ ( x +e 0 ) = x ) )
137	21, 22, 23, 112, 114, 115, 134, 135, 136	gsumress 16597	. . . . . . . . 9 |- ( ph -> ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
138		fconstmpt 4883	. . . . . . . . . . 11 |- ( { 1 } X. { ( X E Y ) } ) = ( j e. { 1 } |-> ( X E Y ) )
139	132, 138	syl6eq 2521	. . . . . . . . . 10 |- ( ph -> ( E o. { <. 1 , <. X , Y >. >. } ) = ( j e. { 1 } |-> ( X E Y ) ) )
140	139	oveq2d 6324	. . . . . . . . 9 |- ( ph -> ( W gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) = ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) )
141		cmnmnd 17523	. . . . . . . . . . 11 |- ( W e. CMnd -> W e. Mnd )
142	67, 141	mp1i 13	. . . . . . . . . 10 |- ( ph -> W e. Mnd )
143	87	a1i 11	. . . . . . . . . 10 |- ( ph -> 1 e. NN )
144		eqidd 2472	. . . . . . . . . . 11 |- ( j = 1 -> ( X E Y ) = ( X E Y ) )
145	65, 144	gsumsn 17665	. . . . . . . . . 10 |- ( ( W e. Mnd /\ 1 e. NN /\ ( X E Y ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
146	142, 143, 121, 145	syl3anc 1292	. . . . . . . . 9 |- ( ph -> ( W gsumg ( j e. { 1 } |-> ( X E Y ) ) ) = ( X E Y ) )
147	137, 140, 146	3eqtrrd 2510	. . . . . . . 8 |- ( ph -> ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
148		fveq1 5878	. . . . . . . . . . . . . . 15 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = ( { <. 1 , <. X , Y >. >. } ` 1 ) )
149	88, 89	fvsn 6113	. . . . . . . . . . . . . . 15 |- ( { <. 1 , <. X , Y >. >. } ` 1 ) = <. X , Y >.
150	148, 149	syl6eq 2521	. . . . . . . . . . . . . 14 |- ( g = { <. 1 , <. X , Y >. >. } -> ( g ` 1 ) = <. X , Y >. )
151	150	fveq2d 5883	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 1st ` ( g ` 1 ) ) = ( 1st ` <. X , Y >. ) )
152	151	fveq2d 5883	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` ( 1st ` <. X , Y >. ) ) )
153	152	eqeq1d 2473	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) ) )
154	150	fveq2d 5883	. . . . . . . . . . . . 13 |- ( g = { <. 1 , <. X , Y >. >. } -> ( 2nd ` ( g ` 1 ) ) = ( 2nd ` <. X , Y >. ) )
155	154	fveq2d 5883	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` ( 2nd ` <. X , Y >. ) ) )
156	155	eqeq1d 2473	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) )
157	153, 156	anbi12d 725	. . . . . . . . . 10 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) <-> ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) ) )
158		coeq2 4998	. . . . . . . . . . . 12 |- ( g = { <. 1 , <. X , Y >. >. } -> ( E o. g ) = ( E o. { <. 1 , <. X , Y >. >. } ) )
159	158	oveq2d 6324	. . . . . . . . . . 11 |- ( g = { <. 1 , <. X , Y >. >. } -> ( RR*s gsumg ( E o. g ) ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) )
160	159	eqeq2d 2481	. . . . . . . . . 10 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) ) )
161	157, 160	anbi12d 725	. . . . . . . . 9 |- ( g = { <. 1 , <. X , Y >. >. } -> ( ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) <-> ( ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) ) ) )
162	161	rspcev 3136	. . . . . . . 8 |- ( ( { <. 1 , <. X , Y >. >. } e. ( ( V X. V ) ^m { 1 } ) /\ ( ( ( F ` ( 1st ` <. X , Y >. ) ) = ( F ` X ) /\ ( F ` ( 2nd ` <. X , Y >. ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. { <. 1 , <. X , Y >. >. } ) ) ) ) -> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
163	104, 111, 147, 162	syl12anc 1290	. . . . . . 7 |- ( ph -> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
164		ovex 6336	. . . . . . . . . 10 |- ( X E Y ) e. _V
165	75	elrnmpt 5087	. . . . . . . . . 10 |- ( ( X E Y ) e. _V -> ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
166	164, 165	ax-mp 5	. . . . . . . . 9 |- ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) )
167	15	rexeqi 2978	. . . . . . . . . . 11 |- ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } ( X E Y ) = ( RR*s gsumg ( E o. g ) ) )
168		fveq1 5878	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` 1 ) = ( g ` 1 ) )
169	168	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 1st ` ( h ` 1 ) ) = ( 1st ` ( g ` 1 ) ) )
170	169	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` ( 1st ` ( g ` 1 ) ) ) )
171	170	eqeq1d 2473	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) <-> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) ) )
172		fveq1 5878	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( h ` n ) = ( g ` n ) )
173	172	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( h = g -> ( 2nd ` ( h ` n ) ) = ( 2nd ` ( g ` n ) ) )
174	173	fveq2d 5883	. . . . . . . . . . . . . 14 |- ( h = g -> ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` ( 2nd ` ( g ` n ) ) ) )
175	174	eqeq1d 2473	. . . . . . . . . . . . 13 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) )
176		fveq1 5878	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` i ) = ( g ` i ) )
177	176	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 2nd ` ( h ` i ) ) = ( 2nd ` ( g ` i ) ) )
178	177	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 2nd ` ( g ` i ) ) ) )
179		fveq1 5878	. . . . . . . . . . . . . . . . 17 |- ( h = g -> ( h ` ( i + 1 ) ) = ( g ` ( i + 1 ) ) )
180	179	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( h = g -> ( 1st ` ( h ` ( i + 1 ) ) ) = ( 1st ` ( g ` ( i + 1 ) ) ) )
181	180	fveq2d 5883	. . . . . . . . . . . . . . 15 |- ( h = g -> ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
182	178, 181	eqeq12d 2486	. . . . . . . . . . . . . 14 |- ( h = g -> ( ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
183	182	ralbidv 2829	. . . . . . . . . . . . 13 |- ( h = g -> ( A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) <-> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
184	171, 175, 183	3anbi123d 1365	. . . . . . . . . . . 12 |- ( h = g -> ( ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) ) )
185	184	rexrab 3190	. . . . . . . . . . 11 |- ( E. g e. { h e. ( ( V X. V ) ^m ( 1 ... n ) ) | ( ( F ` ( 1st ` ( h ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( h ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( h ` i ) ) ) = ( F ` ( 1st ` ( h ` ( i + 1 ) ) ) ) ) } ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. ( ( V X. V ) ^m ( 1 ... n ) ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
186	167, 185	bitri 257	. . . . . . . . . 10 |- ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. ( ( V X. V ) ^m ( 1 ... n ) ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) )
187		oveq2 6316	. . . . . . . . . . . . 13 |- ( n = 1 -> ( 1 ... n ) = ( 1 ... 1 ) )
188		1z 10991	. . . . . . . . . . . . . 14 |- 1 e. ZZ
189		fzsn 11866	. . . . . . . . . . . . . 14 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
190	188, 189	ax-mp 5	. . . . . . . . . . . . 13 |- ( 1 ... 1 ) = { 1 }
191	187, 190	syl6eq 2521	. . . . . . . . . . . 12 |- ( n = 1 -> ( 1 ... n ) = { 1 } )
192	191	oveq2d 6324	. . . . . . . . . . 11 |- ( n = 1 -> ( ( V X. V ) ^m ( 1 ... n ) ) = ( ( V X. V ) ^m { 1 } ) )
193		df-3an 1009	. . . . . . . . . . . . 13 |- ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
194		ral0 3865	. . . . . . . . . . . . . . . 16 |- A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) )
195		oveq1 6315	. . . . . . . . . . . . . . . . . . . 20 |- ( n = 1 -> ( n - 1 ) = ( 1 - 1 ) )
196		1m1e0 10700	. . . . . . . . . . . . . . . . . . . 20 |- ( 1 - 1 ) = 0
197	195, 196	syl6eq 2521	. . . . . . . . . . . . . . . . . . 19 |- ( n = 1 -> ( n - 1 ) = 0 )
198	197	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = ( 1 ... 0 ) )
199		fz10 11846	. . . . . . . . . . . . . . . . . 18 |- ( 1 ... 0 ) = (/)
200	198, 199	syl6eq 2521	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 1 ... ( n - 1 ) ) = (/) )
201	200	raleqdv 2979	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) <-> A. i e. (/) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
202	194, 201	mpbiri 241	. . . . . . . . . . . . . . 15 |- ( n = 1 -> A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) )
203	202	biantrud 515	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) ) )
204		fveq2 5879	. . . . . . . . . . . . . . . . . 18 |- ( n = 1 -> ( g ` n ) = ( g ` 1 ) )
205	204	fveq2d 5883	. . . . . . . . . . . . . . . . 17 |- ( n = 1 -> ( 2nd ` ( g ` n ) ) = ( 2nd ` ( g ` 1 ) ) )
206	205	fveq2d 5883	. . . . . . . . . . . . . . . 16 |- ( n = 1 -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` ( 2nd ` ( g ` 1 ) ) ) )
207	206	eqeq1d 2473	. . . . . . . . . . . . . . 15 |- ( n = 1 -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) )
208	207	anbi2d 718	. . . . . . . . . . . . . 14 |- ( n = 1 -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) ) )
209	203, 208	bitr3d 263	. . . . . . . . . . . . 13 |- ( n = 1 -> ( ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) ) )
210	193, 209	syl5bb 265	. . . . . . . . . . . 12 |- ( n = 1 -> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) <-> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) ) )
211	210	anbi1d 719	. . . . . . . . . . 11 |- ( n = 1 -> ( ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) <-> ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
212	192, 211	rexeqbidv 2988	. . . . . . . . . 10 |- ( n = 1 -> ( E. g e. ( ( V X. V ) ^m ( 1 ... n ) ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
213	186, 212	syl5bb 265	. . . . . . . . 9 |- ( n = 1 -> ( E. g e. S ( X E Y ) = ( RR*s gsumg ( E o. g ) ) <-> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
214	166, 213	syl5bb 265	. . . . . . . 8 |- ( n = 1 -> ( ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) )
215	214	rspcev 3136	. . . . . . 7 |- ( ( 1 e. NN /\ E. g e. ( ( V X. V ) ^m { 1 } ) ( ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` 1 ) ) ) = ( F ` Y ) ) /\ ( X E Y ) = ( RR*s gsumg ( E o. g ) ) ) ) -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
216	87, 163, 215	sylancr 676	. . . . . 6 |- ( ph -> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
217		eliun 4274	. . . . . 6 |- ( ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. n e. NN ( X E Y ) e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
218	216, 217	sylibr 217	. . . . 5 |- ( ph -> ( X E Y ) e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
219	218, 18	syl6eleqr 2560	. . . 4 |- ( ph -> ( X E Y ) e. T )
220		infxrlb 11645	. . . 4 |- ( ( T C_ RR* /\ ( X E Y ) e. T ) -> inf ( T , RR* , < ) <_ ( X E Y ) )
221	82, 219, 220	syl2anc 673	. . 3 |- ( ph -> inf ( T , RR* , < ) <_ ( X E Y ) )
222	18	eleq2i 2541	. . . . . . 7 |- ( p e. T <-> p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
223		eliun 4274	. . . . . . 7 |- ( p e. U_ n e. NN ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
224	222, 223	bitri 257	. . . . . 6 |- ( p e. T <-> E. n e. NN p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) )
225		vex 3034	. . . . . . . . 9 |- p e. _V
226	75	elrnmpt 5087	. . . . . . . . 9 |- ( p e. _V -> ( p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. S p = ( RR*s gsumg ( E o. g ) ) ) )
227	225, 226	ax-mp 5	. . . . . . . 8 |- ( p e. ran ( g e. S |-> ( RR*s gsumg ( E o. g ) ) ) <-> E. g e. S p = ( RR*s gsumg ( E o. g ) ) )
228	184, 15	elrab2 3186	. . . . . . . . . . . . . . . . 17 |- ( g e. S <-> ( g e. ( ( V X. V ) ^m ( 1 ... n ) ) /\ ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) ) )
229	228	simprbi 471	. . . . . . . . . . . . . . . 16 |- ( g e. S -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
230	229	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) /\ ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) /\ A. i e. ( 1 ... ( n - 1 ) ) ( F ` ( 2nd ` ( g ` i ) ) ) = ( F ` ( 1st ` ( g ` ( i + 1 ) ) ) ) ) )
231	230	simp2d 1043	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) )
232	3	ad2antrr 740	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-onto-> B )
233		f1of1 5827	. . . . . . . . . . . . . . . 16 |- ( F : V -1-1-onto-> B -> F : V -1-1-> B )
234	232, 233	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> F : V -1-1-> B )
235		simplr 770	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. NN )
236		elfz1end 11855	. . . . . . . . . . . . . . . . . 18 |- ( n e. NN <-> n e. ( 1 ... n ) )
237	235, 236	sylib 201	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( 1 ... n ) )
238	50, 237	ffvelrnd 6038	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` n ) e. ( V X. V ) )
239		xp2nd 6843	. . . . . . . . . . . . . . . 16 |- ( ( g ` n ) e. ( V X. V ) -> ( 2nd ` ( g ` n ) ) e. V )
240	238, 239	syl 17	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) e. V )
241	13	ad2antrr 740	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> Y e. V )
242		f1fveq 6181	. . . . . . . . . . . . . . 15 |- ( ( F : V -1-1-> B /\ ( ( 2nd ` ( g ` n ) ) e. V /\ Y e. V ) ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
243	234, 240, 241, 242	syl12anc 1290	. . . . . . . . . . . . . 14 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 2nd ` ( g ` n ) ) ) = ( F ` Y ) <-> ( 2nd ` ( g ` n ) ) = Y ) )
244	231, 243	mpbid 215	. . . . . . . . . . . . 13 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` n ) ) = Y )
245	244	oveq2d 6324	. . . . . . . . . . . 12 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` n ) ) ) = ( X E Y ) )
246		eleq1 2537	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( m e. ( 1 ... n ) <-> 1 e. ( 1 ... n ) ) )
247		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( g ` m ) = ( g ` 1 ) )
248	247	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` 1 ) ) )
249	248	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
250		oveq2 6316	. . . . . . . . . . . . . . . . . . . . 21 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
251	250, 190	syl6eq 2521	. . . . . . . . . . . . . . . . . . . 20 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
252	251	reseq2d 5111	. . . . . . . . . . . . . . . . . . 19 |- ( m = 1 -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` { 1 } ) )
253	252	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = 1 -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
254	249, 253	breq12d 4408	. . . . . . . . . . . . . . . . 17 |- ( m = 1 -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) )
255	246, 254	imbi12d 327	. . . . . . . . . . . . . . . 16 |- ( m = 1 -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) ) )
256	255	imbi2d 323	. . . . . . . . . . . . . . 15 |- ( m = 1 -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) ) ) )
257		eleq1 2537	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( m e. ( 1 ... n ) <-> x e. ( 1 ... n ) ) )
258		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( g ` m ) = ( g ` x ) )
259	258	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` x ) ) )
260	259	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` x ) ) ) )
261		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20 |- ( m = x -> ( 1 ... m ) = ( 1 ... x ) )
262	261	reseq2d 5111	. . . . . . . . . . . . . . . . . . 19 |- ( m = x -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... x ) ) )
263	262	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = x -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) )
264	260, 263	breq12d 4408	. . . . . . . . . . . . . . . . 17 |- ( m = x -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) )
265	257, 264	imbi12d 327	. . . . . . . . . . . . . . . 16 |- ( m = x -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
266	265	imbi2d 323	. . . . . . . . . . . . . . 15 |- ( m = x -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) ) )
267		eleq1 2537	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( m e. ( 1 ... n ) <-> ( x + 1 ) e. ( 1 ... n ) ) )
268		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( g ` m ) = ( g ` ( x + 1 ) ) )
269	268	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` ( x + 1 ) ) ) )
270	269	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) )
271		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20 |- ( m = ( x + 1 ) -> ( 1 ... m ) = ( 1 ... ( x + 1 ) ) )
272	271	reseq2d 5111	. . . . . . . . . . . . . . . . . . 19 |- ( m = ( x + 1 ) -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) )
273	272	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = ( x + 1 ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) )
274	270, 273	breq12d 4408	. . . . . . . . . . . . . . . . 17 |- ( m = ( x + 1 ) -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) )
275	267, 274	imbi12d 327	. . . . . . . . . . . . . . . 16 |- ( m = ( x + 1 ) -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) )
276	275	imbi2d 323	. . . . . . . . . . . . . . 15 |- ( m = ( x + 1 ) -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... ( x + 1 ) ) ) ) ) ) ) )
277		eleq1 2537	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( m e. ( 1 ... n ) <-> n e. ( 1 ... n ) ) )
278		fveq2 5879	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( g ` m ) = ( g ` n ) )
279	278	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( 2nd ` ( g ` m ) ) = ( 2nd ` ( g ` n ) ) )
280	279	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( X E ( 2nd ` ( g ` m ) ) ) = ( X E ( 2nd ` ( g ` n ) ) ) )
281		oveq2 6316	. . . . . . . . . . . . . . . . . . . 20 |- ( m = n -> ( 1 ... m ) = ( 1 ... n ) )
282	281	reseq2d 5111	. . . . . . . . . . . . . . . . . . 19 |- ( m = n -> ( ( E o. g ) |` ( 1 ... m ) ) = ( ( E o. g ) |` ( 1 ... n ) ) )
283	282	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( m = n -> ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) = ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) )
284	280, 283	breq12d 4408	. . . . . . . . . . . . . . . . 17 |- ( m = n -> ( ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) <-> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) )
285	277, 284	imbi12d 327	. . . . . . . . . . . . . . . 16 |- ( m = n -> ( ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) <-> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) )
286	285	imbi2d 323	. . . . . . . . . . . . . . 15 |- ( m = n -> ( ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( m e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` m ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... m ) ) ) ) ) <-> ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( n e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` n ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... n ) ) ) ) ) ) )
287	29	ad2antrr 740	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E e. ( *Met ` V ) )
288	11	ad2antrr 740	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> X e. V )
289		nnuz 11218	. . . . . . . . . . . . . . . . . . . . . . 23 |- NN = ( ZZ>= ` 1 )
290	235, 289	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> n e. ( ZZ>= ` 1 ) )
291		eluzfz1 11832	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... n ) )
292	290, 291	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. ( 1 ... n ) )
293	50, 292	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) e. ( V X. V ) )
294		xp2nd 6843	. . . . . . . . . . . . . . . . . . . 20 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 2nd ` ( g ` 1 ) ) e. V )
295	293, 294	syl 17	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 2nd ` ( g ` 1 ) ) e. V )
296		xmetcl 21424	. . . . . . . . . . . . . . . . . . 19 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` 1 ) ) e. V ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
297	287, 288, 295, 296	syl3anc 1292	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* )
298		xrleid 11472	. . . . . . . . . . . . . . . . . 18 |- ( ( X E ( 2nd ` ( g ` 1 ) ) ) e. RR* -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
299	297, 298	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( X E ( 2nd ` ( g ` 1 ) ) ) )
300	142	ad2antrr 740	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> W e. Mnd )
301	87	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> 1 e. NN )
302	44, 293	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) )
303		fveq2 5879	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = 1 -> ( g ` j ) = ( g ` 1 ) )
304	303	fveq2d 5883	. . . . . . . . . . . . . . . . . . . 20 |- ( j = 1 -> ( E ` ( g ` j ) ) = ( E ` ( g ` 1 ) ) )
305	65, 304	gsumsn 17665	. . . . . . . . . . . . . . . . . . 19 |- ( ( W e. Mnd /\ 1 e. NN /\ ( E ` ( g ` 1 ) ) e. ( RR* \ { -oo } ) ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
306	300, 301, 302, 305	syl3anc 1292	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) = ( E ` ( g ` 1 ) ) )
307	287, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> E : ( V X. V ) --> RR* )
308		fcompt 6075	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( E : ( V X. V ) --> RR* /\ g : ( 1 ... n ) --> ( V X. V ) ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
309	307, 50, 308	syl2anc 673	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E o. g ) = ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) )
310	309	reseq1d 5110	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) )
311	292	snssd 4108	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> { 1 } C_ ( 1 ... n ) )
312	311	resmptd 5162	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( j e. ( 1 ... n ) |-> ( E ` ( g ` j ) ) ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
313	310, 312	eqtrd 2505	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( E o. g ) |` { 1 } ) = ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) )
314	313	oveq2d 6324	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( W gsumg ( j e. { 1 } |-> ( E ` ( g ` j ) ) ) ) )
315		df-ov 6311	. . . . . . . . . . . . . . . . . . 19 |- ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. )
316		1st2nd2 6849	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( g ` 1 ) e. ( V X. V ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
317	293, 316	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( g ` 1 ) = <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. )
318	230	simp1d 1042	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) )
319		xp1st 6842	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` 1 ) e. ( V X. V ) -> ( 1st ` ( g ` 1 ) ) e. V )
320	293, 319	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) e. V )
321		f1fveq 6181	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( F : V -1-1-> B /\ ( ( 1st ` ( g ` 1 ) ) e. V /\ X e. V ) ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
322	234, 320, 288, 321	syl12anc 1290	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( ( F ` ( 1st ` ( g ` 1 ) ) ) = ( F ` X ) <-> ( 1st ` ( g ` 1 ) ) = X ) )
323	318, 322	mpbid 215	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1st ` ( g ` 1 ) ) = X )
324	323	opeq1d 4164	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. ( 1st ` ( g ` 1 ) ) , ( 2nd ` ( g ` 1 ) ) >. = <. X , ( 2nd ` ( g ` 1 ) ) >. )
325	317, 324	eqtr2d 2506	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> <. X , ( 2nd ` ( g ` 1 ) ) >. = ( g ` 1 ) )
326	325	fveq2d 5883	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( E ` <. X , ( 2nd ` ( g ` 1 ) ) >. ) = ( E ` ( g ` 1 ) ) )
327	315, 326	syl5eq 2517	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) = ( E ` ( g ` 1 ) ) )
328	306, 314, 327	3eqtr4d 2515	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( W gsumg ( ( E o. g ) |` { 1 } ) ) = ( X E ( 2nd ` ( g ` 1 ) ) ) )
329	299, 328	breqtrrd 4422	. . . . . . . . . . . . . . . 16 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) )
330	329	a1d 25	. . . . . . . . . . . . . . 15 |- ( ( ( ph /\ n e. NN ) /\ g e. S ) -> ( 1 e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` 1 ) ) ) <_ ( W gsumg ( ( E o. g ) |` { 1 } ) ) ) )
331		simprl 772	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. NN )
332	331, 289	syl6eleq 2559	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( ZZ>= ` 1 ) )
333		simprr 774	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( x + 1 ) e. ( 1 ... n ) )
334		peano2fzr 11838	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x e. ( ZZ>= ` 1 ) /\ ( x + 1 ) e. ( 1 ... n ) ) -> x e. ( 1 ... n ) )
335	332, 333, 334	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ( 1 ... n ) )
336	335	expr 626	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x + 1 ) e. ( 1 ... n ) -> x e. ( 1 ... n ) ) )
337	336	imim1d 77	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ x e. NN ) -> ( ( x e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) -> ( ( x + 1 ) e. ( 1 ... n ) -> ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) ) )
338	287	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E e. ( *Met ` V ) )
339	288	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> X e. V )
340	50	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> g : ( 1 ... n ) --> ( V X. V ) )
341	340, 335	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` x ) e. ( V X. V ) )
342		xp2nd 6843	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( g ` x ) e. ( V X. V ) -> ( 2nd ` ( g ` x ) ) e. V )
343	341, 342	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` x ) ) e. V )
344		xmetcl 21424	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( E e. ( *Met ` V ) /\ X e. V /\ ( 2nd ` ( g ` x ) ) e. V ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
345	338, 339, 343, 344	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` x ) ) ) e. RR* )
346	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> W e. CMnd )
347		fzfid 12224	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) e. Fin )
348	52	adantr 472	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E o. g ) : ( 1 ... n ) --> ( RR* \ { -oo } ) )
349		fzsuc 11869	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( x e. ( ZZ>= ` 1 ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
350	332, 349	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) = ( ( 1 ... x ) u. { ( x + 1 ) } ) )
351		elfzuz3 11823	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( x + 1 ) e. ( 1 ... n ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
352	351	ad2antll 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> n e. ( ZZ>= ` ( x + 1 ) ) )
353		fzss2 11864	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( n e. ( ZZ>= ` ( x + 1 ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
354	352, 353	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... ( x + 1 ) ) C_ ( 1 ... n ) )
355	350, 354	eqsstr3d 3453	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( 1 ... x ) u. { ( x + 1 ) } ) C_ ( 1 ... n ) )
356	355	unssad 3602	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 1 ... x ) C_ ( 1 ... n ) )
357	348, 356	fssresd 5762	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) : ( 1 ... x ) --> ( RR* \ { -oo } ) )
358	69	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> 0 e. _V )
359	357, 347, 358	fdmfifsupp 7911	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( E o. g ) |` ( 1 ... x ) ) finSupp 0 )
360	65, 66, 346, 347, 357, 359	gsumcl 17627	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) e. ( RR* \ { -oo } ) )
361	360	eldifad 3402	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* )
362	338, 30	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> E : ( V X. V ) --> RR* )
363	340, 333	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) e. ( V X. V ) )
364	362, 363	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( E ` ( g ` ( x + 1 ) ) ) e. RR* )
365		xleadd1a 11564	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( X E ( 2nd ` ( g ` x ) ) ) e. RR* /\ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* /\ ( E ` ( g ` ( x + 1 ) ) ) e. RR* ) /\ ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) )
366	365	ex 441	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( X E ( 2nd ` ( g ` x ) ) ) e. RR* /\ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) e. RR* /\ ( E ` ( g ` ( x + 1 ) ) ) e. RR* ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
367	345, 361, 364, 366	syl3anc 1292	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) <_ ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) -> ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) <_ ( ( W gsumg ( ( E o. g ) |` ( 1 ... x ) ) ) +e ( E ` ( g ` ( x + 1 ) ) ) ) ) )
368		xp2nd 6843	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
369	363, 368	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( 2nd ` ( g ` ( x + 1 ) ) ) e. V )
370		xmettri 21444	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( E e. ( *Met ` V ) /\ ( X e. V /\ ( 2nd ` ( g ` ( x + 1 ) ) ) e. V /\ ( 2nd ` ( g ` x ) ) e. V ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) ) )
371	338, 339, 369, 343, 370	syl13anc 1294	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( X E ( 2nd ` ( g ` ( x + 1 ) ) ) ) <_ ( ( X E ( 2nd ` ( g ` x ) ) ) +e ( ( 2nd ` ( g ` x ) ) E ( 2nd ` ( g ` ( x + 1 ) ) ) ) ) )
372		1st2nd2 6849	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( g ` ( x + 1 ) ) e. ( V X. V ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
373	363, 372	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( g ` ( x + 1 ) ) = <. ( 1st ` ( g ` ( x + 1 ) ) ) , ( 2nd ` ( g ` ( x + 1 ) ) ) >. )
374		nnz 10983	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( x e. NN -> x e. ZZ )
375	374	ad2antrl 742	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> x e. ZZ )
376		eluzp1m1 11206	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x e. ZZ /\ n e. ( ZZ>= ` ( x + 1 ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
377	375, 352, 376	syl2anc 673	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ n e. NN ) /\ g e. S ) /\ ( x e. NN /\ ( x + 1 ) e. ( 1 ... n ) ) ) -> ( n - 1 ) e. ( ZZ>= ` x ) )
378		elfzuzb 11820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( x e. ( 1 ... ( n - 1 ) ) <-> ( x e. ( ZZ>= ` 1 ) /\ ( n - 1 ) e. ( ZZ>= ` x ) ) )
379	332, 377, 378