Theorem hoidmvlelem3 38429

Description: This is the contradiction proven in step (d) in the proof of Lemma 115B of [Fremlin1] p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020.)

Hypotheses

Ref	Expression
hoidmvlelem3.l	|- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
hoidmvlelem3.x	|- ( ph -> X e. Fin )
hoidmvlelem3.y	|- ( ph -> Y C_ X )
hoidmvlelem3.z	|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem3.w	|- W = ( Y u. { Z } )
hoidmvlelem3.a	|- ( ph -> A : W --> RR )
hoidmvlelem3.b	|- ( ph -> B : W --> RR )
hoidmvlelem3.lt	|- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
hoidmvlelem3.f	|- F = ( y e. Y |-> 0 )
hoidmvlelem3.c	|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem3.j	|- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
hoidmvlelem3.d	|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem3.k	|- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
hoidmvlelem3.r	|- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
hoidmvlelem3.h	|- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) )
hoidmvlelem3.g	|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
hoidmvlelem3.e	|- ( ph -> E e. RR+ )
hoidmvlelem3.u	|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
hoidmvlelem3.s	|- ( ph -> S e. U )
hoidmvlelem3.sb	|- ( ph -> S < ( B ` Z ) )
hoidmvlelem3.p	|- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
hoidmvlelem3.i	|- ( ph -> A. e e. ( RR ^m Y ) A. f e. ( RR ^m Y ) A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` Y ) f ) <_ (Σ^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
hoidmvlelem3.i2	|- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
hoidmvlelem3.o	|- O = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )

Assertion

Ref	Expression
hoidmvlelem3	|- ( ph -> E. u e. U S < u )

Distinct variable groups:   A, a, b, h, j, k, x   A, e, f, g, h, j, k   z, A, h, j   B, a, b, h, j, k, x, y   B, c, h, j, k, x   B, f, g   u, B, h, j   z, B   C, a, b, h, j, k, x, y   C, c   u, C   z, C   D, a, b, h, j, k, x, y   D, c   u, D   z, D   E, a, b, h, k, x, y   E, c   z, E   j, F   G, a, b, h, k, x, y   G, c   z, G   H, a, b, j, k   z, H   J, a, b, h, j, k, x   g, J   K, a, b, h, j, k, x   L, a, b, h, j, k, x   e, L, f, g   z, L   j, O, k   P, a, b, h, j, k, x, y   P, c   S, a, b, h, j, k, x, y   S, c   u, S   z, S   u, U   W, a, b, j, k, x   W, c   z, W   Y, a, b, h, j, k, x, y   Y, c   e, Y, f, g   Z, a, b, h, j, k, x, y   Z, c   u, Z   z, Z   ph, a, b, h, j, k, x, y   ph, c

Allowed substitution hints:   ph( z, u, e, f, g)   A( y, u, c)   B( e)   C( e, f, g)   D( e, f, g)   P( z, u, e, f, g)   S( e, f, g)   U( x, y, z, e, f, g, h, j, k, a, b, c)   E( u, e, f, g, j)   F( x, y, z, u, e, f, g, h, k, a, b, c)   G( u, e, f, g, j)   H( x, y, u, e, f, g, h, c)   J( y, z, u, e, f, c)   K( y, z, u, e, f, g, c)   L( y, u, c)   O( x, y, z, u, e, f, g, h, a, b, c)   W( y, u, e, f, g, h)   X( x, y, z, u, e, f, g, h, j, k, a, b, c)   Y( z, u)   Z( e, f, g)

Proof of Theorem hoidmvlelem3

