Theorem hoidmvlelem2 38536

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

Hypotheses

Ref	Expression
hoidmvlelem2.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 ) ) ) ) ) )
hoidmvlelem2.x	|- ( ph -> X e. Fin )
hoidmvlelem2.y	|- ( ph -> Y C_ X )
hoidmvlelem2.z	|- ( ph -> Z e. ( X \ Y ) )
hoidmvlelem2.w	|- W = ( Y u. { Z } )
hoidmvlelem2.a	|- ( ph -> A : W --> RR )
hoidmvlelem2.b	|- ( ph -> B : W --> RR )
hoidmvlelem2.c	|- ( ph -> C : NN --> ( RR ^m W ) )
hoidmvlelem2.f	|- F = ( y e. Y |-> 0 )
hoidmvlelem2.j	|- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
hoidmvlelem2.d	|- ( ph -> D : NN --> ( RR ^m W ) )
hoidmvlelem2.k	|- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
hoidmvlelem2.r	|- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
hoidmvlelem2.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 ) ) ) ) )
hoidmvlelem2.g	|- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
hoidmvlelem2.e	|- ( ph -> E e. RR+ )
hoidmvlelem2.u	|- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
hoidmvlelem2.su	|- ( ph -> S e. U )
hoidmvlelem2.sb	|- ( ph -> S < ( B ` Z ) )
hoidmvlelem2.p	|- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
hoidmvlelem2.m	|- ( ph -> M e. NN )
hoidmvlelem2.le	|- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )
hoidmvlelem2.O	|- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
hoidmvlelem2.v	|- V = ( { ( B ` Z ) } u. O )
hoidmvlelem2.q	|- Q = inf ( V , RR , < )

Assertion

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

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

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

Proof of Theorem hoidmvlelem2

Dummy variable l is distinct from all other variables.

