Theorem hoidmvlelem3

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)

	Ref	Expression
Hypotheses	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 -> ( sum^ ` ( 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. ( sum^ ` ( 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 ) <_ ( sum^ ` ( 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	hoidmvlelem3	|- ( ph -> E. u e. U S < u )

Proof

Step	Hyp	Ref	Expression
1		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 ) ) ) ) ) )
2		hoidmvlelem3.x	|- ( ph -> X e. Fin )
3		hoidmvlelem3.y	|- ( ph -> Y C_ X )
4		hoidmvlelem3.z	|- ( ph -> Z e. ( X \ Y ) )
5		hoidmvlelem3.w	|- W = ( Y u. { Z } )
6		hoidmvlelem3.a	|- ( ph -> A : W --> RR )
7		hoidmvlelem3.b	|- ( ph -> B : W --> RR )
8		hoidmvlelem3.lt	|- ( ( ph /\ k e. W ) -> ( A ` k ) < ( B ` k ) )
9		hoidmvlelem3.f	|- F = ( y e. Y |-> 0 )
10		hoidmvlelem3.c	|- ( ph -> C : NN --> ( RR ^m W ) )
11		hoidmvlelem3.j	|- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
12		hoidmvlelem3.d	|- ( ph -> D : NN --> ( RR ^m W ) )
13		hoidmvlelem3.k	|- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
14		hoidmvlelem3.r	|- ( ph -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
15		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 ) ) ) ) )
16		hoidmvlelem3.g	|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
17		hoidmvlelem3.e	|- ( ph -> E e. RR+ )
18		hoidmvlelem3.u	|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
19		hoidmvlelem3.s	|- ( ph -> S e. U )
20		hoidmvlelem3.sb	|- ( ph -> S < ( B ` Z ) )
21		hoidmvlelem3.p	|- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
22		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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
23		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 ) ) )
24		hoidmvlelem3.o	|- O = ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) |-> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
25		1nn	|- 1 e. NN
26	25	a1i	|- ( ( ph /\ Y = (/) ) -> 1 e. NN )
27		0le0	|- 0 <_ 0
28	27	a1i	|- ( ( ph /\ Y = (/) ) -> 0 <_ 0 )
29	16	a1i	|- ( ( ph /\ Y = (/) ) -> G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
30		fveq2	|- ( Y = (/) -> ( L ` Y ) = ( L ` (/) ) )
31		reseq2	|- ( Y = (/) -> ( A |` Y ) = ( A |` (/) ) )
32		res0	|- ( A |` (/) ) = (/)
33	32	a1i	|- ( Y = (/) -> ( A |` (/) ) = (/) )
34	31 33	eqtrd	|- ( Y = (/) -> ( A |` Y ) = (/) )
35		reseq2	|- ( Y = (/) -> ( B |` Y ) = ( B |` (/) ) )
36		res0	|- ( B |` (/) ) = (/)
37	36	a1i	|- ( Y = (/) -> ( B |` (/) ) = (/) )
38	35 37	eqtrd	|- ( Y = (/) -> ( B |` Y ) = (/) )
39	30 34 38	oveq123d	|- ( Y = (/) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = ( (/) ( L ` (/) ) (/) ) )
40	39	adantl	|- ( ( ph /\ Y = (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = ( (/) ( L ` (/) ) (/) ) )
41		f0	|- (/) : (/) --> RR
42	41	a1i	|- ( ( ph /\ Y = (/) ) -> (/) : (/) --> RR )
43	1 42 42	hoidmv0val	|- ( ( ph /\ Y = (/) ) -> ( (/) ( L ` (/) ) (/) ) = 0 )
44	29 40 43	3eqtrd	|- ( ( ph /\ Y = (/) ) -> G = 0 )
45		nfcvd	|- ( ph -> F/_ j ( P ` 1 ) )
46		nfv	|- F/ j ph
47		simpr	|- ( ( ph /\ j = 1 ) -> j = 1 )
48	47	fveq2d	|- ( ( ph /\ j = 1 ) -> ( P ` j ) = ( P ` 1 ) )
49		1red	|- ( ph -> 1 e. RR )
50		rge0ssre	|- ( 0 [,) +oo ) C_ RR
51		id	|- ( ph -> ph )
52	25	a1i	|- ( ph -> 1 e. NN )
53	25	elexi	|- 1 e. _V
54		eleq1	|- ( j = 1 -> ( j e. NN <-> 1 e. NN ) )
55	54	anbi2d	|- ( j = 1 -> ( ( ph /\ j e. NN ) <-> ( ph /\ 1 e. NN ) ) )
56		fveq2	|- ( j = 1 -> ( P ` j ) = ( P ` 1 ) )
57	56	eleq1d	|- ( j = 1 -> ( ( P ` j ) e. ( 0 [,) +oo ) <-> ( P ` 1 ) e. ( 0 [,) +oo ) ) )
58	55 57	imbi12d	|- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) ) <-> ( ( ph /\ 1 e. NN ) -> ( P ` 1 ) e. ( 0 [,) +oo ) ) ) )
59		id	|- ( j e. NN -> j e. NN )
60		ovexd	|- ( j e. NN -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V )
61	21	fvmpt2	|- ( ( j e. NN /\ ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
62	59 60 61	syl2anc	|- ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
63	62	adantl	|- ( ( ph /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
64	5	a1i	|- ( ph -> W = ( Y u. { Z } ) )
65	4	eldifad	|- ( ph -> Z e. X )
66		snssi	|- ( Z e. X -> { Z } C_ X )
67	65 66	syl	|- ( ph -> { Z } C_ X )
68	3 67	unssd	|- ( ph -> ( Y u. { Z } ) C_ X )
69	64 68	eqsstrd	|- ( ph -> W C_ X )
70	2 69	ssfid	|- ( ph -> W e. Fin )
71		ssun1	|- Y C_ ( Y u. { Z } )
72	5	eqcomi	|- ( Y u. { Z } ) = W
73	71 72	sseqtri	|- Y C_ W
74	73	a1i	|- ( ph -> Y C_ W )
75	70 74	ssfid	|- ( ph -> Y e. Fin )
76	75	adantr	|- ( ( ph /\ j e. NN ) -> Y e. Fin )
77		iftrue	|- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
78	77	adantl	|- ( ( ( 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 ) )
79	10	ffvelcdmda	|- ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
80		elmapi	|- ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
81	79 80	syl	|- ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
82	71 5	sseqtrri	|- Y C_ W
83	82	a1i	|- ( ( ph /\ j e. NN ) -> Y C_ W )
84	81 83	fssresd	|- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) : Y --> RR )
85		reex	|- RR e. _V
86	85	a1i	|- ( ( ph /\ j e. NN ) -> RR e. _V )
87	70 74	ssexd	|- ( ph -> Y e. _V )
88	87	adantr	|- ( ( ph /\ j e. NN ) -> Y e. _V )
89	86 88	elmapd	|- ( ( ph /\ j e. NN ) -> ( ( ( C ` j ) |` Y ) e. ( RR ^m Y ) <-> ( ( C ` j ) |` Y ) : Y --> RR ) )
90	84 89	mpbird	|- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) e. ( RR ^m Y ) )
91	90	adantr	|- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) e. ( RR ^m Y ) )
92	78 91	eqeltrd	|- ( ( ( 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 ) )
93		iffalse	|- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
94	93	adantl	|- ( ( ( 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 )
95		0red	|- ( ( ph /\ y e. Y ) -> 0 e. RR )
96	95 9	fmptd	|- ( ph -> F : Y --> RR )
97	85	a1i	|- ( ph -> RR e. _V )
98	97 75	elmapd	|- ( ph -> ( F e. ( RR ^m Y ) <-> F : Y --> RR ) )
99	96 98	mpbird	|- ( ph -> F e. ( RR ^m Y ) )
100	99	ad2antrr	|- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F e. ( RR ^m Y ) )
101	94 100	eqeltrd	|- ( ( ( 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 ) )
102	92 101	pm2.61dan	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
103	102 11	fmptd	|- ( ph -> J : NN --> ( RR ^m Y ) )
104	103	ffvelcdmda	|- ( ( ph /\ j e. NN ) -> ( J ` j ) e. ( RR ^m Y ) )
105		elmapi	|- ( ( J ` j ) e. ( RR ^m Y ) -> ( J ` j ) : Y --> RR )
106	104 105	syl	|- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
107		iftrue	|- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
108	107	adantl	|- ( ( ( 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 ) )
109	12	ffvelcdmda	|- ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
110		elmapi	|- ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
111	109 110	syl	|- ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
112	111 83	fssresd	|- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) : Y --> RR )
113	86 88	elmapd	|- ( ( ph /\ j e. NN ) -> ( ( ( D ` j ) |` Y ) e. ( RR ^m Y ) <-> ( ( D ` j ) |` Y ) : Y --> RR ) )
114	112 113	mpbird	|- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) e. ( RR ^m Y ) )
115	114	adantr	|- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( D ` j ) |` Y ) e. ( RR ^m Y ) )
116	108 115	eqeltrd	|- ( ( ( 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 ) )
117		iffalse	|- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
118	117	adantl	|- ( ( ( 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 )
119	118 100	eqeltrd	|- ( ( ( 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 ) )
120	116 119	pm2.61dan	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. ( RR ^m Y ) )
121	120 13	fmptd	|- ( ph -> K : NN --> ( RR ^m Y ) )
122	121	ffvelcdmda	|- ( ( ph /\ j e. NN ) -> ( K ` j ) e. ( RR ^m Y ) )
123		elmapi	|- ( ( K ` j ) e. ( RR ^m Y ) -> ( K ` j ) : Y --> RR )
124	122 123	syl	|- ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR )
125	1 76 106 124	hoidmvcl	|- ( ( ph /\ j e. NN ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. ( 0 [,) +oo ) )
126	63 125	eqeltrd	|- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
127	53 58 126	vtocl	|- ( ( ph /\ 1 e. NN ) -> ( P ` 1 ) e. ( 0 [,) +oo ) )
128	51 52 127	syl2anc	|- ( ph -> ( P ` 1 ) e. ( 0 [,) +oo ) )
129	50 128	sselid	|- ( ph -> ( P ` 1 ) e. RR )
130	129	recnd	|- ( ph -> ( P ` 1 ) e. CC )
131	45 46 48 49 130	sumsnd	|- ( ph -> sum_ j e. { 1 } ( P ` j ) = ( P ` 1 ) )
132	131	adantr	|- ( ( ph /\ Y = (/) ) -> sum_ j e. { 1 } ( P ` j ) = ( P ` 1 ) )
133		fveq2	|- ( j = 1 -> ( J ` j ) = ( J ` 1 ) )
134		fveq2	|- ( j = 1 -> ( K ` j ) = ( K ` 1 ) )
135	133 134	oveq12d	|- ( j = 1 -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
136		ovex	|- ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) e. _V
137	135 21 136	fvmpt	|- ( 1 e. NN -> ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
138	25 137	ax-mp	|- ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) )
139	138	a1i	|- ( ( ph /\ Y = (/) ) -> ( P ` 1 ) = ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) )
140	30	oveqd	|- ( Y = (/) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) )
141	140	adantl	|- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) )
142	133	feq1d	|- ( j = 1 -> ( ( J ` j ) : Y --> RR <-> ( J ` 1 ) : Y --> RR ) )
143	55 142	imbi12d	|- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR ) <-> ( ( ph /\ 1 e. NN ) -> ( J ` 1 ) : Y --> RR ) ) )
144	84	adantr	|- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) : Y --> RR )
145	78	feq1d	|- ( ( ( 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 ) )
146	144 145	mpbird	|- ( ( ( 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 )
147	96	ad2antrr	|- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F : Y --> RR )
148	94	feq1d	|- ( ( ( 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 ) )
149	147 148	mpbird	|- ( ( ( 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 )
150	146 149	pm2.61dan	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
151		simpr	|- ( ( ph /\ j e. NN ) -> j e. NN )
152		fvex	|- ( C ` j ) e. _V
153	152	resex	|- ( ( C ` j ) |` Y ) e. _V
154	78 153	eqeltrdi	|- ( ( ( 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 )
155	99	elexd	|- ( ph -> F e. _V )
156	155	adantr	|- ( ( ph /\ j e. NN ) -> F e. _V )
157	156	adantr	|- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F e. _V )
158	94 157	eqeltrd	|- ( ( ( 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 )
159	154 158	pm2.61dan	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
160	11	fvmpt2	|- ( ( 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 ) )
161	151 159 160	syl2anc	|- ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
162	161	feq1d	|- ( ( ph /\ j e. NN ) -> ( ( J ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR ) )
163	150 162	mpbird	|- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
164	53 143 163	vtocl	|- ( ( ph /\ 1 e. NN ) -> ( J ` 1 ) : Y --> RR )
165	51 52 164	syl2anc	|- ( ph -> ( J ` 1 ) : Y --> RR )
166	165	adantr	|- ( ( ph /\ Y = (/) ) -> ( J ` 1 ) : Y --> RR )
167		id	|- ( Y = (/) -> Y = (/) )
168	167	eqcomd	|- ( Y = (/) -> (/) = Y )
169	168	feq2d	|- ( Y = (/) -> ( ( J ` 1 ) : (/) --> RR <-> ( J ` 1 ) : Y --> RR ) )
170	169	adantl	|- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) : (/) --> RR <-> ( J ` 1 ) : Y --> RR ) )
171	166 170	mpbird	|- ( ( ph /\ Y = (/) ) -> ( J ` 1 ) : (/) --> RR )
172	134	feq1d	|- ( j = 1 -> ( ( K ` j ) : Y --> RR <-> ( K ` 1 ) : Y --> RR ) )
173	55 172	imbi12d	|- ( j = 1 -> ( ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR ) <-> ( ( ph /\ 1 e. NN ) -> ( K ` 1 ) : Y --> RR ) ) )
174	53 173 124	vtocl	|- ( ( ph /\ 1 e. NN ) -> ( K ` 1 ) : Y --> RR )
175	51 52 174	syl2anc	|- ( ph -> ( K ` 1 ) : Y --> RR )
176	175	adantr	|- ( ( ph /\ Y = (/) ) -> ( K ` 1 ) : Y --> RR )
177	168	feq2d	|- ( Y = (/) -> ( ( K ` 1 ) : (/) --> RR <-> ( K ` 1 ) : Y --> RR ) )
178	177	adantl	|- ( ( ph /\ Y = (/) ) -> ( ( K ` 1 ) : (/) --> RR <-> ( K ` 1 ) : Y --> RR ) )
179	176 178	mpbird	|- ( ( ph /\ Y = (/) ) -> ( K ` 1 ) : (/) --> RR )
180	1 171 179	hoidmv0val	|- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` (/) ) ( K ` 1 ) ) = 0 )
181	141 180	eqtrd	|- ( ( ph /\ Y = (/) ) -> ( ( J ` 1 ) ( L ` Y ) ( K ` 1 ) ) = 0 )
182	132 139 181	3eqtrd	|- ( ( ph /\ Y = (/) ) -> sum_ j e. { 1 } ( P ` j ) = 0 )
183	182	oveq2d	|- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) = ( ( 1 + E ) x. 0 ) )
184	17	rpred	|- ( ph -> E e. RR )
185	49 184	readdcld	|- ( ph -> ( 1 + E ) e. RR )
186	185	recnd	|- ( ph -> ( 1 + E ) e. CC )
187	186	mul01d	|- ( ph -> ( ( 1 + E ) x. 0 ) = 0 )
188	187	adantr	|- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. 0 ) = 0 )
189		eqidd	|- ( ( ph /\ Y = (/) ) -> 0 = 0 )
190	183 188 189	3eqtrd	|- ( ( ph /\ Y = (/) ) -> ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) = 0 )
191	44 190	breq12d	|- ( ( ph /\ Y = (/) ) -> ( G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) <-> 0 <_ 0 ) )
192	28 191	mpbird	|- ( ( ph /\ Y = (/) ) -> G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) )
193		oveq2	|- ( m = 1 -> ( 1 ... m ) = ( 1 ... 1 ) )
194	25	nnzi	|- 1 e. ZZ
195		fzsn	|- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
196	194 195	ax-mp	|- ( 1 ... 1 ) = { 1 }
197	196	a1i	|- ( m = 1 -> ( 1 ... 1 ) = { 1 } )
198	193 197	eqtrd	|- ( m = 1 -> ( 1 ... m ) = { 1 } )
199	198	sumeq1d	|- ( m = 1 -> sum_ j e. ( 1 ... m ) ( P ` j ) = sum_ j e. { 1 } ( P ` j ) )
200	199	oveq2d	|- ( m = 1 -> ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) = ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) )
201	200	breq2d	|- ( m = 1 -> ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) <-> G <_ ( ( 1 + E ) x. sum_ j e. { 1 } ( P ` j ) ) ) )
202	201	rspcev	|- ( ( 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 ) ) )
203	26 192 202	syl2anc	|- ( ( ph /\ Y = (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
204		simpl	|- ( ( ph /\ -. Y = (/) ) -> ph )
205		neqne	|- ( -. Y = (/) -> Y =/= (/) )
206	205	adantl	|- ( ( ph /\ -. Y = (/) ) -> Y =/= (/) )
207		nfv	|- F/ j ( ph /\ Y =/= (/) )
208	194	a1i	|- ( ( ph /\ Y =/= (/) ) -> 1 e. ZZ )
209		nnuz	|- NN = ( ZZ>= ` 1 )
210	126	adantlr	|- ( ( ( ph /\ Y =/= (/) ) /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
211	82	a1i	|- ( ph -> Y C_ W )
212	6 211	fssresd	|- ( ph -> ( A |` Y ) : Y --> RR )
213	7 211	fssresd	|- ( ph -> ( B |` Y ) : Y --> RR )
214	1 75 212 213	hoidmvcl	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
215	50 214	sselid	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. RR )
216	16 215	eqeltrid	|- ( ph -> G e. RR )
217		0red	|- ( ph -> 0 e. RR )
218		1rp	|- 1 e. RR+
219	218	a1i	|- ( ph -> 1 e. RR+ )
220	219 17	jca	|- ( ph -> ( 1 e. RR+ /\ E e. RR+ ) )
221		rpaddcl	|- ( ( 1 e. RR+ /\ E e. RR+ ) -> ( 1 + E ) e. RR+ )
222	220 221	syl	|- ( ph -> ( 1 + E ) e. RR+ )
223		rpgt0	|- ( ( 1 + E ) e. RR+ -> 0 < ( 1 + E ) )
224	222 223	syl	|- ( ph -> 0 < ( 1 + E ) )
225	217 224	gtned	|- ( ph -> ( 1 + E ) =/= 0 )
226	216 185 225	redivcld	|- ( ph -> ( G / ( 1 + E ) ) e. RR )
227	226	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) e. RR )
228	226	ltpnfd	|- ( ph -> ( G / ( 1 + E ) ) < +oo )
229	228	adantr	|- ( ( ph /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < +oo )
230		id	|- ( ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo )
231	230	eqcomd	|- ( ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo -> +oo = ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
232	231	adantl	|- ( ( ph /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> +oo = ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
233	229 232	breqtrd	|- ( ( ph /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
234	233	adantlr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
235		simpl	|- ( ( ( ph /\ Y =/= (/) ) /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( ph /\ Y =/= (/) ) )
236		simpr	|- ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo )
237		nnex	|- NN e. _V
238	237	a1i	|- ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> NN e. _V )
239		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
240	239 126	sselid	|- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,] +oo ) )
241		eqid	|- ( j e. NN |-> ( P ` j ) ) = ( j e. NN |-> ( P ` j ) )
242	240 241	fmptd	|- ( ph -> ( j e. NN |-> ( P ` j ) ) : NN --> ( 0 [,] +oo ) )
243	242	adantr	|- ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( j e. NN |-> ( P ` j ) ) : NN --> ( 0 [,] +oo ) )
244	238 243	sge0repnf	|- ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR <-> -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) )
245	236 244	mpbird	|- ( ( ph /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
246	245	adantlr	|- ( ( ( ph /\ Y =/= (/) ) /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
247	227	adantr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) e. RR )
248	216	adantr	|- ( ( ph /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G e. RR )
249	248	adantlr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G e. RR )
250		simpr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR )
251	49 17	ltaddrpd	|- ( ph -> 1 < ( 1 + E ) )
252	251	adantr	|- ( ( ph /\ Y =/= (/) ) -> 1 < ( 1 + E ) )
253	75	adantr	|- ( ( ph /\ Y =/= (/) ) -> Y e. Fin )
254		simpr	|- ( ( ph /\ Y =/= (/) ) -> Y =/= (/) )
255	212	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( A |` Y ) : Y --> RR )
256	213	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( B |` Y ) : Y --> RR )
257	1 253 254 255 256	hoidmvn0val	|- ( ( ph /\ Y =/= (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
258	16	a1i	|- ( ( ph /\ Y =/= (/) ) -> G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
259		fvres	|- ( k e. Y -> ( ( A |` Y ) ` k ) = ( A ` k ) )
260		fvres	|- ( k e. Y -> ( ( B |` Y ) ` k ) = ( B ` k ) )
261	259 260	oveq12d	|- ( k e. Y -> ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
262	261	fveq2d	|- ( k e. Y -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
263	262	adantl	|- ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
264	6	adantr	|- ( ( ph /\ k e. Y ) -> A : W --> RR )
265		elun1	|- ( k e. Y -> k e. ( Y u. { Z } ) )
266	265 5	eleqtrrdi	|- ( k e. Y -> k e. W )
267	266	adantl	|- ( ( ph /\ k e. Y ) -> k e. W )
268	264 267	ffvelcdmd	|- ( ( ph /\ k e. Y ) -> ( A ` k ) e. RR )
269	7	adantr	|- ( ( ph /\ k e. Y ) -> B : W --> RR )
270	269 267	ffvelcdmd	|- ( ( ph /\ k e. Y ) -> ( B ` k ) e. RR )
271		volico	|- ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
272	268 270 271	syl2anc	|- ( ( ph /\ k e. Y ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) )
273	267 8	syldan	|- ( ( ph /\ k e. Y ) -> ( A ` k ) < ( B ` k ) )
274	273	iftrued	|- ( ( ph /\ k e. Y ) -> if ( ( A ` k ) < ( B ` k ) , ( ( B ` k ) - ( A ` k ) ) , 0 ) = ( ( B ` k ) - ( A ` k ) ) )
275	263 272 274	3eqtrd	|- ( ( ph /\ k e. Y ) -> ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = ( ( B ` k ) - ( A ` k ) ) )
276	275	prodeq2dv	|- ( ph -> prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
277	276	eqcomd	|- ( ph -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
278	277	adantr	|- ( ( ph /\ Y =/= (/) ) -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) = prod_ k e. Y ( vol ` ( ( ( A |` Y ) ` k ) [,) ( ( B |` Y ) ` k ) ) ) )
279	257 258 278	3eqtr4d	|- ( ( ph /\ Y =/= (/) ) -> G = prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) )
280		difrp	|- ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
281	268 270 280	syl2anc	|- ( ( ph /\ k e. Y ) -> ( ( A ` k ) < ( B ` k ) <-> ( ( B ` k ) - ( A ` k ) ) e. RR+ ) )
282	273 281	mpbid	|- ( ( ph /\ k e. Y ) -> ( ( B ` k ) - ( A ` k ) ) e. RR+ )
283	75 282	fprodrpcl	|- ( ph -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) e. RR+ )
284	283	adantr	|- ( ( ph /\ Y =/= (/) ) -> prod_ k e. Y ( ( B ` k ) - ( A ` k ) ) e. RR+ )
285	279 284	eqeltrd	|- ( ( ph /\ Y =/= (/) ) -> G e. RR+ )
286	222	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( 1 + E ) e. RR+ )
287	285 286	ltdivgt1	|- ( ( ph /\ Y =/= (/) ) -> ( 1 < ( 1 + E ) <-> ( G / ( 1 + E ) ) < G ) )
288	252 287	mpbid	|- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) < G )
289	288	adantr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) < G )
290	23	adantr	|- ( ( 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 ) ) )
291		fvexd	|- ( ph -> ( x ` k ) e. _V )
292	19	elexd	|- ( ph -> S e. _V )
293	291 292	ifcld	|- ( ph -> if ( k e. Y , ( x ` k ) , S ) e. _V )
294	293	ralrimivw	|- ( ph -> A. k e. W if ( k e. Y , ( x ` k ) , S ) e. _V )
295	294	adantr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> A. k e. W if ( k e. Y , ( x ` k ) , S ) e. _V )
296		eqid	|- ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) )
297	296	fnmpt	|- ( 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 )
298	295 297	syl	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) Fn W )
299		simpr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
300		mptexg	|- ( W e. Fin -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
301	70 300	syl	|- ( ph -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
302	301	adantr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) e. _V )
303	24	fvmpt2	|- ( ( 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 ) ) )
304	299 302 303	syl2anc	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
305	304	fneq1d	|- ( ( 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 ) )
306	298 305	mpbird	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) Fn W )
307		nfv	|- F/ k ph
308		nfcv	|- F/_ k x
309		nfixp1	|- F/_ k X_ k e. Y ( ( A ` k ) [,) ( B ` k ) )
310	308 309	nfel	|- F/ k x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) )
311	307 310	nfan	|- F/ k ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
312	304	fveq1d	|- ( ( 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 ) )
313	312	adantr	|- ( ( ( 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 ) )
314		simpr	|- ( ( ph /\ k e. W ) -> k e. W )
315	293	adantr	|- ( ( ph /\ k e. W ) -> if ( k e. Y , ( x ` k ) , S ) e. _V )
316	296	fvmpt2	|- ( ( 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 ) )
317	314 315 316	syl2anc	|- ( ( ph /\ k e. W ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
318	317	adantlr	|- ( ( ( 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 ) )
319	313 318	eqtrd	|- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
320		iftrue	|- ( k e. Y -> if ( k e. Y , ( x ` k ) , S ) = ( x ` k ) )
321	320	adantl	|- ( ( ( ( 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 ) )
322		vex	|- x e. _V
323	322	elixp	|- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) <-> ( x Fn Y /\ A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
324	323	simprbi	|- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) -> A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
325	324	adantr	|- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
326		simpr	|- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> k e. Y )
327		rspa	|- ( ( A. k e. Y ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
328	325 326 327	syl2anc	|- ( ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
329	328	ad4ant24	|- ( ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) /\ k e. Y ) -> ( x ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
330	321 329	eqeltrd	|- ( ( ( ( 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 ) ) )
331		snidg	|- ( Z e. ( X \ Y ) -> Z e. { Z } )
332	4 331	syl	|- ( ph -> Z e. { Z } )
333		elun2	|- ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
334	332 333	syl	|- ( ph -> Z e. ( Y u. { Z } ) )
335	72	a1i	|- ( ph -> ( Y u. { Z } ) = W )
336	334 335	eleqtrd	|- ( ph -> Z e. W )
337	6 336	ffvelcdmd	|- ( ph -> ( A ` Z ) e. RR )
338	337	rexrd	|- ( ph -> ( A ` Z ) e. RR* )
339	7 336	ffvelcdmd	|- ( ph -> ( B ` Z ) e. RR )
340	339	rexrd	|- ( ph -> ( B ` Z ) e. RR* )
341		iccssxr	|- ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR*
342		ssrab2	|- { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
343	18 342	eqsstri	|- U C_ ( ( A ` Z ) [,] ( B ` Z ) )
344	343 19	sselid	|- ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
345	341 344	sselid	|- ( ph -> S e. RR* )
346		iccgelb	|- ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ S )
347	338 340 344 346	syl3anc	|- ( ph -> ( A ` Z ) <_ S )
348	338 340 345 347 20	elicod	|- ( ph -> S e. ( ( A ` Z ) [,) ( B ` Z ) ) )
349	348	ad2antrr	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> S e. ( ( A ` Z ) [,) ( B ` Z ) ) )
350		iffalse	|- ( -. k e. Y -> if ( k e. Y , ( x ` k ) , S ) = S )
351	350	adantl	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) = S )
352	5	eleq2i	|- ( k e. W <-> k e. ( Y u. { Z } ) )
353	352	birani	|- ( ( k e. W /\ -. k e. Y ) -> k e. ( Y u. { Z } ) )
354		simpr	|- ( ( k e. W /\ -. k e. Y ) -> -. k e. Y )
355		elunnel1	|- ( ( k e. ( Y u. { Z } ) /\ -. k e. Y ) -> k e. { Z } )
356	353 354 355	syl2anc	|- ( ( k e. W /\ -. k e. Y ) -> k e. { Z } )
357		elsni	|- ( k e. { Z } -> k = Z )
358	356 357	syl	|- ( ( k e. W /\ -. k e. Y ) -> k = Z )
359		fveq2	|- ( k = Z -> ( A ` k ) = ( A ` Z ) )
360		fveq2	|- ( k = Z -> ( B ` k ) = ( B ` Z ) )
361	359 360	oveq12d	|- ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
362	358 361	syl	|- ( ( k e. W /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
363	362	adantll	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
364	351 363	eleq12d	|- ( ( ( 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	349 364	mpbird	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
366	365	adantllr	|- ( ( ( ( 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	330 366	pm2.61dan	|- ( ( ( 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	319 367	eqeltrd	|- ( ( ( 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	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W -> ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
370	311 369	ralrimi	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
371	306 370	jca	|- ( ( 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	|- ( O ` x ) e. _V
373	372	elixp	|- ( ( 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	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) e. X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) )
375	290 374	sseldd	|- ( ( 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	|- ( ( 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	|- ( ( 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	|- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) -> x Fn Y )
379	378	adantl	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x Fn Y )
380	379	ad2antrr	|- ( ( ( ( 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	|- F/ k j e. NN
382	311 381	nfan	|- F/ k ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN )
383		nfcv	|- F/_ k ( O ` x )
384		nfixp1	|- F/_ k X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
385	383 384	nfel	|- F/ k ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
386	382 385	nfan	|- 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	312	3adant3	|- ( ( 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	293	adantr	|- ( ( ph /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. _V )
389	267 388 316	syl2anc	|- ( ( 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	|- ( ( 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	320	3ad2ant3	|- ( ( 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	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) = ( ( O ` x ) ` k ) )
393	392	ad5ant125	|- ( ( ( ( ( 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	372	elixp	|- ( ( 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 ) ) ) )
395	394	birani	|- ( ( ( 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 ) ) ) )
396	395	simprd	|- ( ( ( 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 ) ) )
397	266	adantl	|- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> k e. W )
398		rspa	|- ( ( 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 ) ) )
399	396 397 398	syl2anc	|- ( ( ( 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 ) ) )
400	399	adantll	|- ( ( ( ( ( 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 ) ) )
401	393 400	eqeltrd	|- ( ( ( ( ( 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 ) ) )
402	51	ad3antrrr	|- ( ( ( ( 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 )
403	59	ad2antlr	|- ( ( ( ( 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 )
404	304	fveq1d	|- ( ( 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 ) )
405		eqidd	|- ( ph -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
406		eleq1	|- ( k = Z -> ( k e. Y <-> Z e. Y ) )
407		fveq2	|- ( k = Z -> ( x ` k ) = ( x ` Z ) )
408	406 407	ifbieq1d	|- ( k = Z -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
409	408	adantl	|- ( ( ph /\ k = Z ) -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
410		fvexd	|- ( ph -> ( x ` Z ) e. _V )
411	410 292	ifcld	|- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) e. _V )
412	405 409 336 411	fvmptd	|- ( ph -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` Z ) = if ( Z e. Y , ( x ` Z ) , S ) )
413	412	adantr	|- ( ( 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 ) )
414	4	eldifbd	|- ( ph -> -. Z e. Y )
415	414	iffalsed	|- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) = S )
416	415	adantr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> if ( Z e. Y , ( x ` Z ) , S ) = S )
417	404 413 416	3eqtrrd	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> S = ( ( O ` x ) ` Z ) )
418	417	ad2antrr	|- ( ( ( ( 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 ) )
419	402 336	syl	|- ( ( ( ( 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 )
420	394	simprbi	|- ( ( 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 ) ) )
421	420	adantl	|- ( ( ( ( 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 ) ) )
422		fveq2	|- ( k = Z -> ( ( O ` x ) ` k ) = ( ( O ` x ) ` Z ) )
423		fveq2	|- ( k = Z -> ( ( C ` j ) ` k ) = ( ( C ` j ) ` Z ) )
424		fveq2	|- ( k = Z -> ( ( D ` j ) ` k ) = ( ( D ` j ) ` Z ) )
425	423 424	oveq12d	|- ( k = Z -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
426	422 425	eleq12d	|- ( k = Z -> ( ( ( O ` x ) ` k ) e. ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) <-> ( ( O ` x ) ` Z ) e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) )
427	426	rspcva	|- ( ( 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 ) ) )
428	419 421 427	syl2anc	|- ( ( ( ( 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 ) ) )
429	418 428	eqeltrd	|- ( ( ( ( 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 ) ) )
430	161	3adant3	|- ( ( 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 ) )
431	77	3ad2ant3	|- ( ( 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 ) )
432	430 431	eqtrd	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = ( ( C ` j ) |` Y ) )
433	432	fveq1d	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
434	402 403 429 433	syl3anc	|- ( ( ( ( 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 ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
435	434	adantr	|- ( ( ( ( ( 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 ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
436		fvres	|- ( k e. Y -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
437	436	adantl	|- ( ( ( ( ( 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 ) -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
438	435 437	eqtrd	|- ( ( ( ( ( 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 ) -> ( ( J ` j ) ` k ) = ( ( C ` j ) ` k ) )
439	120	elexd	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
440	13	fvmpt2	|- ( ( j e. NN /\ if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
441	151 439 440	syl2anc	|- ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
442	441	3adant3	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
443	107	3ad2ant3	|- ( ( 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 ) )
444	442 443	eqtrd	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = ( ( D ` j ) |` Y ) )
445	444	fveq1d	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
446	402 403 429 445	syl3anc	|- ( ( ( ( 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 ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
447	446	adantr	|- ( ( ( ( ( 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 ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
448		fvres	|- ( k e. Y -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
449	448	adantl	|- ( ( ( ( ( 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 ) -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
450	447 449	eqtrd	|- ( ( ( ( ( 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 ) -> ( ( K ` j ) ` k ) = ( ( D ` j ) ` k ) )
451	438 450	oveq12d	|- ( ( ( ( ( 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 ) -> ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
452	451	eqcomd	|- ( ( ( ( ( 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 ) -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
453	401 452	eleqtrd	|- ( ( ( ( ( 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. ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
454	453	ex	|- ( ( ( ( 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. ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
455	386 454	ralrimi	|- ( ( ( ( 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. Y ( x ` k ) e. ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
456	380 455	jca	|- ( ( ( ( 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 /\ A. k e. Y ( x ` k ) e. ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
457	322	elixp	|- ( x e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) <-> ( x Fn Y /\ A. k e. Y ( x ` k ) e. ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
458	456 457	sylibr	|- ( ( ( ( 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 e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
459	458	ex	|- ( ( ( 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 e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
460	459	reximdva	|- ( ( 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 ) ) -> E. j e. NN x e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
461	377 460	mpd	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> E. j e. NN x e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
462		eliun	|- ( x e. U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) <-> E. j e. NN x e. X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
463	461 462	sylibr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x e. U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
464	463	ralrimiva	|- ( ph -> A. x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) x e. U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
465		dfss3	|- ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) <-> A. x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) x e. U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
466	464 465	sylibr	|- ( ph -> X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
467		ovexd	|- ( ph -> ( RR ^m Y ) e. _V )
468	237	a1i	|- ( ph -> NN e. _V )
469	467 468	elmapd	|- ( ph -> ( K e. ( ( RR ^m Y ) ^m NN ) <-> K : NN --> ( RR ^m Y ) ) )
470	121 469	mpbird	|- ( ph -> K e. ( ( RR ^m Y ) ^m NN ) )
471	467 468	elmapd	|- ( ph -> ( J e. ( ( RR ^m Y ) ^m NN ) <-> J : NN --> ( RR ^m Y ) ) )
472	103 471	mpbird	|- ( ph -> J e. ( ( RR ^m Y ) ^m NN ) )
473	97 87	elmapd	|- ( ph -> ( ( B |` Y ) e. ( RR ^m Y ) <-> ( B |` Y ) : Y --> RR ) )
474	213 473	mpbird	|- ( ph -> ( B |` Y ) e. ( RR ^m Y ) )
475	97 87	elmapd	|- ( ph -> ( ( A |` Y ) e. ( RR ^m Y ) <-> ( A |` Y ) : Y --> RR ) )
476	212 475	mpbird	|- ( ph -> ( A |` Y ) e. ( RR ^m Y ) )
477		fveq1	|- ( e = ( A |` Y ) -> ( e ` k ) = ( ( A |` Y ) ` k ) )
478	477	adantr	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( e ` k ) = ( ( A |` Y ) ` k ) )
479	259	adantl	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( ( A |` Y ) ` k ) = ( A ` k ) )
480	478 479	eqtrd	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( e ` k ) = ( A ` k ) )
481	480	oveq1d	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( ( e ` k ) [,) ( f ` k ) ) = ( ( A ` k ) [,) ( f ` k ) ) )
482	481	ixpeq2dva	|- ( e = ( A |` Y ) -> X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) = X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) )
483	482	sseq1d	|- ( e = ( A |` Y ) -> ( X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) <-> X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) ) )
484		oveq1	|- ( e = ( A |` Y ) -> ( e ( L ` Y ) f ) = ( ( A |` Y ) ( L ` Y ) f ) )
485	484	breq1d	|- ( e = ( A |` Y ) -> ( ( e ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) <-> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
486	483 485	imbi12d	|- ( e = ( A |` Y ) -> ( ( 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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
487	486	ralbidv	|- ( e = ( A |` Y ) -> ( 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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
488	487	ralbidv	|- ( e = ( A |` 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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
489	488	ralbidv	|- ( e = ( A |` 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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> 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 ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
490	489	rspcva	|- ( ( ( A |` Y ) e. ( RR ^m Y ) /\ 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 ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) -> 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 ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
491	476 22 490	syl2anc	|- ( ph -> 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 ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
492		fveq1	|- ( f = ( B |` Y ) -> ( f ` k ) = ( ( B |` Y ) ` k ) )
493	492	adantr	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( f ` k ) = ( ( B |` Y ) ` k ) )
494	260	adantl	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( ( B |` Y ) ` k ) = ( B ` k ) )
495	493 494	eqtrd	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( f ` k ) = ( B ` k ) )
496	495	oveq2d	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( ( A ` k ) [,) ( f ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
497	496	ixpeq2dva	|- ( f = ( B |` Y ) -> X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) = X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
498	497	sseq1d	|- ( f = ( B |` Y ) -> ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) <-> X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) ) )
499		oveq2	|- ( f = ( B |` Y ) -> ( ( A |` Y ) ( L ` Y ) f ) = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
500	499	breq1d	|- ( f = ( B |` Y ) -> ( ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) <-> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
501	498 500	imbi12d	|- ( f = ( B |` Y ) -> ( ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
502	501	ralbidv	|- ( f = ( B |` Y ) -> ( A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
503	502	ralbidv	|- ( f = ( B |` Y ) -> ( A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
504	503	rspcva	|- ( ( ( B |` Y ) 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 ( ( A ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) -> A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
505	474 491 504	syl2anc	|- ( ph -> A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
506		fveq1	|- ( g = J -> ( g ` j ) = ( J ` j ) )
507	506	fveq1d	|- ( g = J -> ( ( g ` j ) ` k ) = ( ( J ` j ) ` k ) )
508	507	oveq1d	|- ( g = J -> ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
509	508	ixpeq2dv	|- ( g = J -> X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
510	509	iuneq2d	|- ( g = J -> U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
511	510	sseq2d	|- ( g = J -> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) <-> X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) ) )
512	506	oveq1d	|- ( g = J -> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) = ( ( J ` j ) ( L ` Y ) ( h ` j ) ) )
513	512	mpteq2dv	|- ( g = J -> ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) )
514	513	fveq2d	|- ( g = J -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) )
515	514	breq2d	|- ( g = J -> ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) <-> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
516	511 515	imbi12d	|- ( g = J -> ( ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
517	516	ralbidv	|- ( g = J -> ( A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) )
518	517	rspcva	|- ( ( J e. ( ( RR ^m Y ) ^m NN ) /\ A. g e. ( ( RR ^m Y ) ^m NN ) A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) -> A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
519	472 505 518	syl2anc	|- ( ph -> A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) )
520		fveq1	|- ( h = K -> ( h ` j ) = ( K ` j ) )
521	520	fveq1d	|- ( h = K -> ( ( h ` j ) ` k ) = ( ( K ` j ) ` k ) )
522	521	oveq2d	|- ( h = K -> ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
523	522	ixpeq2dv	|- ( h = K -> X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
524	523	iuneq2d	|- ( h = K -> U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
525	524	sseq2d	|- ( h = K -> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) <-> X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) ) )
526	520	oveq2d	|- ( h = K -> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
527	526	mpteq2dv	|- ( h = K -> ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) )
528	527	fveq2d	|- ( h = K -> ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
529	528	breq2d	|- ( h = K -> ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) <-> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) )
530	525 529	imbi12d	|- ( h = K -> ( ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) <-> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) ) )
531	530	rspcva	|- ( ( K e. ( ( RR ^m Y ) ^m NN ) /\ A. h e. ( ( RR ^m Y ) ^m NN ) ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) ) ) -> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) )
532	470 519 531	syl2anc	|- ( ph -> ( X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) )
533	466 532	mpd	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
534		idd	|- ( ph -> ( ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) )
535	533 534	mpd	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
536	535	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
537	62	adantl	|- ( ( ( ph /\ Y =/= (/) ) /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
538	537	mpteq2dva	|- ( ( ph /\ Y =/= (/) ) -> ( j e. NN |-> ( P ` j ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) )
539	538	fveq2d	|- ( ( ph /\ Y =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
540	258 539	breq12d	|- ( ( ph /\ Y =/= (/) ) -> ( G <_ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) <-> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) ) )
541	536 540	mpbird	|- ( ( ph /\ Y =/= (/) ) -> G <_ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
542	541	adantr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G <_ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
543	247 249 250 289 542	ltletrd	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
544	235 246 543	syl2anc	|- ( ( ( ph /\ Y =/= (/) ) /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
545	234 544	pm2.61dan	|- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
546	207 208 209 210 227 545	sge0uzfsumgt	|- ( ( ph /\ Y =/= (/) ) -> E. m e. NN ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) )
547	226	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) e. RR )
548		fzfid	|- ( ph -> ( 1 ... m ) e. Fin )
549		simpl	|- ( ( ph /\ j e. ( 1 ... m ) ) -> ph )
550		elfznn	|- ( j e. ( 1 ... m ) -> j e. NN )
551	550	adantl	|- ( ( ph /\ j e. ( 1 ... m ) ) -> j e. NN )
552	50 126	sselid	|- ( ( ph /\ j e. NN ) -> ( P ` j ) e. RR )
553	549 551 552	syl2anc	|- ( ( ph /\ j e. ( 1 ... m ) ) -> ( P ` j ) e. RR )
554	548 553	fsumrecl	|- ( ph -> sum_ j e. ( 1 ... m ) ( P ` j ) e. RR )
555	554	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> sum_ j e. ( 1 ... m ) ( P ` j ) e. RR )
556		simpr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) )
557	547 555 556	ltled	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) <_ sum_ j e. ( 1 ... m ) ( P ` j ) )
558	216	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G e. RR )
559	222	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( 1 + E ) e. RR+ )
560	558 555 559	ledivmuld	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( ( G / ( 1 + E ) ) <_ sum_ j e. ( 1 ... m ) ( P ` j ) <-> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
561	557 560	mpbid	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
562	561	ex	|- ( ph -> ( ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
563	562	adantr	|- ( ( ph /\ m e. NN ) -> ( ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
564	563	adantlr	|- ( ( ( ph /\ Y =/= (/) ) /\ m e. NN ) -> ( ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
565	564	reximdva	|- ( ( ph /\ Y =/= (/) ) -> ( E. m e. NN ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
566	546 565	mpd	|- ( ( ph /\ Y =/= (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
567	204 206 566	syl2anc	|- ( ( ph /\ -. Y = (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
568	203 567	pm2.61dan	|- ( ph -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
569	2	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> X e. Fin )
570	3	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> Y C_ X )
571	4	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> Z e. ( X \ Y ) )
572	6	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> A : W --> RR )
573	7	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> B : W --> RR )
574	10	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> C : NN --> ( RR ^m W ) )
575		eqid	|- ( y e. Y |-> 0 ) = ( y e. Y |-> 0 )
576		eqid	|- ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
577	12	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> D : NN --> ( RR ^m W ) )
578		eqid	|- ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) = ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
579		fveq2	|- ( i = j -> ( C ` i ) = ( C ` j ) )
580		fveq2	|- ( i = j -> ( D ` i ) = ( D ` j ) )
581	579 580	oveq12d	|- ( i = j -> ( ( C ` i ) ( L ` W ) ( D ` i ) ) = ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
582	581	cbvmptv	|- ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
583	582	fveq2i	|- ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) )
584	583 14	eqeltrid	|- ( ph -> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
585	584	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
586		eleq1w	|- ( j = i -> ( j e. Y <-> i e. Y ) )
587		fveq2	|- ( j = i -> ( c ` j ) = ( c ` i ) )
588	587	breq1d	|- ( j = i -> ( ( c ` j ) <_ x <-> ( c ` i ) <_ x ) )
589	588 587	ifbieq1d	|- ( j = i -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` i ) <_ x , ( c ` i ) , x ) )
590	586 587 589	ifbieq12d	|- ( j = i -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) )
591	590	cbvmptv	|- ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) )
592	591	mpteq2i	|- ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) = ( c e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) )
593	592	mpteq2i	|- ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) ) ) = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) ) )
594	15 593	eqtri	|- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( i e. W |-> if ( i e. Y , ( c ` i ) , if ( ( c ` i ) <_ x , ( c ` i ) , x ) ) ) ) )
595	17	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> E e. RR+ )
596		fveq2	|- ( j = i -> ( C ` j ) = ( C ` i ) )
597		fveq2	|- ( j = i -> ( D ` j ) = ( D ` i ) )
598	597	fveq2d	|- ( j = i -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` z ) ` ( D ` i ) ) )
599	596 598	oveq12d	|- ( j = i -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) )
600	599	cbvmptv	|- ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) )
601	600	fveq2i	|- ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) ) )
602	601	oveq2i	|- ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) ) ) )
603	602	breq2i	|- ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) ) ) ) )
604	603	rabbii	|- { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) ) ) ) }
605	18 604	eqtri	|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) ) ) ) }
606	19	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> S e. U )
607	20	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> S < ( B ` Z ) )
608		eqid	|- ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) = ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) )
609		simp2	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> m e. NN )
610		id	|- ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
611		fveq2	|- ( j = i -> ( P ` j ) = ( P ` i ) )
612	611	cbvsumv	|- sum_ j e. ( 1 ... m ) ( P ` j ) = sum_ i e. ( 1 ... m ) ( P ` i )
613	612	oveq2i	|- ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) = ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) )
614	613	a1i	|- ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) = ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) ) )
615	610 614	breqtrd	|- ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) ) )
616	615	3ad2ant3	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> G <_ ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) ) )
617		simpl	|- ( ( ph /\ i e. ( 1 ... m ) ) -> ph )
618		elfznn	|- ( i e. ( 1 ... m ) -> i e. NN )
619	618	adantl	|- ( ( ph /\ i e. ( 1 ... m ) ) -> i e. NN )
620		eleq1w	|- ( j = i -> ( j e. NN <-> i e. NN ) )
621		fveq2	|- ( j = i -> ( J ` j ) = ( J ` i ) )
622		fveq2	|- ( j = i -> ( K ` j ) = ( K ` i ) )
623	621 622	oveq12d	|- ( j = i -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
624	611 623	eqeq12d	|- ( j = i -> ( ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) <-> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) ) )
625	620 624	imbi12d	|- ( j = i -> ( ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) <-> ( i e. NN -> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) ) ) )
626	625 62	chvarvv	|- ( i e. NN -> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
627	626	adantl	|- ( ( ph /\ i e. NN ) -> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
628	620	anbi2d	|- ( j = i -> ( ( ph /\ j e. NN ) <-> ( ph /\ i e. NN ) ) )
629	596	fveq1d	|- ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
630	597	fveq1d	|- ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
631	629 630	oveq12d	|- ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
632	631	eleq2d	|- ( j = i -> ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
633	596	reseq1d	|- ( j = i -> ( ( C ` j ) |` Y ) = ( ( C ` i ) |` Y ) )
634	632 633	ifbieq1d	|- ( j = i -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
635	621 634	eqeq12d	|- ( j = i -> ( ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) <-> ( J ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ) )
636	628 635	imbi12d	|- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) ) <-> ( ( ph /\ i e. NN ) -> ( J ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ) ) )
637	636 161	chvarvv	|- ( ( ph /\ i e. NN ) -> ( J ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
638	597	reseq1d	|- ( j = i -> ( ( D ` j ) |` Y ) = ( ( D ` i ) |` Y ) )
639	632 638	ifbieq1d	|- ( j = i -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) )
640	622 639	eqeq12d	|- ( j = i -> ( ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) <-> ( K ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) )
641	628 640	imbi12d	|- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) ) <-> ( ( ph /\ i e. NN ) -> ( K ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) ) )
642	641 441	chvarvv	|- ( ( ph /\ i e. NN ) -> ( K ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) )
643	637 642	oveq12d	|- ( ( ph /\ i e. NN ) -> ( ( J ` i ) ( L ` Y ) ( K ` i ) ) = ( if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ( L ` Y ) if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) )
644	627 643	eqtrd	|- ( ( ph /\ i e. NN ) -> ( P ` i ) = ( if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ( L ` Y ) if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) )
645		simpr	|- ( ( ph /\ i e. NN ) -> i e. NN )
646		ovexd	|- ( ( ph /\ i e. NN ) -> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) e. _V )
647	608	fvmpt2	|- ( ( i e. NN /\ ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) e. _V ) -> ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) = ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) )
648	645 646 647	syl2anc	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) = ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) )
649		fvex	|- ( C ` i ) e. _V
650	649	resex	|- ( ( C ` i ) |` Y ) e. _V
651	650	a1i	|- ( ph -> ( ( C ` i ) |` Y ) e. _V )
652	9 155	eqeltrrid	|- ( ph -> ( y e. Y |-> 0 ) e. _V )
653	651 652	ifcld	|- ( ph -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
654	653	adantr	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
655	576	fvmpt2	|- ( ( i e. NN /\ if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
656	645 654 655	syl2anc	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
657	9	eqcomi	|- ( y e. Y |-> 0 ) = F
658		ifeq2	|- ( ( y e. Y |-> 0 ) = F -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
659	657 658	ax-mp	|- if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F )
660	659	a1i	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
661	656 660	eqtrd	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
662		fvex	|- ( D ` i ) e. _V
663	662	resex	|- ( ( D ` i ) |` Y ) e. _V
664	663	a1i	|- ( ph -> ( ( D ` i ) |` Y ) e. _V )
665	664 652	ifcld	|- ( ph -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
666	665	adantr	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
667	578	fvmpt2	|- ( ( i e. NN /\ if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
668	645 666 667	syl2anc	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) )
669		biid	|- ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
670	669 657	ifbieq2i	|- if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F )
671	670	a1i	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) )
672	668 671	eqtrd	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) )
673	661 672	oveq12d	|- ( ( ph /\ i e. NN ) -> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) = ( if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ( L ` Y ) if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) )
674	648 673	eqtrd	|- ( ( ph /\ i e. NN ) -> ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) = ( if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) ( L ` Y ) if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) ) )
675	644 674	eqtr4d	|- ( ( ph /\ i e. NN ) -> ( P ` i ) = ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) )
676	617 619 675	syl2anc	|- ( ( ph /\ i e. ( 1 ... m ) ) -> ( P ` i ) = ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) )
677	676	3ad2antl1	|- ( ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) /\ i e. ( 1 ... m ) ) -> ( P ` i ) = ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) )
678	677	sumeq2dv	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> sum_ i e. ( 1 ... m ) ( P ` i ) = sum_ i e. ( 1 ... m ) ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) )
679	678	oveq2d	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) ) = ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) ) )
680	616 679	breqtrd	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> G <_ ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( ( i e. NN |-> ( ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ( L ` Y ) ( ( i e. NN |-> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) ) ` i ) ) ) ` i ) ) )
681		fveq2	|- ( j = h -> ( D ` j ) = ( D ` h ) )
682	681	fveq1d	|- ( j = h -> ( ( D ` j ) ` Z ) = ( ( D ` h ) ` Z ) )
683	682	cbvmptv	|- ( j e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) = ( h e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` h ) ` Z ) )
684	683	rneqi	|- ran ( j e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) = ran ( h e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` h ) ` Z ) )
685		fveq2	|- ( h = i -> ( C ` h ) = ( C ` i ) )
686	685	fveq1d	|- ( h = i -> ( ( C ` h ) ` Z ) = ( ( C ` i ) ` Z ) )
687		fveq2	|- ( h = i -> ( D ` h ) = ( D ` i ) )
688	687	fveq1d	|- ( h = i -> ( ( D ` h ) ` Z ) = ( ( D ` i ) ` Z ) )
689	686 688	oveq12d	|- ( h = i -> ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
690	689	eleq2d	|- ( h = i -> ( S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
691	690	cbvrabv	|- { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } = { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) }
692	691	mpteq1i	|- ( j e. { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) = ( j e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) )
693	692	rneqi	|- ran ( j e. { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) = ran ( j e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) )
694	693	uneq2i	|- ( { ( B ` Z ) } u. ran ( j e. { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) ) = ( { ( B ` Z ) } u. ran ( j e. { i e. ( 1 ... m ) | S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) )
695		eqid	|- inf ( ( { ( B ` Z ) } u. ran ( j e. { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) ) , RR , < ) = inf ( ( { ( B ` Z ) } u. ran ( j e. { h e. ( 1 ... m ) | S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) } |-> ( ( D ` j ) ` Z ) ) ) , RR , < )
696	1 569 570 571 5 572 573 574 575 576 577 578 585 594 16 595 605 606 607 608 609 680 684 694 695	hoidmvlelem2	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> E. u e. U S < u )
697	696	3exp	|- ( ph -> ( m e. NN -> ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> E. u e. U S < u ) ) )
698	697	rexlimdv	|- ( ph -> ( E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> E. u e. U S < u ) )
699	568 698	mpd	|- ( ph -> E. u e. U S < u )