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	biimpi	|- ( k e. W -> k e. ( Y u. { Z } ) )
354	353	adantr	|- ( ( k e. W /\ -. k e. Y ) -> k e. ( Y u. { Z } ) )
355		simpr	|- ( ( k e. W /\ -. k e. Y ) -> -. k e. Y )
356		elunnel1	|- ( ( k e. ( Y u. { Z } ) /\ -. k e. Y ) -> k e. { Z } )
357	354 355 356	syl2anc	|- ( ( k e. W /\ -. k e. Y ) -> k e. { Z } )
358		elsni	|- ( k e. { Z } -> k = Z )
359	357 358	syl	|- ( ( k e. W /\ -. k e. Y ) -> k = Z )
360		fveq2	|- ( k = Z -> ( A ` k ) = ( A ` Z ) )
361		fveq2	|- ( k = Z -> ( B ` k ) = ( B ` Z ) )
362	360 361	oveq12d	|- ( k = Z -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
363	359 362	syl	|- ( ( k e. W /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
364	363	adantll	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> ( ( A ` k ) [,) ( B ` k ) ) = ( ( A ` Z ) [,) ( B ` Z ) ) )
365	351 364	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 ) ) ) )
366	349 365	mpbird	|- ( ( ( ph /\ k e. W ) /\ -. k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. ( ( A ` k ) [,) ( B ` k ) ) )
367	366	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 ) ) )
368	330 367	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 ) ) )
369	319 368	eqeltrd	|- ( ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ k e. W ) -> ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
370	369	ex	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( k e. W -> ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) ) )
371	311 370	ralrimi	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> A. k e. W ( ( O ` x ) ` k ) e. ( ( A ` k ) [,) ( B ` k ) ) )
372	306 371	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 ) ) ) )
373		fvex	|- ( O ` x ) e. _V
374	373	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 ) ) ) )
375	372 374	sylibr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> ( O ` x ) e. X_ k e. W ( ( A ` k ) [,) ( B ` k ) ) )
376	290 375	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 ) ) )
377		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 ) ) )
378	376 377	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 ) ) )
379		ixpfn	|- ( x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) -> x Fn Y )
380	379	adantl	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> x Fn Y )
381	380	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 )
382		nfv	|- F/ k j e. NN
383	311 382	nfan	|- F/ k ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) /\ j e. NN )
384		nfcv	|- F/_ k ( O ` x )
385		nfixp1	|- F/_ k X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
386	384 385	nfel	|- F/ k ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) )
387	383 386	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 ) ) )
388	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 ) )
389	293	adantr	|- ( ( ph /\ k e. Y ) -> if ( k e. Y , ( x ` k ) , S ) e. _V )
390	267 389 316	syl2anc	|- ( ( ph /\ k e. Y ) -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` k ) = if ( k e. Y , ( x ` k ) , S ) )
391	390	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 ) )
392	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 ) )
393	388 391 392	3eqtrrd	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) /\ k e. Y ) -> ( x ` k ) = ( ( O ` x ) ` k ) )
394	393	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 ) )
395		simpl	|- ( ( ( 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 ) ) )
396	373	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 ) ) ) )
397	395 396	sylib	|- ( ( ( 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 ) ) ) )
398	397	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 ) ) )
399	266	adantl	|- ( ( ( O ` x ) e. X_ k e. W ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) /\ k e. Y ) -> k e. W )
400		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 ) ) )
401	398 399 400	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 ) ) )
402	401	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 ) ) )
403	394 402	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 ) ) )
404	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 )
405	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 )
406	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 ) )
407		eqidd	|- ( ph -> ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) = ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) )
408		eleq1	|- ( k = Z -> ( k e. Y <-> Z e. Y ) )
409		fveq2	|- ( k = Z -> ( x ` k ) = ( x ` Z ) )
410	408 409	ifbieq1d	|- ( k = Z -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
411	410	adantl	|- ( ( ph /\ k = Z ) -> if ( k e. Y , ( x ` k ) , S ) = if ( Z e. Y , ( x ` Z ) , S ) )
412		fvexd	|- ( ph -> ( x ` Z ) e. _V )
413	412 292	ifcld	|- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) e. _V )
414	407 411 336 413	fvmptd	|- ( ph -> ( ( k e. W |-> if ( k e. Y , ( x ` k ) , S ) ) ` Z ) = if ( Z e. Y , ( x ` Z ) , S ) )
415	414	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 ) )
416	4	eldifbd	|- ( ph -> -. Z e. Y )
417	416	iffalsed	|- ( ph -> if ( Z e. Y , ( x ` Z ) , S ) = S )
418	417	adantr	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> if ( Z e. Y , ( x ` Z ) , S ) = S )
419	406 415 418	3eqtrrd	|- ( ( ph /\ x e. X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) ) -> S = ( ( O ` x ) ` Z ) )
420	419	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 ) )
421	404 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 )
422	396	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 ) ) )
423	422	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 ) ) )
424		fveq2	|- ( k = Z -> ( ( O ` x ) ` k ) = ( ( O ` x ) ` Z ) )
425		fveq2	|- ( k = Z -> ( ( C ` j ) ` k ) = ( ( C ` j ) ` Z ) )
426		fveq2	|- ( k = Z -> ( ( D ` j ) ` k ) = ( ( D ` j ) ` Z ) )
427	425 426	oveq12d	|- ( k = Z -> ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) = ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) )
428	424 427	eleq12d	|- ( 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	|- ( ( 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	|- ( ( ( ( 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	|- ( ( ( ( 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	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 ) )
433	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 ) )
434	432 433	eqtrd	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( J ` j ) = ( ( C ` j ) |` Y ) )
435	434	fveq1d	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( J ` j ) ` k ) = ( ( ( C ` j ) |` Y ) ` k ) )
436	404 405 431 435	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 ) )
437	436	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 ) )
438		fvres	|- ( k e. Y -> ( ( ( C ` j ) |` Y ) ` k ) = ( ( C ` j ) ` k ) )
439	438	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 ) )
440	437 439	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 ) )
441	120	elexd	|- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
442	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 ) )
443	151 441 442	syl2anc	|- ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
444	443	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 ) )
445	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 ) )
446	444 445	eqtrd	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( K ` j ) = ( ( D ` j ) |` Y ) )
447	446	fveq1d	|- ( ( ph /\ j e. NN /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( K ` j ) ` k ) = ( ( ( D ` j ) |` Y ) ` k ) )
448	404 405 431 447	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 ) )
449	448	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 ) )
450		fvres	|- ( k e. Y -> ( ( ( D ` j ) |` Y ) ` k ) = ( ( D ` j ) ` k ) )
451	450	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 ) )
452	449 451	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 ) )
453	440 452	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 ) ) )
454	453	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 ) ) )
455	403 454	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 ) ) )
456	455	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 ) ) ) )
457	387 456	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 ) ) )
458	381 457	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 ) ) ) )
459	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 ) ) ) )
460	458 459	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 ) ) )
461	460	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 ) ) ) )
462	461	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 ) ) ) )
463	378 462	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 ) ) )
464		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 ) ) )
465	463 464	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 ) ) )
466	465	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 ) ) )
467		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 ) ) )
468	466 467	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 ) ) )
469		ovexd	|- ( ph -> ( RR ^m Y ) e. _V )
470	237	a1i	|- ( ph -> NN e. _V )
471	469 470	elmapd	|- ( ph -> ( K e. ( ( RR ^m Y ) ^m NN ) <-> K : NN --> ( RR ^m Y ) ) )
472	121 471	mpbird	|- ( ph -> K e. ( ( RR ^m Y ) ^m NN ) )
473	469 470	elmapd	|- ( ph -> ( J e. ( ( RR ^m Y ) ^m NN ) <-> J : NN --> ( RR ^m Y ) ) )
474	103 473	mpbird	|- ( ph -> J e. ( ( RR ^m Y ) ^m NN ) )
475	97 87	elmapd	|- ( ph -> ( ( B |` Y ) e. ( RR ^m Y ) <-> ( B |` Y ) : Y --> RR ) )
476	213 475	mpbird	|- ( ph -> ( B |` Y ) e. ( RR ^m Y ) )
477	97 87	elmapd	|- ( ph -> ( ( A |` Y ) e. ( RR ^m Y ) <-> ( A |` Y ) : Y --> RR ) )
478	212 477	mpbird	|- ( ph -> ( A |` Y ) e. ( RR ^m Y ) )
479		fveq1	|- ( e = ( A |` Y ) -> ( e ` k ) = ( ( A |` Y ) ` k ) )
480	479	adantr	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( e ` k ) = ( ( A |` Y ) ` k ) )
481	259	adantl	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( ( A |` Y ) ` k ) = ( A ` k ) )
482	480 481	eqtrd	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( e ` k ) = ( A ` k ) )
483	482	oveq1d	|- ( ( e = ( A |` Y ) /\ k e. Y ) -> ( ( e ` k ) [,) ( f ` k ) ) = ( ( A ` k ) [,) ( f ` k ) ) )
484	483	ixpeq2dva	|- ( e = ( A |` Y ) -> X_ k e. Y ( ( e ` k ) [,) ( f ` k ) ) = X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) )
485	484	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 ) ) ) )
486		oveq1	|- ( e = ( A |` Y ) -> ( e ( L ` Y ) f ) = ( ( A |` Y ) ( L ` Y ) f ) )
487	486	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 ) ) ) ) ) )
488	485 487	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 ) ) ) ) ) ) )
489	488	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 ) ) ) ) ) ) )
490	489	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 ) ) ) ) ) ) )
491	490	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 ) ) ) ) ) ) )
492	491	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 ) ) ) ) ) )
493	478 22 492	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 ) ) ) ) ) )
494		fveq1	|- ( f = ( B |` Y ) -> ( f ` k ) = ( ( B |` Y ) ` k ) )
495	494	adantr	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( f ` k ) = ( ( B |` Y ) ` k ) )
496	260	adantl	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( ( B |` Y ) ` k ) = ( B ` k ) )
497	495 496	eqtrd	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( f ` k ) = ( B ` k ) )
498	497	oveq2d	|- ( ( f = ( B |` Y ) /\ k e. Y ) -> ( ( A ` k ) [,) ( f ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
499	498	ixpeq2dva	|- ( f = ( B |` Y ) -> X_ k e. Y ( ( A ` k ) [,) ( f ` k ) ) = X_ k e. Y ( ( A ` k ) [,) ( B ` k ) ) )
500	499	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 ) ) ) )
501		oveq2	|- ( f = ( B |` Y ) -> ( ( A |` Y ) ( L ` Y ) f ) = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) )
502	501	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 ) ) ) ) ) )
503	500 502	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 ) ) ) ) ) ) )
504	503	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 ) ) ) ) ) ) )
505	504	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 ) ) ) ) ) ) )
506	505	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 ) ) ) ) ) )
507	476 493 506	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 ) ) ) ) ) )
508		fveq1	|- ( g = J -> ( g ` j ) = ( J ` j ) )
509	508	fveq1d	|- ( g = J -> ( ( g ` j ) ` k ) = ( ( J ` j ) ` k ) )
510	509	oveq1d	|- ( g = J -> ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
511	510	ixpeq2dv	|- ( g = J -> X_ k e. Y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
512	511	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 ) ) )
513	512	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 ) ) ) )
514	508	oveq1d	|- ( g = J -> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) = ( ( J ` j ) ( L ` Y ) ( h ` j ) ) )
515	514	mpteq2dv	|- ( g = J -> ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) )
516	515	fveq2d	|- ( g = J -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` Y ) ( h ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) )
517	516	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 ) ) ) ) ) )
518	513 517	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 ) ) ) ) ) ) )
519	518	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 ) ) ) ) ) ) )
520	519	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 ) ) ) ) ) )
521	474 507 520	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 ) ) ) ) ) )
522		fveq1	|- ( h = K -> ( h ` j ) = ( K ` j ) )
523	522	fveq1d	|- ( h = K -> ( ( h ` j ) ` k ) = ( ( K ` j ) ` k ) )
524	523	oveq2d	|- ( h = K -> ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
525	524	ixpeq2dv	|- ( h = K -> X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. Y ( ( ( J ` j ) ` k ) [,) ( ( K ` j ) ` k ) ) )
526	525	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 ) ) )
527	526	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 ) ) ) )
528	522	oveq2d	|- ( h = K -> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
529	528	mpteq2dv	|- ( h = K -> ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) )
530	529	fveq2d	|- ( h = K -> ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( h ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
531	530	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 ) ) ) ) ) )
532	527 531	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 ) ) ) ) ) ) )
533	532	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 ) ) ) ) ) )
534	472 521 533	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 ) ) ) ) ) )
535	468 534	mpd	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
536		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 ) ) ) ) ) )
537	535 536	mpd	|- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
538	537	adantr	|- ( ( ph /\ Y =/= (/) ) -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) <_ ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
539	62	adantl	|- ( ( ( ph /\ Y =/= (/) ) /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
540	539	mpteq2dva	|- ( ( ph /\ Y =/= (/) ) -> ( j e. NN |-> ( P ` j ) ) = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) )
541	540	fveq2d	|- ( ( ph /\ Y =/= (/) ) -> ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = ( sum^ ` ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) ) ) )
542	258 541	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 ) ) ) ) ) )
543	538 542	mpbird	|- ( ( ph /\ Y =/= (/) ) -> G <_ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
544	543	adantr	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> G <_ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
545	247 249 250 289 544	ltletrd	|- ( ( ( ph /\ Y =/= (/) ) /\ ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) e. RR ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
546	235 246 545	syl2anc	|- ( ( ( ph /\ Y =/= (/) ) /\ -. ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) = +oo ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
547	234 546	pm2.61dan	|- ( ( ph /\ Y =/= (/) ) -> ( G / ( 1 + E ) ) < ( sum^ ` ( j e. NN |-> ( P ` j ) ) ) )
548	207 208 209 210 227 547	sge0uzfsumgt	|- ( ( ph /\ Y =/= (/) ) -> E. m e. NN ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) )
549	226	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) e. RR )
550		fzfid	|- ( ph -> ( 1 ... m ) e. Fin )
551		simpl	|- ( ( ph /\ j e. ( 1 ... m ) ) -> ph )
552		elfznn	|- ( j e. ( 1 ... m ) -> j e. NN )
553	552	adantl	|- ( ( ph /\ j e. ( 1 ... m ) ) -> j e. NN )
554	50 126	sselid	|- ( ( ph /\ j e. NN ) -> ( P ` j ) e. RR )
555	551 553 554	syl2anc	|- ( ( ph /\ j e. ( 1 ... m ) ) -> ( P ` j ) e. RR )
556	550 555	fsumrecl	|- ( ph -> sum_ j e. ( 1 ... m ) ( P ` j ) e. RR )
557	556	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> sum_ j e. ( 1 ... m ) ( P ` j ) e. RR )
558		simpr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) )
559	549 557 558	ltled	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( G / ( 1 + E ) ) <_ sum_ j e. ( 1 ... m ) ( P ` j ) )
560	216	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G e. RR )
561	222	adantr	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> ( 1 + E ) e. RR+ )
562	560 557 561	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 ) ) ) )
563	559 562	mpbid	|- ( ( ph /\ ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
564	563	ex	|- ( ph -> ( ( G / ( 1 + E ) ) < sum_ j e. ( 1 ... m ) ( P ` j ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) )
565	564	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 ) ) ) )
566	565	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 ) ) ) )
567	566	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 ) ) ) )
568	548 567	mpd	|- ( ( ph /\ Y =/= (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
569	204 206 568	syl2anc	|- ( ( ph /\ -. Y = (/) ) -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
570	203 569	pm2.61dan	|- ( ph -> E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
571	2	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> X e. Fin )
572	3	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> Y C_ X )
573	4	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> Z e. ( X \ Y ) )
574	6	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> A : W --> RR )
575	7	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> B : W --> RR )
576	10	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> C : NN --> ( RR ^m W ) )
577		eqid	|- ( y e. Y |-> 0 ) = ( y e. Y |-> 0 )
578		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 ) ) )
579	12	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> D : NN --> ( RR ^m W ) )
580		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 ) ) )
581		fveq2	|- ( i = j -> ( C ` i ) = ( C ` j ) )
582		fveq2	|- ( i = j -> ( D ` i ) = ( D ` j ) )
583	581 582	oveq12d	|- ( i = j -> ( ( C ` i ) ( L ` W ) ( D ` i ) ) = ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
584	583	cbvmptv	|- ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) )
585	584	fveq2i	|- ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) )
586	585 14	eqeltrid	|- ( ph -> ( sum^ ` ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( D ` i ) ) ) ) e. RR )
587	586	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 )
588		eleq1w	|- ( j = i -> ( j e. Y <-> i e. Y ) )
589		fveq2	|- ( j = i -> ( c ` j ) = ( c ` i ) )
590	589	breq1d	|- ( j = i -> ( ( c ` j ) <_ x <-> ( c ` i ) <_ x ) )
591	590 589	ifbieq1d	|- ( j = i -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` i ) <_ x , ( c ` i ) , x ) )
592	588 589 591	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 ) ) )
593	592	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 ) ) )
594	593	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 ) ) ) )
595	594	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 ) ) ) ) )
596	15 595	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 ) ) ) ) )
597	17	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> E e. RR+ )
598		fveq2	|- ( j = i -> ( C ` j ) = ( C ` i ) )
599		fveq2	|- ( j = i -> ( D ` j ) = ( D ` i ) )
600	599	fveq2d	|- ( j = i -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` z ) ` ( D ` i ) ) )
601	598 600	oveq12d	|- ( j = i -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) )
602	601	cbvmptv	|- ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( i e. NN |-> ( ( C ` i ) ( L ` W ) ( ( H ` z ) ` ( D ` i ) ) ) )
603	602	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 ) ) ) ) )
604	603	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 ) ) ) ) ) )
605	604	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 ) ) ) ) ) ) )
606	605	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 ) ) ) ) ) ) }
607	18 606	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 ) ) ) ) ) ) }
608	19	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> S e. U )
609	20	3ad2ant1	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> S < ( B ` Z ) )
610		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 ) ) )
611		simp2	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> m e. NN )
612		id	|- ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) )
613		fveq2	|- ( j = i -> ( P ` j ) = ( P ` i ) )
614	613	cbvsumv	|- sum_ j e. ( 1 ... m ) ( P ` j ) = sum_ i e. ( 1 ... m ) ( P ` i )
615	614	oveq2i	|- ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) = ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) )
616	615	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 ) ) )
617	612 616	breqtrd	|- ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> G <_ ( ( 1 + E ) x. sum_ i e. ( 1 ... m ) ( P ` i ) ) )
618	617	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 ) ) )
619		simpl	|- ( ( ph /\ i e. ( 1 ... m ) ) -> ph )
620		elfznn	|- ( i e. ( 1 ... m ) -> i e. NN )
621	620	adantl	|- ( ( ph /\ i e. ( 1 ... m ) ) -> i e. NN )
622		eleq1w	|- ( j = i -> ( j e. NN <-> i e. NN ) )
623		fveq2	|- ( j = i -> ( J ` j ) = ( J ` i ) )
624		fveq2	|- ( j = i -> ( K ` j ) = ( K ` i ) )
625	623 624	oveq12d	|- ( j = i -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
626	613 625	eqeq12d	|- ( j = i -> ( ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) <-> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) ) )
627	622 626	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 ) ) ) ) )
628	627 62	chvarvv	|- ( i e. NN -> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
629	628	adantl	|- ( ( ph /\ i e. NN ) -> ( P ` i ) = ( ( J ` i ) ( L ` Y ) ( K ` i ) ) )
630	622	anbi2d	|- ( j = i -> ( ( ph /\ j e. NN ) <-> ( ph /\ i e. NN ) ) )
631	598	fveq1d	|- ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
632	599	fveq1d	|- ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
633	631 632	oveq12d	|- ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
634	633	eleq2d	|- ( j = i -> ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
635	598	reseq1d	|- ( j = i -> ( ( C ` j ) |` Y ) = ( ( C ` i ) |` Y ) )
636	634 635	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 ) )
637	623 636	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 ) ) )
638	630 637	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 ) ) ) )
639	638 161	chvarvv	|- ( ( ph /\ i e. NN ) -> ( J ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , F ) )
640	599	reseq1d	|- ( j = i -> ( ( D ` j ) |` Y ) = ( ( D ` i ) |` Y ) )
641	634 640	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 ) )
642	624 641	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 ) ) )
643	630 642	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 ) ) ) )
644	643 443	chvarvv	|- ( ( ph /\ i e. NN ) -> ( K ` i ) = if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , F ) )
645	639 644	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 ) ) )
646	629 645	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 ) ) )
647		simpr	|- ( ( ph /\ i e. NN ) -> i e. NN )
648		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 )
649	610	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 ) ) )
650	647 648 649	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 ) ) )
651		fvex	|- ( C ` i ) e. _V
652	651	resex	|- ( ( C ` i ) |` Y ) e. _V
653	652	a1i	|- ( ph -> ( ( C ` i ) |` Y ) e. _V )
654	9 155	eqeltrrid	|- ( ph -> ( y e. Y |-> 0 ) e. _V )
655	653 654	ifcld	|- ( ph -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
656	655	adantr	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( C ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
657	578	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 ) ) )
658	647 656 657	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 ) ) )
659	9	eqcomi	|- ( y e. Y |-> 0 ) = F
660		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 ) )
661	659 660	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 )
662	661	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 ) )
663	658 662	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 ) )
664		fvex	|- ( D ` i ) e. _V
665	664	resex	|- ( ( D ` i ) |` Y ) e. _V
666	665	a1i	|- ( ph -> ( ( D ` i ) |` Y ) e. _V )
667	666 654	ifcld	|- ( ph -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
668	667	adantr	|- ( ( ph /\ i e. NN ) -> if ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) , ( ( D ` i ) |` Y ) , ( y e. Y |-> 0 ) ) e. _V )
669	580	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 ) ) )
670	647 668 669	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 ) ) )
671		biid	|- ( S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
672	671 659	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 )
673	672	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 ) )
674	670 673	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 ) )
675	663 674	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 ) ) )
676	650 675	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 ) ) )
677	646 676	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 ) )
678	619 621 677	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 ) )
679	678	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 ) )
680	679	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 ) )
681	680	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 ) ) )
682	618 681	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 ) ) )
683		fveq2	|- ( j = h -> ( D ` j ) = ( D ` h ) )
684	683	fveq1d	|- ( j = h -> ( ( D ` j ) ` Z ) = ( ( D ` h ) ` Z ) )
685	684	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 ) )
686	685	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 ) )
687		fveq2	|- ( h = i -> ( C ` h ) = ( C ` i ) )
688	687	fveq1d	|- ( h = i -> ( ( C ` h ) ` Z ) = ( ( C ` i ) ` Z ) )
689		fveq2	|- ( h = i -> ( D ` h ) = ( D ` i ) )
690	689	fveq1d	|- ( h = i -> ( ( D ` h ) ` Z ) = ( ( D ` i ) ` Z ) )
691	688 690	oveq12d	|- ( h = i -> ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
692	691	eleq2d	|- ( h = i -> ( S e. ( ( ( C ` h ) ` Z ) [,) ( ( D ` h ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
693	692	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 ) ) }
694	693	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 ) )
695	694	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 ) )
696	695	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 ) ) )
697		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 , < )
698	1 571 572 573 5 574 575 576 577 578 579 580 587 596 16 597 607 608 609 610 611 682 686 696 697	hoidmvlelem2	|- ( ( ph /\ m e. NN /\ G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) ) -> E. u e. U S < u )
699	698	3exp	|- ( ph -> ( m e. NN -> ( G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> E. u e. U S < u ) ) )
700	699	rexlimdv	|- ( ph -> ( E. m e. NN G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... m ) ( P ` j ) ) -> E. u e. U S < u ) )
701	570 700	mpd	|- ( ph -> E. u e. U S < u )