Step	Hyp	Ref	Expression
1		hoidmvlelem2.a	. . . . . . 7 |- ( ph -> A : W --> RR )
2		hoidmvlelem2.z	. . . . . . . . . 10 |- ( ph -> Z e. ( X \ Y ) )
3		snidg 3986	. . . . . . . . . 10 |- ( Z e. ( X \ Y ) -> Z e. { Z } )
4	2, 3	syl 17	. . . . . . . . 9 |- ( ph -> Z e. { Z } )
5		elun2 3593	. . . . . . . . 9 |- ( Z e. { Z } -> Z e. ( Y u. { Z } ) )
6	4, 5	syl 17	. . . . . . . 8 |- ( ph -> Z e. ( Y u. { Z } ) )
7		hoidmvlelem2.w	. . . . . . . 8 |- W = ( Y u. { Z } )
8	6, 7	syl6eleqr 2560	. . . . . . 7 |- ( ph -> Z e. W )
9	1, 8	ffvelrnd 6038	. . . . . 6 |- ( ph -> ( A ` Z ) e. RR )
10		hoidmvlelem2.b	. . . . . . 7 |- ( ph -> B : W --> RR )
11	10, 8	ffvelrnd 6038	. . . . . 6 |- ( ph -> ( B ` Z ) e. RR )
12		hoidmvlelem2.v	. . . . . . . 8 |- V = ( { ( B ` Z ) } u. O )
13	11	snssd 4108	. . . . . . . . 9 |- ( ph -> { ( B ` Z ) } C_ RR )
14		hoidmvlelem2.O	. . . . . . . . . 10 |- O = ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
15		nfv 1769	. . . . . . . . . . 11 |- F/ i ph
16		eqid 2471	. . . . . . . . . . 11 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) = ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) )
17		simpl 464	. . . . . . . . . . . 12 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ph )
18		fz1ssnn 11856	. . . . . . . . . . . . . 14 |- ( 1 ... M ) C_ NN
19		elrabi 3181	. . . . . . . . . . . . . 14 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. ( 1 ... M ) )
20	18, 19	sseldi 3416	. . . . . . . . . . . . 13 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> i e. NN )
21	20	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> i e. NN )
22		eleq1 2537	. . . . . . . . . . . . . . 15 |- ( j = i -> ( j e. NN <-> i e. NN ) )
23	22	anbi2d 718	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ph /\ j e. NN ) <-> ( ph /\ i e. NN ) ) )
24		fveq2 5879	. . . . . . . . . . . . . . . 16 |- ( j = i -> ( D ` j ) = ( D ` i ) )
25	24	fveq1d 5881	. . . . . . . . . . . . . . 15 |- ( j = i -> ( ( D ` j ) ` Z ) = ( ( D ` i ) ` Z ) )
26	25	eleq1d 2533	. . . . . . . . . . . . . 14 |- ( j = i -> ( ( ( D ` j ) ` Z ) e. RR <-> ( ( D ` i ) ` Z ) e. RR ) )
27	23, 26	imbi12d 327	. . . . . . . . . . . . 13 |- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR ) ) )
28		hoidmvlelem2.d	. . . . . . . . . . . . . . . 16 |- ( ph -> D : NN --> ( RR ^m W ) )
29	28	ffvelrnda 6037	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( D ` j ) e. ( RR ^m W ) )
30		elmapi 7511	. . . . . . . . . . . . . . 15 |- ( ( D ` j ) e. ( RR ^m W ) -> ( D ` j ) : W --> RR )
31	29, 30	syl 17	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( D ` j ) : W --> RR )
32	8	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> Z e. W )
33	31, 32	ffvelrnd 6038	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) ` Z ) e. RR )
34	27, 33	chvarv 2120	. . . . . . . . . . . 12 |- ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR )
35	17, 21, 34	syl2anc 673	. . . . . . . . . . 11 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR )
36	15, 16, 35	rnmptssd 37544	. . . . . . . . . 10 |- ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) C_ RR )
37	14, 36	syl5eqss 3462	. . . . . . . . 9 |- ( ph -> O C_ RR )
38	13, 37	unssd 3601	. . . . . . . 8 |- ( ph -> ( { ( B ` Z ) } u. O ) C_ RR )
39	12, 38	syl5eqss 3462	. . . . . . 7 |- ( ph -> V C_ RR )
40		hoidmvlelem2.q	. . . . . . . 8 |- Q = inf ( V , RR , < )
41		ltso 9732	. . . . . . . . . 10 |- < Or RR
42	41	a1i 11	. . . . . . . . 9 |- ( ph -> < Or RR )
43		snfi 7668	. . . . . . . . . . . 12 |- { ( B ` Z ) } e. Fin
44	43	a1i 11	. . . . . . . . . . 11 |- ( ph -> { ( B ` Z ) } e. Fin )
45		fzfi 12223	. . . . . . . . . . . . . . 15 |- ( 1 ... M ) e. Fin
46		rabfi 7814	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) e. Fin -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
47	45, 46	ax-mp 5	. . . . . . . . . . . . . 14 |- { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin
48	47	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin )
49	16	rnmptfi 37508	. . . . . . . . . . . . 13 |- ( { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } e. Fin -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) e. Fin )
50	48, 49	syl 17	. . . . . . . . . . . 12 |- ( ph -> ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) e. Fin )
51	14, 50	syl5eqel 2553	. . . . . . . . . . 11 |- ( ph -> O e. Fin )
52		unfi 7856	. . . . . . . . . . 11 |- ( ( { ( B ` Z ) } e. Fin /\ O e. Fin ) -> ( { ( B ` Z ) } u. O ) e. Fin )
53	44, 51, 52	syl2anc 673	. . . . . . . . . 10 |- ( ph -> ( { ( B ` Z ) } u. O ) e. Fin )
54	12, 53	syl5eqel 2553	. . . . . . . . 9 |- ( ph -> V e. Fin )
55		fvex 5889	. . . . . . . . . . . . . 14 |- ( B ` Z ) e. _V
56	55	snid 3988	. . . . . . . . . . . . 13 |- ( B ` Z ) e. { ( B ` Z ) }
57		elun1 3592	. . . . . . . . . . . . 13 |- ( ( B ` Z ) e. { ( B ` Z ) } -> ( B ` Z ) e. ( { ( B ` Z ) } u. O ) )
58	56, 57	ax-mp 5	. . . . . . . . . . . 12 |- ( B ` Z ) e. ( { ( B ` Z ) } u. O )
59	12	eqcomi 2480	. . . . . . . . . . . 12 |- ( { ( B ` Z ) } u. O ) = V
60	58, 59	eleqtri 2547	. . . . . . . . . . 11 |- ( B ` Z ) e. V
61	60	a1i 11	. . . . . . . . . 10 |- ( ph -> ( B ` Z ) e. V )
62		ne0i 3728	. . . . . . . . . 10 |- ( ( B ` Z ) e. V -> V =/= (/) )
63	61, 62	syl 17	. . . . . . . . 9 |- ( ph -> V =/= (/) )
64		fiinfcl 8035	. . . . . . . . 9 |- ( ( < Or RR /\ ( V e. Fin /\ V =/= (/) /\ V C_ RR ) ) -> inf ( V , RR , < ) e. V )
65	42, 54, 63, 39, 64	syl13anc 1294	. . . . . . . 8 |- ( ph -> inf ( V , RR , < ) e. V )
66	40, 65	syl5eqel 2553	. . . . . . 7 |- ( ph -> Q e. V )
67	39, 66	sseldd 3419	. . . . . 6 |- ( ph -> Q e. RR )
68		hoidmvlelem2.u	. . . . . . . . . . . 12 |- U = { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) }
69		ssrab2 3500	. . . . . . . . . . . 12 |- { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } C_ ( ( A ` Z ) [,] ( B ` Z ) )
70	68, 69	eqsstri 3448	. . . . . . . . . . 11 |- U C_ ( ( A ` Z ) [,] ( B ` Z ) )
71	70	a1i 11	. . . . . . . . . 10 |- ( ph -> U C_ ( ( A ` Z ) [,] ( B ` Z ) ) )
72	9, 11	iccssred 37698	. . . . . . . . . 10 |- ( ph -> ( ( A ` Z ) [,] ( B ` Z ) ) C_ RR )
73	71, 72	sstrd 3428	. . . . . . . . 9 |- ( ph -> U C_ RR )
74		hoidmvlelem2.su	. . . . . . . . 9 |- ( ph -> S e. U )
75	73, 74	sseldd 3419	. . . . . . . 8 |- ( ph -> S e. RR )
76	9	rexrd 9708	. . . . . . . . 9 |- ( ph -> ( A ` Z ) e. RR* )
77	11	rexrd 9708	. . . . . . . . 9 |- ( ph -> ( B ` Z ) e. RR* )
78	70, 74	sseldi 3416	. . . . . . . . 9 |- ( ph -> S e. ( ( A ` Z ) [,] ( B ` Z ) ) )
79		iccgelb 11716	. . . . . . . . 9 |- ( ( ( A ` Z ) e. RR* /\ ( B ` Z ) e. RR* /\ S e. ( ( A ` Z ) [,] ( B ` Z ) ) ) -> ( A ` Z ) <_ S )
80	76, 77, 78, 79	syl3anc 1292	. . . . . . . 8 |- ( ph -> ( A ` Z ) <_ S )
81		hoidmvlelem2.sb	. . . . . . . . . . . . . . 15 |- ( ph -> S < ( B ` Z ) )
82	81	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = ( B ` Z ) ) -> S < ( B ` Z ) )
83		id 22	. . . . . . . . . . . . . . . 16 |- ( x = ( B ` Z ) -> x = ( B ` Z ) )
84	83	eqcomd 2477	. . . . . . . . . . . . . . 15 |- ( x = ( B ` Z ) -> ( B ` Z ) = x )
85	84	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ x = ( B ` Z ) ) -> ( B ` Z ) = x )
86	82, 85	breqtrd 4420	. . . . . . . . . . . . 13 |- ( ( ph /\ x = ( B ` Z ) ) -> S < x )
87	86	adantlr 729	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. V ) /\ x = ( B ` Z ) ) -> S < x )
88		simpll 768	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> ph )
89		id 22	. . . . . . . . . . . . . . . . 17 |- ( x e. V -> x e. V )
90	89, 12	syl6eleq 2559	. . . . . . . . . . . . . . . 16 |- ( x e. V -> x e. ( { ( B ` Z ) } u. O ) )
91	90	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. ( { ( B ` Z ) } u. O ) )
92		elsni 3985	. . . . . . . . . . . . . . . . 17 |- ( x e. { ( B ` Z ) } -> x = ( B ` Z ) )
93	92	con3i 142	. . . . . . . . . . . . . . . 16 |- ( -. x = ( B ` Z ) -> -. x e. { ( B ` Z ) } )
94	93	adantl 473	. . . . . . . . . . . . . . 15 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> -. x e. { ( B ` Z ) } )
95		elunnel1 3566	. . . . . . . . . . . . . . 15 |- ( ( x e. ( { ( B ` Z ) } u. O ) /\ -. x e. { ( B ` Z ) } ) -> x e. O )
96	91, 94, 95	syl2anc 673	. . . . . . . . . . . . . 14 |- ( ( x e. V /\ -. x = ( B ` Z ) ) -> x e. O )
97	96	adantll 728	. . . . . . . . . . . . 13 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> x e. O )
98		id 22	. . . . . . . . . . . . . . . . 17 |- ( x e. O -> x e. O )
99	98, 14	syl6eleq 2559	. . . . . . . . . . . . . . . 16 |- ( x e. O -> x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) )
100		vex 3034	. . . . . . . . . . . . . . . . 17 |- x e. _V
101	16	elrnmpt 5087	. . . . . . . . . . . . . . . . 17 |- ( x e. _V -> ( x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) <-> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) ) )
102	100, 101	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( x e. ran ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } |-> ( ( D ` i ) ` Z ) ) <-> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
103	99, 102	sylib 201	. . . . . . . . . . . . . . 15 |- ( x e. O -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
104	103	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. O ) -> E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) )
105		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = i -> ( C ` j ) = ( C ` i ) )
106	105	fveq1d 5881	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = i -> ( ( C ` j ) ` Z ) = ( ( C ` i ) ` Z ) )
107	106	eleq1d 2533	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = i -> ( ( ( C ` j ) ` Z ) e. RR <-> ( ( C ` i ) ` Z ) e. RR ) )
108	23, 107	imbi12d 327	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = i -> ( ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR ) <-> ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR ) ) )
109		hoidmvlelem2.c	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ph -> C : NN --> ( RR ^m W ) )
110	109	ffvelrnda 6037	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ j e. NN ) -> ( C ` j ) e. ( RR ^m W ) )
111		elmapi 7511	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( C ` j ) e. ( RR ^m W ) -> ( C ` j ) : W --> RR )
112	110, 111	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ j e. NN ) -> ( C ` j ) : W --> RR )
113	112, 32	ffvelrnd 6038	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ` Z ) e. RR )
114	108, 113	chvarv 2120	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR )
115	114	rexrd 9708	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. NN ) -> ( ( C ` i ) ` Z ) e. RR* )
116	17, 21, 115	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( C ` i ) ` Z ) e. RR* )
117	34	rexrd 9708	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ i e. NN ) -> ( ( D ` i ) ` Z ) e. RR* )
118	17, 21, 117	syl2anc 673	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> ( ( D ` i ) ` Z ) e. RR* )
119	106, 25	oveq12d 6326	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = i -> ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) = ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
120	119	eleq2d 2534	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = i -> ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) <-> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
121	120	elrab 3184	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } <-> ( i e. ( 1 ... M ) /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
122	121	biimpi 199	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( i e. ( 1 ... M ) /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) )
123	122	simprd 470	. . . . . . . . . . . . . . . . . . . . 21 |- ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
124	123	adantl 473	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) )
125		icoltub 37703	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( C ` i ) ` Z ) e. RR* /\ ( ( D ` i ) ` Z ) e. RR* /\ S e. ( ( ( C ` i ) ` Z ) [,) ( ( D ` i ) ` Z ) ) ) -> S < ( ( D ` i ) ` Z ) )
126	116, 118, 124, 125	syl3anc 1292	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } ) -> S < ( ( D ` i ) ` Z ) )
127	126	3adant3 1050	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < ( ( D ` i ) ` Z ) )
128		id 22	. . . . . . . . . . . . . . . . . . . 20 |- ( x = ( ( D ` i ) ` Z ) -> x = ( ( D ` i ) ` Z ) )
129	128	eqcomd 2477	. . . . . . . . . . . . . . . . . . 19 |- ( x = ( ( D ` i ) ` Z ) -> ( ( D ` i ) ` Z ) = x )
130	129	3ad2ant3 1053	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> ( ( D ` i ) ` Z ) = x )
131	127, 130	breqtrd 4420	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } /\ x = ( ( D ` i ) ` Z ) ) -> S < x )
132	131	3exp 1230	. . . . . . . . . . . . . . . 16 |- ( ph -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
133	132	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ x e. O ) -> ( i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } -> ( x = ( ( D ` i ) ` Z ) -> S < x ) ) )
134	133	rexlimdv 2870	. . . . . . . . . . . . . 14 |- ( ( ph /\ x e. O ) -> ( E. i e. { j e. ( 1 ... M ) | S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) } x = ( ( D ` i ) ` Z ) -> S < x ) )
135	104, 134	mpd 15	. . . . . . . . . . . . 13 |- ( ( ph /\ x e. O ) -> S < x )
136	88, 97, 135	syl2anc 673	. . . . . . . . . . . 12 |- ( ( ( ph /\ x e. V ) /\ -. x = ( B ` Z ) ) -> S < x )
137	87, 136	pm2.61dan 808	. . . . . . . . . . 11 |- ( ( ph /\ x e. V ) -> S < x )
138	137	ralrimiva 2809	. . . . . . . . . 10 |- ( ph -> A. x e. V S < x )
139		breq2 4399	. . . . . . . . . . 11 |- ( x = inf ( V , RR , < ) -> ( S < x <-> S < inf ( V , RR , < ) ) )
140	139	rspcva 3134	. . . . . . . . . 10 |- ( (inf ( V , RR , < ) e. V /\ A. x e. V S < x ) -> S < inf ( V , RR , < ) )
141	65, 138, 140	syl2anc 673	. . . . . . . . 9 |- ( ph -> S < inf ( V , RR , < ) )
142	40	eqcomi 2480	. . . . . . . . . 10 |- inf ( V , RR , < ) = Q
143	142	a1i 11	. . . . . . . . 9 |- ( ph -> inf ( V , RR , < ) = Q )
144	141, 143	breqtrd 4420	. . . . . . . 8 |- ( ph -> S < Q )
145	9, 75, 67, 80, 144	lelttrd 9810	. . . . . . 7 |- ( ph -> ( A ` Z ) < Q )
146	9, 67, 145	ltled 9800	. . . . . 6 |- ( ph -> ( A ` Z ) <_ Q )
147		fiminre 10577	. . . . . . . . 9 |- ( ( V C_ RR /\ V e. Fin /\ V =/= (/) ) -> E. x e. V A. y e. V x <_ y )
148	39, 54, 63, 147	syl3anc 1292	. . . . . . . 8 |- ( ph -> E. x e. V A. y e. V x <_ y )
149		lbinfle 10585	. . . . . . . 8 |- ( ( V C_ RR /\ E. x e. V A. y e. V x <_ y /\ ( B ` Z ) e. V ) -> inf ( V , RR , < ) <_ ( B ` Z ) )
150	39, 148, 61, 149	syl3anc 1292	. . . . . . 7 |- ( ph -> inf ( V , RR , < ) <_ ( B ` Z ) )
151	40, 150	syl5eqbr 4429	. . . . . 6 |- ( ph -> Q <_ ( B ` Z ) )
152	9, 11, 67, 146, 151	eliccd 37697	. . . . 5 |- ( ph -> Q e. ( ( A ` Z ) [,] ( B ` Z ) ) )
153	67	recnd 9687	. . . . . . . . . 10 |- ( ph -> Q e. CC )
154	75	recnd 9687	. . . . . . . . . 10 |- ( ph -> S e. CC )
155	9	recnd 9687	. . . . . . . . . 10 |- ( ph -> ( A ` Z ) e. CC )
156	153, 154, 155	npncand 10029	. . . . . . . . 9 |- ( ph -> ( ( Q - S ) + ( S - ( A ` Z ) ) ) = ( Q - ( A ` Z ) ) )
157	156	eqcomd 2477	. . . . . . . 8 |- ( ph -> ( Q - ( A ` Z ) ) = ( ( Q - S ) + ( S - ( A ` Z ) ) ) )
158	157	oveq2d 6324	. . . . . . 7 |- ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) )
159		rge0ssre 11766	. . . . . . . . . 10 |- ( 0 [,) +oo ) C_ RR
160		hoidmvlelem2.g	. . . . . . . . . . 11 |- G = ( ( A |` Y ) ( L ` Y ) ( B |` Y ) )
161		hoidmvlelem2.l	. . . . . . . . . . . 12 |- 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 ) ) ) ) ) )
162		hoidmvlelem2.x	. . . . . . . . . . . . 13 |- ( ph -> X e. Fin )
163		hoidmvlelem2.y	. . . . . . . . . . . . 13 |- ( ph -> Y C_ X )
164	162, 163	ssfid 37473	. . . . . . . . . . . 12 |- ( ph -> Y e. Fin )
165		ssun1 3588	. . . . . . . . . . . . . . 15 |- Y C_ ( Y u. { Z } )
166	165, 7	sseqtr4i 3451	. . . . . . . . . . . . . 14 |- Y C_ W
167	166	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> Y C_ W )
168	1, 167	fssresd 5762	. . . . . . . . . . . 12 |- ( ph -> ( A |` Y ) : Y --> RR )
169	10, 167	fssresd 5762	. . . . . . . . . . . 12 |- ( ph -> ( B |` Y ) : Y --> RR )
170	161, 164, 168, 169	hoidmvcl 38522	. . . . . . . . . . 11 |- ( ph -> ( ( A |` Y ) ( L ` Y ) ( B |` Y ) ) e. ( 0 [,) +oo ) )
171	160, 170	syl5eqel 2553	. . . . . . . . . 10 |- ( ph -> G e. ( 0 [,) +oo ) )
172	159, 171	sseldi 3416	. . . . . . . . 9 |- ( ph -> G e. RR )
173	172	recnd 9687	. . . . . . . 8 |- ( ph -> G e. CC )
174	153, 154	subcld 10005	. . . . . . . 8 |- ( ph -> ( Q - S ) e. CC )
175	154, 155	subcld 10005	. . . . . . . 8 |- ( ph -> ( S - ( A ` Z ) ) e. CC )
176	173, 174, 175	adddid 9685	. . . . . . 7 |- ( ph -> ( G x. ( ( Q - S ) + ( S - ( A ` Z ) ) ) ) = ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) )
177	173, 174	mulcld 9681	. . . . . . . 8 |- ( ph -> ( G x. ( Q - S ) ) e. CC )
178	173, 175	mulcld 9681	. . . . . . . 8 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. CC )
179	177, 178	addcomd 9853	. . . . . . 7 |- ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
180	158, 176, 179	3eqtrd 2509	. . . . . 6 |- ( ph -> ( G x. ( Q - ( A ` Z ) ) ) = ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) )
181	67, 75	jca 541	. . . . . . . . . . . . 13 |- ( ph -> ( Q e. RR /\ S e. RR ) )
182		resubcl 9958	. . . . . . . . . . . . 13 |- ( ( Q e. RR /\ S e. RR ) -> ( Q - S ) e. RR )
183	181, 182	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( Q - S ) e. RR )
184	172, 183	jca 541	. . . . . . . . . . 11 |- ( ph -> ( G e. RR /\ ( Q - S ) e. RR ) )
185		remulcl 9642	. . . . . . . . . . 11 |- ( ( G e. RR /\ ( Q - S ) e. RR ) -> ( G x. ( Q - S ) ) e. RR )
186	184, 185	syl 17	. . . . . . . . . 10 |- ( ph -> ( G x. ( Q - S ) ) e. RR )
187	75, 9	jca 541	. . . . . . . . . . . . 13 |- ( ph -> ( S e. RR /\ ( A ` Z ) e. RR ) )
188		resubcl 9958	. . . . . . . . . . . . 13 |- ( ( S e. RR /\ ( A ` Z ) e. RR ) -> ( S - ( A ` Z ) ) e. RR )
189	187, 188	syl 17	. . . . . . . . . . . 12 |- ( ph -> ( S - ( A ` Z ) ) e. RR )
190	172, 189	jca 541	. . . . . . . . . . 11 |- ( ph -> ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) )
191		remulcl 9642	. . . . . . . . . . 11 |- ( ( G e. RR /\ ( S - ( A ` Z ) ) e. RR ) -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
192	190, 191	syl 17	. . . . . . . . . 10 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) e. RR )
193	186, 192	jca 541	. . . . . . . . 9 |- ( ph -> ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) )
194		readdcl 9640	. . . . . . . . 9 |- ( ( ( G x. ( Q - S ) ) e. RR /\ ( G x. ( S - ( A ` Z ) ) ) e. RR ) -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
195	193, 194	syl 17	. . . . . . . 8 |- ( ph -> ( ( G x. ( Q - S ) ) + ( G x. ( S - ( A ` Z ) ) ) ) e. RR )
196	179, 195	eqeltrrd 2550	. . . . . . 7 |- ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) e. RR )
197		1red 9676	. . . . . . . . . 10 |- ( ph -> 1 e. RR )
198		hoidmvlelem2.e	. . . . . . . . . . 11 |- ( ph -> E e. RR+ )
199	198	rpred 11364	. . . . . . . . . 10 |- ( ph -> E e. RR )
200	197, 199	readdcld 9688	. . . . . . . . 9 |- ( ph -> ( 1 + E ) e. RR )
201	2	eldifbd 3403	. . . . . . . . . . 11 |- ( ph -> -. Z e. Y )
202	8, 201	eldifd 3401	. . . . . . . . . 10 |- ( ph -> Z e. ( W \ Y ) )
203		hoidmvlelem2.r	. . . . . . . . . 10 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( D ` j ) ) ) ) e. RR )
204		hoidmvlelem2.h	. . . . . . . . . 10 |- 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 ) ) ) ) )
205	161, 164, 202, 7, 109, 28, 203, 204, 75	sge0hsphoire 38529	. . . . . . . . 9 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
206	200, 205	remulcld 9689	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
207		fzfid 12224	. . . . . . . . . 10 |- ( ph -> ( 1 ... M ) e. Fin )
208	183	adantr 472	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. RR )
209		simpl 464	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ph )
210		elfznn 11854	. . . . . . . . . . . . 13 |- ( j e. ( 1 ... M ) -> j e. NN )
211	210	adantl 473	. . . . . . . . . . . 12 |- ( ( ph /\ j e. ( 1 ... M ) ) -> j e. NN )
212		id 22	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> j e. NN )
213		ovex 6336	. . . . . . . . . . . . . . . . 17 |- ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V
214	213	a1i 11	. . . . . . . . . . . . . . . 16 |- ( j e. NN -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V )
215		hoidmvlelem2.p	. . . . . . . . . . . . . . . . 17 |- P = ( j e. NN |-> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
216	215	fvmpt2 5972	. . . . . . . . . . . . . . . 16 |- ( ( j e. NN /\ ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. _V ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
217	212, 214, 216	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( j e. NN -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
218	217	adantl 473	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( P ` j ) = ( ( J ` j ) ( L ` Y ) ( K ` j ) ) )
219	164	adantr 472	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> Y e. Fin )
220	166	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ j e. NN ) -> Y C_ W )
221	112, 220	fssresd 5762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) |` Y ) : Y --> RR )
222	221	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( C ` j ) |` Y ) : Y --> RR )
223		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
224	223	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = ( ( C ` j ) |` Y ) )
225	224	feq1d 5724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> ( ( C ` j ) |` Y ) : Y --> RR ) )
226	222, 225	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
227		0red 9662	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ y e. Y ) -> 0 e. RR )
228		hoidmvlelem2.f	. . . . . . . . . . . . . . . . . . . 20 |- F = ( y e. Y |-> 0 )
229	227, 228	fmptd 6061	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> F : Y --> RR )
230	229	ad2antrr 740	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> F : Y --> RR )
231		iffalse 3881	. . . . . . . . . . . . . . . . . . . 20 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
232	231	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) = F )
233	232	feq1d 5724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR <-> F : Y --> RR ) )
234	230, 233	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( ( ph /\ j e. NN ) /\ -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
235	226, 234	pm2.61dan 808	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR )
236		simpr 468	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> j e. NN )
237		fvex 5889	. . . . . . . . . . . . . . . . . . . . . 22 |- ( C ` j ) e. _V
238	237	resex 5154	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( C ` j ) |` Y ) e. _V
239	238	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( C ` j ) |` Y ) e. _V )
240	162, 163	ssexd 4543	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ph -> Y e. _V )
241		mptexg 6151	. . . . . . . . . . . . . . . . . . . . . 22 |- ( Y e. _V -> ( y e. Y |-> 0 ) e. _V )
242	240, 241	syl 17	. . . . . . . . . . . . . . . . . . . . 21 |- ( ph -> ( y e. Y |-> 0 ) e. _V )
243	228, 242	syl5eqel 2553	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> F e. _V )
244	239, 243	ifcld 3915	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
245	244	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V )
246		hoidmvlelem2.j	. . . . . . . . . . . . . . . . . . 19 |- J = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
247	246	fvmpt2 5972	. . . . . . . . . . . . . . . . . 18 |- ( ( j e. NN /\ if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) e. _V ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
248	236, 245, 247	syl2anc 673	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( J ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) )
249	248	feq1d 5724	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( C ` j ) |` Y ) , F ) : Y --> RR ) )
250	235, 249	mpbird 240	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( J ` j ) : Y --> RR )
251	31, 220	fssresd 5762	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ j e. NN ) -> ( ( D ` j ) |` Y ) : Y --> RR )
252	251	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ph /\ j e. NN ) /\ S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) ) -> ( ( D ` j ) |` Y ) : Y --> RR )
253		iftrue 3878	. . . . . . . . . . . . . . . . . . . 20 |- ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = ( ( D ` j ) |` Y ) )
254	253	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) )
255	254	feq1d 5724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) : Y --> RR <-> ( ( D ` j ) |` Y ) : Y --> RR ) )
256	252, 255	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) : Y --> RR )
257		iffalse 3881	. . . . . . . . . . . . . . . . . . . 20 |- ( -. S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) = F )
258	257	adantl 473	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 )
259	258	feq1d 5724	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) : Y --> RR <-> F : Y --> RR ) )
260	230, 259	mpbird 240	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) : Y --> RR )
261	256, 260	pm2.61dan 808	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR )
262		fvex 5889	. . . . . . . . . . . . . . . . . . . . . 22 |- ( D ` j ) e. _V
263	262	resex 5154	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( D ` j ) |` Y ) e. _V
264	263	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> ( ( D ` j ) |` Y ) e. _V )
265	264, 243	ifcld 3915	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
266	265	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) e. _V )
267		hoidmvlelem2.k	. . . . . . . . . . . . . . . . . . 19 |- K = ( j e. NN |-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
268	267	fvmpt2 5972	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 ) )
269	236, 266, 268	syl2anc 673	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( K ` j ) = if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) )
270	269	feq1d 5724	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( K ` j ) : Y --> RR <-> if ( S e. ( ( ( C ` j ) ` Z ) [,) ( ( D ` j ) ` Z ) ) , ( ( D ` j ) |` Y ) , F ) : Y --> RR ) )
271	261, 270	mpbird 240	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. NN ) -> ( K ` j ) : Y --> RR )
272	161, 219, 250, 271	hoidmvcl 38522	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( ( J ` j ) ( L ` Y ) ( K ` j ) ) e. ( 0 [,) +oo ) )
273	218, 272	eqeltrd 2549	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. ( 0 [,) +oo ) )
274	159, 273	sseldi 3416	. . . . . . . . . . . 12 |- ( ( ph /\ j e. NN ) -> ( P ` j ) e. RR )
275	209, 211, 274	syl2anc 673	. . . . . . . . . . 11 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. RR )
276	208, 275	remulcld 9689	. . . . . . . . . 10 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
277	207, 276	fsumrecl 13877	. . . . . . . . 9 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. RR )
278	200, 277	remulcld 9689	. . . . . . . 8 |- ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) e. RR )
279	206, 278	readdcld 9688	. . . . . . 7 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) e. RR )
280	161, 164, 202, 7, 109, 28, 203, 204, 67	sge0hsphoire 38529	. . . . . . . 8 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) e. RR )
281	200, 280	remulcld 9689	. . . . . . 7 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` Q ) ` ( D ` j ) ) ) ) ) ) e. RR )
282	74, 68	syl6eleq 2559	. . . . . . . . . 10 |- ( ph -> S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } )
283		oveq1 6315	. . . . . . . . . . . . 13 |- ( z = S -> ( z - ( A ` Z ) ) = ( S - ( A ` Z ) ) )
284	283	oveq2d 6324	. . . . . . . . . . . 12 |- ( z = S -> ( G x. ( z - ( A ` Z ) ) ) = ( G x. ( S - ( A ` Z ) ) ) )
285		fveq2 5879	. . . . . . . . . . . . . . . . 17 |- ( z = S -> ( H ` z ) = ( H ` S ) )
286	285	fveq1d 5881	. . . . . . . . . . . . . . . 16 |- ( z = S -> ( ( H ` z ) ` ( D ` j ) ) = ( ( H ` S ) ` ( D ` j ) ) )
287	286	oveq2d 6324	. . . . . . . . . . . . . . 15 |- ( z = S -> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) = ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
288	287	mpteq2dv 4483	. . . . . . . . . . . . . 14 |- ( z = S -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
289	288	fveq2d 5883	. . . . . . . . . . . . 13 |- ( z = S -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) = (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
290	289	oveq2d 6324	. . . . . . . . . . . 12 |- ( z = S -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
291	284, 290	breq12d 4408	. . . . . . . . . . 11 |- ( z = S -> ( ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) <-> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
292	291	elrab 3184	. . . . . . . . . 10 |- ( S e. { z e. ( ( A ` Z ) [,] ( B ` Z ) ) | ( G x. ( z - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` z ) ` ( D ` j ) ) ) ) ) ) } <-> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
293	282, 292	sylib 201	. . . . . . . . 9 |- ( ph -> ( S e. ( ( A ` Z ) [,] ( B ` Z ) ) /\ ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
294	293	simprd 470	. . . . . . . 8 |- ( ph -> ( G x. ( S - ( A ` Z ) ) ) <_ ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
295	207, 275	fsumrecl 13877	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. RR )
296	200, 295	remulcld 9689	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) e. RR )
297		0red 9662	. . . . . . . . . . 11 |- ( ph -> 0 e. RR )
298	75, 67	posdifd 10221	. . . . . . . . . . . 12 |- ( ph -> ( S < Q <-> 0 < ( Q - S ) ) )
299	144, 298	mpbid 215	. . . . . . . . . . 11 |- ( ph -> 0 < ( Q - S ) )
300	297, 183, 299	ltled 9800	. . . . . . . . . 10 |- ( ph -> 0 <_ ( Q - S ) )
301		hoidmvlelem2.le	. . . . . . . . . 10 |- ( ph -> G <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) )
302	172, 296, 183, 300, 301	lemul1ad 10568	. . . . . . . . 9 |- ( ph -> ( G x. ( Q - S ) ) <_ ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) )
303	200	recnd 9687	. . . . . . . . . . 11 |- ( ph -> ( 1 + E ) e. CC )
304	295	recnd 9687	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( P ` j ) e. CC )
305	303, 304, 174	mulassd 9684	. . . . . . . . . 10 |- ( ph -> ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) = ( ( 1 + E ) x. ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) ) )
306	275	recnd 9687	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( P ` j ) e. CC )
307	207, 174, 306	fsummulc1 13923	. . . . . . . . . . . 12 |- ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) )
308	174	adantr 472	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( Q - S ) e. CC )
309	306, 308	mulcomd 9682	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( P ` j ) x. ( Q - S ) ) = ( ( Q - S ) x. ( P ` j ) ) )
310	309	sumeq2dv 13846	. . . . . . . . . . . 12 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
311	307, 310	eqtrd 2505	. . . . . . . . . . 11 |- ( ph -> ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) = sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) )
312	311	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. ( sum_ j e. ( 1 ... M ) ( P ` j ) x. ( Q - S ) ) ) = ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
313	305, 312	eqtrd 2505	. . . . . . . . 9 |- ( ph -> ( ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( P ` j ) ) x. ( Q - S ) ) = ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
314	302, 313	breqtrd 4420	. . . . . . . 8 |- ( ph -> ( G x. ( Q - S ) ) <_ ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
315	192, 186, 206, 278, 294, 314	leadd12dd 37626	. . . . . . 7 |- ( ph -> ( ( G x. ( S - ( A ` Z ) ) ) + ( G x. ( Q - S ) ) ) <_ ( ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
316		hoidmvlelem2.m	. . . . . . . . . . . . . . . . 17 |- ( ph -> M e. NN )
317		nnsplit 37668	. . . . . . . . . . . . . . . . 17 |- ( M e. NN -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
318	316, 317	syl 17	. . . . . . . . . . . . . . . 16 |- ( ph -> NN = ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) )
319		uncom 3569	. . . . . . . . . . . . . . . . 17 |- ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) )
320	319	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ph -> ( ( 1 ... M ) u. ( ZZ>= ` ( M + 1 ) ) ) = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
321	318, 320	eqtr2d 2506	. . . . . . . . . . . . . . 15 |- ( ph -> ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) = NN )
322	321	eqcomd 2477	. . . . . . . . . . . . . 14 |- ( ph -> NN = ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) )
323	322	mpteq1d 4477	. . . . . . . . . . . . 13 |- ( ph -> ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) = ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) )
324	323	fveq2d 5883	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = (Σ^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) )
325		nfv 1769	. . . . . . . . . . . . 13 |- F/ j ph
326		fvex 5889	. . . . . . . . . . . . . 14 |- ( ZZ>= ` ( M + 1 ) ) e. _V
327	326	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ZZ>= ` ( M + 1 ) ) e. _V )
328		ovex 6336	. . . . . . . . . . . . . 14 |- ( 1 ... M ) e. _V
329	328	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( 1 ... M ) e. _V )
330		incom 3616	. . . . . . . . . . . . . . 15 |- ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) )
331		nnuzdisj 37665	. . . . . . . . . . . . . . 15 |- ( ( 1 ... M ) i^i ( ZZ>= ` ( M + 1 ) ) ) = (/)
332	330, 331	eqtri 2493	. . . . . . . . . . . . . 14 |- ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/)
333	332	a1i 11	. . . . . . . . . . . . 13 |- ( ph -> ( ( ZZ>= ` ( M + 1 ) ) i^i ( 1 ... M ) ) = (/) )
334		icossicc 11746	. . . . . . . . . . . . . 14 |- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
335		ssid 3437	. . . . . . . . . . . . . . 15 |- ( 0 [,) +oo ) C_ ( 0 [,) +oo )
336		simpl 464	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ph )
337	316	peano2nnd 10648	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( M + 1 ) e. NN )
338		uznnssnn 11229	. . . . . . . . . . . . . . . . . . 19 |- ( ( M + 1 ) e. NN -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
339	337, 338	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ph -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
340	339	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ZZ>= ` ( M + 1 ) ) C_ NN )
341		simpr 468	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. ( ZZ>= ` ( M + 1 ) ) )
342	340, 341	sseldd 3419	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> j e. NN )
343		snfi 7668	. . . . . . . . . . . . . . . . . . . . 21 |- { Z } e. Fin
344	343	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ph -> { Z } e. Fin )
345		unfi 7856	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Y e. Fin /\ { Z } e. Fin ) -> ( Y u. { Z } ) e. Fin )
346	164, 344, 345	syl2anc 673	. . . . . . . . . . . . . . . . . . 19 |- ( ph -> ( Y u. { Z } ) e. Fin )
347	7, 346	syl5eqel 2553	. . . . . . . . . . . . . . . . . 18 |- ( ph -> W e. Fin )
348	347	adantr 472	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> W e. Fin )
349		eleq1 2537	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> ( j e. Y <-> l e. Y ) )
350		fveq2 5879	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> ( c ` j ) = ( c ` l ) )
351	350	breq1d 4405	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( j = l -> ( ( c ` j ) <_ x <-> ( c ` l ) <_ x ) )
352	351, 350	ifbieq1d 3895	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( j = l -> if ( ( c ` j ) <_ x , ( c ` j ) , x ) = if ( ( c ` l ) <_ x , ( c ` l ) , x ) )
353	349, 350, 352	ifbieq12d 3899	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j = l -> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) = if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) )
354	353	cbvmptv 4488	. . . . . . . . . . . . . . . . . . . . 21 |- ( j e. W |-> if ( j e. Y , ( c ` j ) , if ( ( c ` j ) <_ x , ( c ` j ) , x ) ) ) = ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) )
355	354	mpteq2i 4479	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) )
356	355	mpteq2i 4479	. . . . . . . . . . . . . . . . . . 19 |- ( 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 ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) ) )
357	204, 356	eqtri 2493	. . . . . . . . . . . . . . . . . 18 |- H = ( x e. RR |-> ( c e. ( RR ^m W ) |-> ( l e. W |-> if ( l e. Y , ( c ` l ) , if ( ( c ` l ) <_ x , ( c ` l ) , x ) ) ) ) )
358	75	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> S e. RR )
359	357, 358, 348, 31	hsphoif 38516	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( ( H ` S ) ` ( D ` j ) ) : W --> RR )
360	161, 348, 112, 359	hoidmvcl 38522	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
361	336, 342, 360	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
362	335, 361	sseldi 3416	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
363	334, 362	sseldi 3416	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( ZZ>= ` ( M + 1 ) ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
364	209, 211, 360	syl2anc 673	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,) +oo ) )
365	334, 364	sseldi 3416	. . . . . . . . . . . . 13 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
366	325, 327, 329, 333, 363, 365	sge0splitmpt 38367	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( ( ZZ>= ` ( M + 1 ) ) u. ( 1 ... M ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
367		nnex 10637	. . . . . . . . . . . . . . 15 |- NN e. _V
368	367	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> NN e. _V )
369	334, 360	sseldi 3416	. . . . . . . . . . . . . 14 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. ( 0 [,] +oo ) )
370	325, 368, 369, 205, 339	sge0ssrempt 38361	. . . . . . . . . . . . 13 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
371	18	a1i 11	. . . . . . . . . . . . . 14 |- ( ph -> ( 1 ... M ) C_ NN )
372	325, 368, 369, 205, 371	sge0ssrempt 38361	. . . . . . . . . . . . 13 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR )
373		rexadd 11548	. . . . . . . . . . . . 13 |- ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR /\ (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. RR ) -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
374	370, 372, 373	syl2anc 673	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) +e (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
375	324, 366, 374	3eqtrd 2509	. . . . . . . . . . 11 |- ( ph -> (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) )
376	375	oveq2d 6324	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) = ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) )
377	376	oveq1d 6323	. . . . . . . . 9 |- ( ph -> ( ( ( 1 + E ) x. (Σ^ ` ( j e. NN |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
378	375, 205	eqeltrrd 2550	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. RR )
379	378	recnd 9687	. . . . . . . . . . 11 |- ( ph -> ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) e. CC )
380	277	recnd 9687	. . . . . . . . . . 11 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) e. CC )
381	303, 379, 380	adddid 9685	. . . . . . . . . 10 |- ( ph -> ( ( 1 + E ) x. ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
382	381	eqcomd 2477	. . . . . . . . 9 |- ( ph -> ( ( ( 1 + E ) x. ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) ) + ( ( 1 + E ) x. sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) = ( ( 1 + E ) x. ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
383	370	recnd 9687	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
384	372	recnd 9687	. . . . . . . . . . . 12 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) e. CC )
385	383, 384, 380	addassd 9683	. . . . . . . . . . 11 |- ( ph -> ( ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( (Σ^ ` ( j e. ( ZZ>= ` ( M + 1 ) ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + ( (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) ) )
386	207, 364	sge0fsummpt 38346	. . . . . . . . . . . . . 14 |- ( ph -> (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) = sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) )
387	386	oveq1d 6323	. . . . . . . . . . . . 13 |- ( ph -> ( (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
388		ax-resscn 9614	. . . . . . . . . . . . . . . . . 18 |- RR C_ CC
389	159, 388	sstri 3427	. . . . . . . . . . . . . . . . 17 |- ( 0 [,) +oo ) C_ CC
390	389, 360	sseldi 3416	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
391	209, 211, 390	syl2anc 673	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) e. CC )
392	183	adantr 472	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ j e. NN ) -> ( Q - S ) e. RR )
393	392, 274	remulcld 9689	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. RR )
394	393	recnd 9687	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ j e. NN ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
395	211, 394	syldan 478	. . . . . . . . . . . . . . 15 |- ( ( ph /\ j e. ( 1 ... M ) ) -> ( ( Q - S ) x. ( P ` j ) ) e. CC )
396	207, 391, 395	fsumadd 13882	. . . . . . . . . . . . . 14 |- ( ph -> sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) = ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) )
397	396	eqcomd 2477	. . . . . . . . . . . . 13 |- ( ph -> ( sum_ j e. ( 1 ... M ) ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + sum_ j e. ( 1 ... M ) ( ( Q - S ) x. ( P ` j ) ) ) = sum_ j e. ( 1 ... M ) ( ( ( C ` j ) ( L ` W ) ( ( H ` S ) ` ( D ` j ) ) ) + ( ( Q - S ) x. ( P ` j ) ) ) )
398	387, 397	eqtrd 2505	. . . . . . . . . . . 12 |- ( ph -> ( (Σ^ ` ( j e. ( 1 ... M ) |-> ( ( C ` j ) ( L ` W ) (