Dummy variables i m are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		1nn 10627	. . . . 5 |- 1 e. NN
2	1	a1i 11	. . . 4 |- ( ( ph /\ Y = (/) ) -> 1 e. NN )
3		0le0 10706	. . . . . 6 |- 0 <_ 0
4	3	a1i 11	. . . . 5 |- ( ( ph /\ Y = (/) ) -> 0 <_ 0 )
5		hoidmvlelem3.g	. . . . . . . 8 |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
6	5	a1i 11	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
7		fveq2 5870	. . . . . . . . 9 |- ( Y = (/) -> ( L ` Y ) = ( L ` (/) ) )
8		reseq2 5103	. . . . . . . . . 10 |- ( Y = (/) -> ( A |` Y ) = ( A |` (/) ) )
9		res0 5112	. . . . . . . . . . 11 |- ( A |` (/) ) = (/)
10	9	a1i 11	. . . . . . . . . 10 |- ( Y = (/) -> ( A |` (/) ) = (/) )
11	8, 10	eqtrd 2487	. . . . . . . . 9 |- ( Y = (/) -> ( A |` Y ) = (/) )
12		reseq2 5103	. . . . . . . . . 10 |- ( Y = (/) -> ( B |` Y ) = ( B |` (/) ) )
13		res0 5112	. . . . . . . . . . 11 |- ( B |` (/) ) = (/)
14	13	a1i 11	. . . . . . . . . 10 |- ( Y = (/) -> ( B |` (/) ) = (/) )
15	12, 14	eqtrd 2487	. . . . . . . . 9 |- ( Y = (/) -> ( B |` Y ) = (/) )
16	7, 11, 15	oveq123d 6316	. . . . . . . 8 |- ( Y = (/) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = ( (/) ( L ` (/) ) (/) ) )
17	16	adantl 468	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = ( (/) ( L ` (/) ) (/) ) )
18		hoidmvlelem3.l	. . . . . . . 8 |- L = ( x e. Fin |-> ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) )
19		f0 5769	. . . . . . . . 9 |- (/) : (/) --> RR
20	19	a1i 11	. . . . . . . 8 |- ( ( ph /\ Y = (/) ) -> (/) : (/) --> RR )
21	18, 20, 20	hoidmv0val 38415	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> ( (/) ( L ` (/) ) (/) ) = 0 )
22	6, 17, 21	3eqtrd 2491	. . . . . 6 |- ( ( ph /\ Y = (/) ) -> G = 0 )
23		nfcvd 2595	. . . . . . . . . . 11 |- ( ph -> F/_ j ( P ` 1 ) )
24		nfv 1763	. . . . . . . . . . 11 |- F/ j ph
25		simpr 463	. . . . . . . . . . . 12 |- ( ( ph /\ j = 1 ) -> j = 1 )
26	25	fveq2d 5874	. . . . . . . . . . 11 |- ( ( ph /\ j = 1 ) -> ( P ` j ) = ( P ` 1 ) )
27		1red 9663	. . . . . . . . . . 11 |- ( ph -> 1 e. RR )
28		rge0ssre 11747	. . . . . . . . . . . . 13 |- ( 0 [,) +oo ) C_ RR
29		id 22	. . . . . . . . . . . . . 14 |- ( ph -> ph )
30	1	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> 1 e. NN )
31	1	elexi 3057	. . . . . . . . . . . . . . 15 |- 1 e. _V
32		eleq1 2519	. . . . . . . . . . . . . . . . 17 |- ( j = 1 -> ( j e. NN <-> 1 e. NN ) )
33	32	anbi2d 711	. . . . . . . . . . . . . . . 16 |- ( j = 1 -> ( ( ph /\ j e. NN ) <-> ( ph /\ 1 e. NN ) ) )
34		fveq2 5870	. . . . . . . . . . . . . . . . 17 |- ( j = 1 -> ( P ` j ) = ( P ` 1 ) )
35	34	eleq1d 2515	. . . . . . . . . . . . . . . 16 |- ( j = 1 -> ( ( P ` j ) e. ( 0 [,) +oo ) <-> ( P ` 1 ) e. ( 0 [,) +oo ) ) )
36	33, 35	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) ) <-> ( ( ph /\ 1 e. NN ) -> ( P ` 1 ) e. ( 0 [,) +oo ) ) ) )
37		id 22	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> j e. NN )
38		ovex 6323	. . . . . . . . . . . . . . . . . . 19 |- ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V
39	38	a1i 11	. . . . . . . . . . . . . . . . . 18 |- ( j e. NN -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V )
40		hoidmvlelem3.p	. . . . . . . . . . . . . . . . . . 19 |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
41	40	fvmpt2 5962	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. NN /\ ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
42	37, 39, 41	syl2anc 667	. . . . . . . . . . . . . . . . 17 |- ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
43	42	adantl 468	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
44		hoidmvlelem3.x	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> X e. Fin )
45		hoidmvlelem3.w	. . . . . . . . . . . . . . . . . . . . . 22 |- W = ( Y u. { Z } )
46	45	a1i 11	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> W = ( Y u. { Z } ) )
47		hoidmvlelem3.y	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> Y C_ X )
48		hoidmvlelem3.z	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> Z e. ( X \ Y ) )
49	48	eldifad 3418	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> Z e. X )
50		snssi 4119	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( Z e. X -> { Z } C_ X )
51	49, 50	syl 17	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> { Z } C_ X )
52	47, 51	unssd 3612	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( Y u. { Z } ) C_ X )
53	46, 52	eqsstrd 3468	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> W C_ X )
54	44, 53	ssfid 37424	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> W e. Fin )
55		ssun1 3599	. . . . . . . . . . . . . . . . . . . . 21 |- Y C_ ( Y u. { Z } )
56	45	eqcomi 2462	. . . . . . . . . . . . . . . . . . . . 21 |- ( Y u. { Z } ) = W
57	55, 56	sseqtri 3466	. . . . . . . . . . . . . . . . . . . 20 |- Y C_ W
58	57	a1i 11	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> Y C_ W )
59	54, 58	ssfid 37424	. . . . . . . . . . . . . . . . . 18 |- ( ph -> Y e. Fin )
60	59	adantr 467	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> Y e. Fin )
61		iftrue 3889	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
62	61	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
63		hoidmvlelem3.c	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> C : NN --> ( RR ^m W ) )
64	63	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
65		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
66	64, 65	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
67	55, 45	sseqtr4i 3467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- Y C_ W
68	67	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> Y C_ W )
69	66, 68	fssresd 5755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) : Y --> RR )
70		reex 9635	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- RR e. _V
71	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> RR e. _V )
72	54, 58	ssexd 4553	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> Y e. _V )
73	72	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> Y e. _V )
74	71, 73	elmapd 7491	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) |` Y ) e. ( RR ^m Y ) <-> ( ( C ` j ) |` Y ) : Y --> RR ) )
75	69, 74	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) e. ( RR ^m Y ) )
76	75	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) e. ( RR ^m Y ) )
77	62, 76	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
78		iffalse 3892	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
79	78	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
80		0red 9649	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ y e. Y ) -> 0 e. RR )
81		hoidmvlelem3.f	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F = ( y e. Y |-> 0 )
82	80, 81	fmptd 6051	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> F : Y --> RR )
83	70	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> RR e. _V )
84	83, 59	elmapd 7491	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ph -> ( F e. ( RR ^m Y ) <-> F : Y --> RR ) )
85	82, 84	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ph -> F e. ( RR ^m Y ) )
86	85	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F e. ( RR ^m Y ) )
87	79, 86	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
88	77, 87	pm2.61dan 801	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
89		hoidmvlelem3.j	. . . . . . . . . . . . . . . . . . . 20 |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
90	88, 89	fmptd 6051	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> J : NN --> ( RR ^m Y ) )
91	90	ffvelrnda 6027	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> ( J ` j ) e. ( RR ^m Y ) )
92		elmapi 7498	. . . . . . . . . . . . . . . . . 18 |- ( ( J ` j ) e. ( RR ^m Y ) -> ( J ` j ) : Y --> RR )
93	91, 92	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
94		iftrue 3889	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
95	94	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
96		hoidmvlelem3.d	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> D : NN --> ( RR ^m W ) )
97	96	ffvelrnda 6027	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
98		elmapi 7498	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
99	97, 98	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
100	99, 68	fssresd 5755	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) : Y --> RR )
101	71, 73	elmapd 7491	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( ( ( D ` j ) |` Y ) e. ( RR ^m Y ) <-> ( ( D ` j ) |` Y ) : Y --> RR ) )
102	100, 101	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) e. ( RR ^m Y ) )
103	102	adantr 467	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( D ` j ) |` Y ) e. ( RR ^m Y ) )
104	95, 103	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
105		iffalse 3892	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
106	105	adantl 468	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
107	106, 86	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
108	104, 107	pm2.61dan 801	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
109		hoidmvlelem3.k	. . . . . . . . . . . . . . . . . . . 20 |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
110	108, 109	fmptd 6051	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> K : NN --> ( RR ^m Y ) )
111	110	ffvelrnda 6027	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> ( K ` j ) e. ( RR ^m Y ) )
112		elmapi 7498	. . . . . . . . . . . . . . . . . 18 |- ( ( K ` j ) e. ( RR ^m Y ) -> ( K ` j ) : Y --> RR )
113	111, 112	syl 17	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR )
114	18, 60, 93, 113	hoidmvcl 38414	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. ( 0 [,) +oo ) )
115	43, 114	eqeltrd 2531	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
116	31, 36, 115	vtocl 3102	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 e. NN ) -> ( P ` 1 ) e. ( 0 [,) +oo ) )
117	29, 30, 116	syl2anc 667	. . . . . . . . . . . . 13 |- ( ph -> ( P ` 1 ) e. ( 0 [,) +oo ) )
118	28, 117	sseldi 3432	. . . . . . . . . . . 12 |- ( ph -> ( P ` 1 ) e. RR )
119	118	recnd 9674	. . . . . . . . . . 11 |- ( ph -> ( P ` 1 ) e. CC )
120	23, 24, 26, 27, 119	sumsnd 37357	. . . . . . . . . 10 |- ( ph -> sum_ j e. { 1 } ( P ` j ) = ( P ` 1 ) )
121	120	adantr 467	. . . . . . . . 9 |- ( ( ph /\ Y = (/) ) -> sum_ j e. { 1 } ( P ` j ) = ( P ` 1 ) )
122		fveq2 5870	. . . . . . . . . . . . 13 |- ( j = 1 -> ( J ` j ) = ( J ` 1 ) )
123		fveq2 5870	. . . . . . . . . . . . 13 |- ( j = 1 -> ( K ` j ) = ( K ` 1 ) )
124	122, 123	oveq12d 6313	. . . . . . . . . . . 12 |- ( j = 1 -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
125		ovex 6323	. . . . . . . . . . . 12 |- ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) e. _V
126	124, 40, 125	fvmpt 5953	. . . . . . . . . . 11 |- ( 1 e. NN -> ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
127	1, 126	ax-mp 5	. . . . . . . . . 10 |- ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) )
128	127	a1i 11	. . . . . . . . 9 |- ( ( ph /\ Y = (/) ) -> ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
129	7	oveqd 6312	. . . . . . . . . . 11 |- ( Y = (/) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) )
130	129	adantl 468	. . . . . . . . . 10 |- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) )
131	122	feq1d 5719	. . . . . . . . . . . . . . . 16 |- ( j = 1 -> ( ( J ` j ) : Y --> RR <-> ( J ` 1 ) : Y --> RR ) )
132	33, 131	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR ) <-> ( ( ph /\ 1 e. NN ) -> ( J ` 1 ) : Y --> RR ) ) )
133	69	adantr 467	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) : Y --> RR )
134	62	feq1d 5719	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> ( ( C ` j ) |` Y ) : Y --> RR ) )
135	133, 134	mpbird 236	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
136	82	ad2antrr 733	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F : Y --> RR )
137	79	feq1d 5719	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> F : Y --> RR ) )
138	136, 137	mpbird 236	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
139	135, 138	pm2.61dan 801	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
140		simpr 463	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> j e. NN )
141		fvex 5880	. . . . . . . . . . . . . . . . . . . . 21 |- ( C ` j ) e. _V
142	141	resex 5151	. . . . . . . . . . . . . . . . . . . 20 |- ( ( C ` j ) |` Y ) e. _V
143	62, 142	syl6eqel 2539	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
144	85	elexd 3058	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> F e. _V )
145	144	adantr 467	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ j e. NN ) -> F e. _V )
146	145	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F e. _V )
147	79, 146	eqeltrd 2531	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
148	143, 147	pm2.61dan 801	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
149	89	fvmpt2 5962	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. NN /\ if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
150	140, 148, 149	syl2anc 667	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
151	150	feq1d 5719	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR ) )
152	139, 151	mpbird 236	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
153	31, 132, 152	vtocl 3102	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 e. NN ) -> ( J ` 1 ) : Y --> RR )
154	29, 30, 153	syl2anc 667	. . . . . . . . . . . . 13 |- ( ph -> ( J ` 1 ) : Y --> RR )
155	154	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ Y = (/) ) -> ( J ` 1 ) : Y --> RR )
156		id 22	. . . . . . . . . . . . . . 15 |- ( Y = (/) -> Y = (/) )
157	156	eqcomd 2459	. . . . . . . . . . . . . 14 |- ( Y = (/) -> (/) = Y )
158	157	feq2d 5720	. . . . . . . . . . . . 13 |- ( Y = (/) -> ( ( J ` 1 ) : (/) --> RR <-> ( J ` 1 ) : Y --> RR ) )
159	158	adantl 468	. . . . . . . . . . . 12 |- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) : (/) --> RR <-> ( J ` 1 ) : Y --> RR ) )
160	155, 159	mpbird 236	. . . . . . . . . . 11 |- ( ( ph /\ Y = (/) ) -> ( J ` 1 ) : (/) --> RR )
161	123	feq1d 5719	. . . . . . . . . . . . . . . 16 |- ( j = 1 -> ( ( K ` j ) : Y --> RR <-> ( K ` 1 ) : Y --> RR ) )
162	33, 161	imbi12d 322	. . . . . . . . . . . . . . 15 |- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR ) <-> ( ( ph /\ 1 e. NN ) -> ( K ` 1 ) : Y --> RR ) ) )
163	31, 162, 113	vtocl 3102	. . . . . . . . . . . . . 14 |- ( ( ph /\ 1 e. NN ) -> ( K ` 1 ) : Y --> RR )
164	29, 30, 163	syl2anc 667	. . . . . . . . . . . . 13 |- ( ph -> ( K ` 1 ) : Y --> RR )
165	164	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ Y = (/) ) -> ( K ` 1 ) : Y --> RR )
166	157	feq2d 5720	. . . . . . . . . . . . 13 |- ( Y = (/) -> ( ( K ` 1 ) : (/) --> RR <-> ( K ` 1 ) : Y --> RR ) )
167	166	adantl 468	. . . . . . . . . . . 12 |- ( ( ph /\ Y = (/) ) -> ( ( K ` 1 ) : (/) --> RR <-> ( K ` 1 ) : Y --> RR ) )
168	165, 167	mpbird 236	. . . . . . . . . . 11 |- ( ( ph /\ Y = (/) ) -> ( K ` 1 ) : (/) --> RR )
169	18, 160, 168	hoidmv0val 38415	. . . . . . . . . 10 |- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) = 0 )
170	130, 169	eqtrd 2487	. . . . . . . . 9 |- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = 0 )
171	121, 128, 170	3eqtrd 2491	. . . . . . . 8 |- ( ( ph /\ Y = (/) ) -> sum_ j e. { 1 } ( P ` j ) = 0 )
172	171	oveq2d 6311	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) = ( ( 1 + E ) x. 0 ) )
173		hoidmvlelem3.e	. . . . . . . . . . . 12 |- ( ph -> E e. RR+ )
174	173	rpred 11348	. . . . . . . . . . 11 |- ( ph -> E e. RR )
175	27, 174	readdcld 9675	. . . . . . . . . 10 |- ( ph -> ( 1 + E ) e. RR )
176	175	recnd 9674	. . . . . . . . 9 |- ( ph -> ( 1 + E ) e. CC )
177	176	mul01d 9837	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. 0 ) = 0 )
178	177	adantr 467	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. 0 ) = 0 )
179		eqidd 2454	. . . . . . 7 |- ( ( ph /\ Y = (/) ) -> 0 = 0 )
180	172, 178, 179	3eqtrd 2491	. . . . . 6 |- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) = 0 )
181	22, 180	breq12d 4418	. . . . 5 |- ( ( ph /\ Y = (/) ) -> ( G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) <-> 0 <_ 0 ) )
182	4, 181	mpbird 236	. . . 4 |- ( ( ph /\ Y = (/) ) -> G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) )
183		oveq2 6303	. . . . . . . . 9 |- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
184	1	nnzi 10968	. . . . . . . . . . 11 |- 1 e. ZZ
185		fzsn 11847	. . . . . . . . . . 11 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
186	184, 185	ax-mp 5	. . . . . . . . . 10 |- ( 1 ... 1 ) = { 1 }
187	186	a1i 11	. . . . . . . . 9 |- ( m = 1 -> ( 1 ... 1 ) = { 1 } )
188	183, 187	eqtrd 2487	. . . . . . . 8 |- ( m = 1 -> ( 1 ... m ) = { 1 } )
189	188	sumeq1d 13779	. . . . . . 7 |- ( m = 1 -> sum_ j e. ( 1 ... m ) ( P ` j ) = sum_ j e. { 1 } ( P ` j ) )
190	189	oveq2d 6311	. . . . . 6 |- ( m = 1 -> ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) = ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) )
191	190	breq2d 4417	. . . . 5 |- ( m = 1 -> ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) <-> G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) ) )
192	191	rspcev 3152	. . . 4 |- ( ( 1 e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
193	2, 182, 192	syl2anc 667	. . 3 |- ( ( ph /\ Y = (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
194		simpl 459	. . . 4 |- ( ( ph /\ -. Y = (/) ) -> ph )
195		neqne 37384	. . . . 5 |- ( -. Y = (/) -> Y =/= (/) )
196	195	adantl 468	. . . 4 |- ( ( ph /\ -. Y = (/) ) -> Y =/= (/) )
197		nfv 1763	. . . . . 6 |- F/ j ( ph /\ Y =/= (/) )
198	184	a1i 11	. . . . . 6 |- ( ( ph /\ Y =/= (/) ) -> 1 e. ZZ )
199		nnuz 11201	. . . . . 6 |- NN = ( ZZ>= ` 1 )
200	115	adantlr 722	. . . . . 6 |- ( ( ( ph /\ Y =/= (/) ) /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
201		hoidmvlelem3.a	. . . . . . . . . . . 12 |- ( ph -> A : W --> RR )
202	67	a1i 11	. . . . . . . . . . . 12 |- ( ph -> Y C_ W )
203	201, 202	fssresd 5755	. . . . . . . . . . 11 |- ( ph -> ( A |` Y ) : Y --> RR )
204		hoidmvlelem3.b	. . . . . . . . . . . 12 |- ( ph -> B : W --> RR )
205	204, 202	fssresd 5755	. . . . . . . . . . 11 |- ( ph -> ( B |` Y ) : Y --> RR )
206	18, 59, 203, 205	hoidmvcl 38414	. . . . . . . . . 10 |- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
207	28, 206	sseldi 3432	. . . . . . . . 9 |- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. RR )
208	5, 207	syl5eqel 2535	. . . . . . . 8 |- ( ph -> G e. RR )
209		0red 9649	. . . . . . . . 9 |- ( ph -> 0 e. RR )
210		1rp 11313	. . . . . . . . . . . . 13 |- 1 e. RR+
211	210	a1i 11	. . . . . . . . . . . 12 |- ( ph -> 1 e. RR+ )
212	211, 173	jca 535	. . . . . . . . . . 11 |- ( ph -> ( 1 e. RR+ /\ E e. RR+ ) )
213		rpaddcl 11330	. . . . . . . . . . 11 |- ( ( 1 e. RR+ /\ E e. RR+ ) -> ( 1 + E ) e. RR+ )
214	212, 213	syl 17	. . . . . . . . . 10 |- ( ph -> ( 1 + E ) e. RR+ )
215		rpgt0 11320	. . . . . . . . . 10 |- ( ( 1 + E ) e. RR+ -> 0 < ( 1 + E ) )
216	214, 215	syl 17	. . . . . . . . 9 |- ( ph -> 0 < ( 1 + E ) )
217	209, 216	gtned 9775	. . . . . . . 8 |- ( ph -> ( 1 + E ) =/= 0 )
218	208, 175, 217	redivcld 10442	. . . . . . 7 |- ( ph -> ( G / ( 1 + E ) ) e. RR )
219	218	adantr 467	. . . . . 6 |- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) e. RR )
220	218	ltpnfd 11430	. . . . . . . . . 10 |- ( ph -> ( G / ( 1 + E ) ) < +oo )
221	220	adantr 467	. . . . . . . . 9 |- ( ( ph /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < +oo )
222		id 22	. . . . . . . . . . 11 |- ( (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo -> (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo )
223	222	eqcomd 2459	. . . . . . . . . 10 |- ( (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo -> +oo = (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) )
224	223	adantl 468	. . . . . . . . 9 |- ( ( ph /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> +oo = (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) )
225	221, 224	breqtrd 4430	. . . . . . . 8 |- ( ( ph /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) )
226	225	adantlr 722	. . . . . . 7 |- ( ( ( ph /\ Y =/= (/) ) /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) )
227		simpl 459	. . . . . . . 8 |- ( ( ( ph /\ Y =/= (/) ) /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( ph /\ Y =/= (/) ) )
228		simpr 463	. . . . . . . . . 10 |- ( ( ph /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo )
229		nnex 10622	. . . . . . . . . . . 12 |- NN e. _V
230	229	a1i 11	. . . . . . . . . . 11 |- ( ( ph /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> NN e. _V )
231		icossicc 11728	. . . . . . . . . . . . . 14 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
232	231, 115	sseldi 3432	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,] +oo ) )
233		eqid 2453	. . . . . . . . . . . . 13 |- ( j e. NN |-> ( P ` j ) ) = ( j e. NN |-> ( P ` j ) )
234	232, 233	fmptd 6051	. . . . . . . . . . . 12 |- ( ph -> ( j e. NN |-> ( P ` j ) ) : NN --> ( 0 [,] +oo ) )
235	234	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( j e. NN |-> ( P ` j ) ) : NN --> ( 0 [,] +oo ) )
236	230, 235	sge0repnf 38238	. . . . . . . . . 10 |- ( ( ph /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR <-> -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) )
237	228, 236	mpbird 236	. . . . . . . . 9 |- ( ( ph /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
238	237	adantlr 722	. . . . . . . 8 |- ( ( ( ph /\ Y =/= (/) ) /\ -. (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
239	219	adantr 467	. . . . . . . . 9 |- ( ( ( ph /\ Y =/= (/) ) /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) e. RR )
240	208	adantr 467	. . . . . . . . . 10 |- ( ( ph /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G e. RR )
241	240	adantlr 722	. . . . . . . . 9 |- ( ( ( ph /\ Y =/= (/) ) /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G e. RR )
242		simpr 463	. . . . . . . . 9 |- ( ( ( ph /\ Y =/= (/) ) /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
243	27, 173	ltaddrpd 11378	. . . . . . . . . . . 12 |- ( ph -> 1 < ( 1 + E ) )
244	243	adantr 467	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= (/) ) -> 1 < ( 1 + E ) )
245	59	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= (/) ) -> Y e. Fin )
246		simpr 463	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= (/) ) -> Y =/= (/) )
247	203	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= (/) ) -> ( A |` Y ) : Y --> RR )
248	205	adantr 467	. . . . . . . . . . . . . . 15 |- ( ( ph /\ Y =/= (/) ) -> ( B |` Y ) : Y --> RR )
249	18, 245, 246, 247, 248	hoidmvn0val 38416	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
250	5	a1i 11	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= (/) ) -> G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
251		fvres 5884	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. Y -> ( ( A |` Y ) ` k ) = ( A ` k ) )
252		fvres 5884	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. Y -> ( ( B |` Y ) ` k ) = ( B ` k ) )
253	251, 252	oveq12d 6313	. . . . . . . . . . . . . . . . . . . 20 |- ( k e. Y -> ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
254	253	fveq2d 5874	. . . . . . . . . . . . . . . . . . 19 |- ( k e. Y -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
255	254	adantl 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
256	201	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. Y ) -> A : W --> RR )
257		elun1 3603	. . . . . . . . . . . . . . . . . . . . . 22 |- ( k e. Y -> k e. ( Y u. { Z } ) )
258	257, 45	syl6eleqr 2542	. . . . . . . . . . . . . . . . . . . . 21 |- ( k e. Y -> k e. W )
259	258	adantl 468	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. Y ) -> k e. W )
260	256, 259	ffvelrnd 6028	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. Y ) -> ( A ` k ) e. RR )
261	204	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. Y ) -> B : W --> RR )
262	261, 259	ffvelrnd 6028	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. Y ) -> ( B ` k ) e. RR )
263		volico 38373	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
264	260, 262, 263	syl2anc 667	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. Y ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
265		hoidmvlelem3.lt	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
266	259, 265	syldan 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ k e. Y ) -> ( A ` k ) < ( B ` k ) )
267	266	iftrued 3891	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ k e. Y ) -> if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) = ( ( B ` k ) - ( A ` k ) ) )
268	255, 264, 267	3eqtrd 2491	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
269	268	prodeq2dv 13989	. . . . . . . . . . . . . . . 16 |- ( ph -> prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
270	269	eqcomd 2459	. . . . . . . . . . . . . . 15 |- ( ph -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
271	270	adantr 467	. . . . . . . . . . . . . 14 |- ( ( ph /\ Y =/= (/) ) -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
272	249, 250, 271	3eqtr4d 2497	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= (/) ) -> G = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
273		difrp 11344	. . . . . . . . . . . . . . . . 17 |- ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
274	260, 262, 273	syl2anc 667	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ k e. Y ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
275	266, 274	mpbid 214	. . . . . . . . . . . . . . 15 |- ( ( ph /\ k e. Y ) -> ( ( B ` k ) - ( A ` k ) ) e. RR+ )
276	59, 275	fprodrpcl 14022	. . . . . . . . . . . . . 14 |- ( ph -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) e. RR+ )
277	276	adantr 467	. . . . . . . . . . . . 13 |- ( ( ph /\ Y =/= (/) ) -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) e. RR+ )
278	272, 277	eqeltrd 2531	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= (/) ) -> G e. RR+ )
279	214	adantr 467	. . . . . . . . . . . 12 |- ( ( ph /\ Y =/= (/) ) -> ( 1 + E ) e. RR+ )
280	278, 279	ltdivgt1 37589	. . . . . . . . . . 11 |- ( ( ph /\ Y =/= (/) ) -> ( 1 < ( 1 + E ) <-> ( G / ( 1 + E ) ) < G ) )
281	244, 280	mpbid 214	. . . . . . . . . 10 |- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) < G )
282	281	adantr 467	. . . . . . . . 9 |- ( ( ( ph /\ Y =/= (/) ) /\ (Σ^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) < G )
283		hoidmvlelem3.i2	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
284	283	adantr 467	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
285		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( x ` k ) e. _V
286	285	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> ( x ` k ) e. _V )
287		hoidmvlelem3.s	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ph -> S e. U )
288	287	elexd 3058	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ph -> S e. _V )
289	286, 288	ifcld 3926	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> if ( k e. Y , ( x ` k ) , S ) e. _V )
290	289	ralrimivw 2805	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ph -> A. k e. W if ( k e. Y , ( x ` k ) , S ) e. _V )
291	290	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> A. k e. W if ( k e. Y , ( x ` k ) , S ) e. _V )
292		eqid 2453	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) )
293	292	fnmpt 5709	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( A. k e. W if ( k e. Y , ( x ` k ) , S ) e. _V -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) Fn W )
294	291, 293	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) Fn W )
295		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
296		mptexg 6140	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( W e. Fin -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
297	54, 296	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
298	297	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
299		hoidmvlelem3.o	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- O = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
300	299	fvmpt2 5962	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V ) -> ( O ` x ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
301	295, 298, 300	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
302	301	fneq1d 5671	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( O ` x ) Fn W <-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) Fn W ) )
303	294, 302	mpbird 236	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) Fn W )
304		nfv 1763	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ k ph
305		nfcv 2594	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ k x
306		nfixp1 7547	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ k X_ k e. Y ( ( A ` k ) [,) ( B ` k ) )
307	305, 306	nfel 2606	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ k x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) )
308	304, 307	nfan 2013	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ k ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
309	301	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( O ` x ) ` k ) = ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) )
310	309	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) = ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) )
311		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. W ) -> k e. W )
312	289	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ k e. W ) -> if ( k e. Y , ( x ` k ) , S ) e. _V )
313	292	fvmpt2 5962	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( k e. W /\ if ( k e. Y , ( x ` k ) , S ) e. _V ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
314	311, 312, 313	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ k e. W ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
315	314	adantlr 722	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
316	310, 315	eqtrd 2487	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
317		iftrue 3889	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( k e. Y -> if ( k e. Y , ( x ` k ) , S ) = ( x ` k ) )
318	317	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) = ( x ` k ) )
319		vex 3050	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- x e. _V
320	319	elixp 7534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) <-> ( x Fn Y /\ A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
321	320	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) -> A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
322	321	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
323		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> k e. Y )
324		rspa 2757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
325	322, 323, 324	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
326	325	ad4ant24 1241	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
327	318, 326	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
328		snidg 3996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( Z e. ( X \ Y ) -> Z e. { Z } )
329	48, 328	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> Z e. { Z } )
330		elun2 3604	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
331	329, 330	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> Z e. ( Y u. { Z } ) )
332	56	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ph -> ( Y u. { Z } ) = W )
333	331, 332	eleqtrd 2533	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ph -> Z e. W )
334	201, 333	ffvelrnd 6028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( A ` Z ) e. RR )
335	334	rexrd 9695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> ( A ` Z ) e. RR* )
336	204, 333	ffvelrnd 6028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> ( B ` Z ) e. RR )
337	336	rexrd 9695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> ( B ` Z ) e. RR* )
338		iccssxr 11724	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR*
339		hoidmvlelem3.u	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
340		ssrab2 3516	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
341	339, 340	eqsstri 3464	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- U C_ ( ( A ` Z ) [,] ( B ` Z ) )
342	341, 287	sseldi 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
343	338, 342	sseldi 3432	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> S e. RR* )
344		iccgelb 11698	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ S )
345	335, 337, 342, 344	syl3anc 1269	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> ( A ` Z ) <_ S )
346		hoidmvlelem3.sb	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ph -> S < ( B ` Z ) )
347	335, 337, 343, 345, 346	elicod 11692	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ph -> S e. ( ( A ` Z ) [,) ( B ` Z ) ) )
348	347	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> S e. ( ( A ` Z ) [,) ( B ` Z ) ) )
349		iffalse 3892	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( -. k e. Y -> if ( k e. Y , ( x ` k ) , S ) = S )
350	349	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) = S )
351	45	eleq2i 2523	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k e. W <-> k e. ( Y u. { Z } ) )
352	351	biimpi 198	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k e. W -> k e. ( Y u. { Z } ) )
353	352	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( k e. W /\ -. k e. Y ) -> k e. ( Y u. { Z } ) )
354		simpr 463	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( k e. W /\ -. k e. Y ) -> -. k e. Y )
355		elunnel1 3577	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( k e. ( Y u. { Z } ) /\ -. k e. Y ) -> k e. { Z } )
356	353, 354, 355	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( k e. W /\ -. k e. Y ) -> k e. { Z } )
357		elsni 3995	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k e. { Z } -> k = Z )
358	356, 357	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( k e. W /\ -. k e. Y ) -> k = Z )
359		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k = Z -> ( A ` k ) = ( A ` Z ) )
360		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( k = Z -> ( B ` k ) = ( B ` Z ) )
361	359, 360	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
362	358, 361	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( k e. W /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
363	362	adantll 721	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
364	350, 363	eleq12d 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> ( if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) <-> S e. ( ( A ` Z ) [,) ( B ` Z ) ) ) )
365	348, 364	mpbird 236	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
366	365	adantllr 726	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
367	327, 366	pm2.61dan 801	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
368	316, 367	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
369	368	ex 436	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W -> ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
370	308, 369	ralrimi 2790	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
371	303, 370	jca 535	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( O ` x ) Fn W /\ A. k e. W ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
372		fvex 5880	. . . . . . . . . . . . . . . . . . . . . 22 |- ( O ` x ) e. _V
373	372	elixp 7534	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( O ` x ) e. X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) <-> ( ( O ` x ) Fn W /\ A. k e. W ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
374	371, 373	sylibr 216	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) e. X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) )
375	284, 374	sseldd 3435	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) e. U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
376		eliun 4286	. . . . . . . . . . . . . . . . . . 19 |- ( ( O ` x ) e. U_ j e. NN X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> E. j e. NN ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
377	375, 376	sylib 200	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> E. j e. NN ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
378		ixpfn 7533	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) -> x Fn Y )
379	378	adantl 468	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x Fn Y )
380	379	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> x Fn Y )
381		nfv 1763	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/ k j e. NN
382	308, 381	nfan 2013	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ k ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN )
383		nfcv 2594	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ k ( O ` x )
384		nfixp1 7547	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- F/_ k X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
385	383, 384	nfel 2606	. . . . . . . . . . . . . . . . . . . . . . . 24 |- F/ k ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
386	382, 385	nfan 2013	. . . . . . . . . . . . . . . . . . . . . . 23 |- F/ k ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
387	309	3adant3 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( ( O ` x ) ` k ) = ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) )
388	289	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. _V )
389	259, 388, 313	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ph /\ k e. Y ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
390	389	3adant2 1028	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
391	317	3ad2ant3 1032	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) = ( x ` k ) )
392	387, 390, 391	3eqtrrd 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) = ( ( O ` x ) ` k ) )
393	392	ad5ant125 1255	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. Y ) -> ( x ` k ) = ( ( O ` x ) ` k ) )
394		simpl 459	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
395	372	elixp 7534	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> ( ( O ` x ) Fn W /\ A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
396	394, 395	sylib 200	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> ( ( O ` x ) Fn W /\ A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
397	396	simprd 465	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
398	258	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> k e. W )
399		rspa 2757	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
400	397, 398, 399	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
401	400	adantll 721	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. Y ) -> ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
402	393, 401	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) /\ k e. Y ) -> ( x ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
403	29	ad3antrrr 737	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ph )
404	37	ad2antlr 734	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> j e. NN )
405	301	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( O ` x ) ` Z ) = ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` Z ) )
406		eqidd 2454	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
407		eleq1 2519	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( k = Z -> ( k e. Y <-> Z e. Y ) )
408		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( k = Z -> ( x ` k ) = ( x ` Z ) )
409	407, 408	ifbieq1d 3906	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( k = Z -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
410	409	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ph /\ k = Z ) -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
411		fvex 5880	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( x ` Z ) e. _V
412	411	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ph -> ( x ` Z ) e. _V )
413	412, 288	ifcld 3926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) e. _V )
414	406, 410, 333, 413	fvmptd 5959	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` Z ) = if ( Z e. Y , ( x ` Z ) , S ) )
415	414	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` Z ) = if ( Z e. Y , ( x ` Z ) , S ) )
416	48	eldifbd 3419	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ph -> -. Z e. Y )
417	416	iffalsed 3894	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) = S )
418	417	adantr 467	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> if ( Z e. Y , ( x ` Z ) , S ) = S )
419	405, 415, 418	3eqtrrd 2492	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> S = ( ( O ` x ) ` Z ) )
420	419	ad2antrr 733	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> S = ( ( O ` x ) ` Z ) )
421	403, 333	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> Z e. W )
422	395	simprbi 466	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
423	422	adantl 468	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
424		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k = Z -> ( ( O ` x ) ` k ) = ( ( O ` x ) ` Z ) )
425		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k = Z -> ( ( C ` j ) ` k ) = ( ( C ` j ) ` Z ) )
426		fveq2 5870	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( k = Z -> ( ( D ` j ) ` k ) = ( ( D ` j ) ` Z ) )
427	425, 426	oveq12d 6313	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( k = Z -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
428	424, 427	eleq12d 2525	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( k = Z -> ( ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> ( ( O ` x ) ` Z ) e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
429	428	rspcva 3150	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( Z e. W /\ A. k e. W ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( ( O ` x ) ` Z ) e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
430	421, 423, 429	syl2anc 667	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> ( ( O ` x ) ` Z ) e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
431	420, 430	eqeltrd 2531	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN ) /\ ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) -> S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
432	150	3adant3 1029	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
433	61	3ad2ant3 1032	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
434	432, 433	eqtrd 2487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = ( ( C ` j ) |` Y ) )
435	434	fveq1d 5872	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z )