Theorem hoidmvle

Description: The dimensional volume of a n-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. Lemma 115B of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 21-Nov-2020)

	Ref	Expression
Hypotheses	hoidmvle.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 ) ) ) ) ) )
	hoidmvle.x	|- ( ph -> X e. Fin )
	hoidmvle.a	|- ( ph -> A : X --> RR )
	hoidmvle.b	|- ( ph -> B : X --> RR )
	hoidmvle.c	|- ( ph -> C : NN --> ( RR ^m X ) )
	hoidmvle.d	|- ( ph -> D : NN --> ( RR ^m X ) )
	hoidmvle.s	|- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
Assertion	hoidmvle	|- ( ph -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		hoidmvle.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		hoidmvle.x	|- ( ph -> X e. Fin )
3		hoidmvle.a	|- ( ph -> A : X --> RR )
4		hoidmvle.b	|- ( ph -> B : X --> RR )
5		hoidmvle.c	|- ( ph -> C : NN --> ( RR ^m X ) )
6		hoidmvle.d	|- ( ph -> D : NN --> ( RR ^m X ) )
7		hoidmvle.s	|- ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
8		ovex	|- ( RR ^m X ) e. _V
9		nnex	|- NN e. _V
10	8 9	pm3.2i	|- ( ( RR ^m X ) e. _V /\ NN e. _V )
11	10	a1i	|- ( ph -> ( ( RR ^m X ) e. _V /\ NN e. _V ) )
12		elmapg	|- ( ( ( RR ^m X ) e. _V /\ NN e. _V ) -> ( D e. ( ( RR ^m X ) ^m NN ) <-> D : NN --> ( RR ^m X ) ) )
13	11 12	syl	|- ( ph -> ( D e. ( ( RR ^m X ) ^m NN ) <-> D : NN --> ( RR ^m X ) ) )
14	6 13	mpbird	|- ( ph -> D e. ( ( RR ^m X ) ^m NN ) )
15		elmapg	|- ( ( ( RR ^m X ) e. _V /\ NN e. _V ) -> ( C e. ( ( RR ^m X ) ^m NN ) <-> C : NN --> ( RR ^m X ) ) )
16	11 15	syl	|- ( ph -> ( C e. ( ( RR ^m X ) ^m NN ) <-> C : NN --> ( RR ^m X ) ) )
17	5 16	mpbird	|- ( ph -> C e. ( ( RR ^m X ) ^m NN ) )
18		reex	|- RR e. _V
19	18	a1i	|- ( ph -> RR e. _V )
20	19 2	jca	|- ( ph -> ( RR e. _V /\ X e. Fin ) )
21		elmapg	|- ( ( RR e. _V /\ X e. Fin ) -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
22	20 21	syl	|- ( ph -> ( B e. ( RR ^m X ) <-> B : X --> RR ) )
23	4 22	mpbird	|- ( ph -> B e. ( RR ^m X ) )
24		elmapg	|- ( ( RR e. _V /\ X e. Fin ) -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
25	20 24	syl	|- ( ph -> ( A e. ( RR ^m X ) <-> A : X --> RR ) )
26	3 25	mpbird	|- ( ph -> A e. ( RR ^m X ) )
27		oveq2	|- ( x = (/) -> ( RR ^m x ) = ( RR ^m (/) ) )
28	27	eleq2d	|- ( x = (/) -> ( a e. ( RR ^m x ) <-> a e. ( RR ^m (/) ) ) )
29	27	eleq2d	|- ( x = (/) -> ( b e. ( RR ^m x ) <-> b e. ( RR ^m (/) ) ) )
30	27	oveq1d	|- ( x = (/) -> ( ( RR ^m x ) ^m NN ) = ( ( RR ^m (/) ) ^m NN ) )
31	30	eleq2d	|- ( x = (/) -> ( c e. ( ( RR ^m x ) ^m NN ) <-> c e. ( ( RR ^m (/) ) ^m NN ) ) )
32	30	eleq2d	|- ( x = (/) -> ( d e. ( ( RR ^m x ) ^m NN ) <-> d e. ( ( RR ^m (/) ) ^m NN ) ) )
33		ixpeq1	|- ( x = (/) -> X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) )
34		ixpeq1	|- ( x = (/) -> X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
35	34	iuneq2d	|- ( x = (/) -> U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
36	33 35	sseq12d	|- ( x = (/) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
37		fveq2	|- ( x = (/) -> ( L ` x ) = ( L ` (/) ) )
38	37	oveqd	|- ( x = (/) -> ( a ( L ` x ) b ) = ( a ( L ` (/) ) b ) )
39	37	oveqd	|- ( x = (/) -> ( ( c ` j ) ( L ` x ) ( d ` j ) ) = ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) )
40	39	mpteq2dv	|- ( x = (/) -> ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) )
41	40	fveq2d	|- ( x = (/) -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
42	38 41	breq12d	|- ( x = (/) -> ( ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) <-> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
43	36 42	imbi12d	|- ( x = (/) -> ( ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) )
44	32 43	imbi12d	|- ( x = (/) -> ( ( d e. ( ( RR ^m x ) ^m NN ) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( d e. ( ( RR ^m (/) ) ^m NN ) -> ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) ) )
45	44	ralbidv2	|- ( x = (/) -> ( A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) )
46	31 45	imbi12d	|- ( x = (/) -> ( ( c e. ( ( RR ^m x ) ^m NN ) -> A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( c e. ( ( RR ^m (/) ) ^m NN ) -> A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) ) )
47	46	ralbidv2	|- ( x = (/) -> ( A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) )
48	29 47	imbi12d	|- ( x = (/) -> ( ( b e. ( RR ^m x ) -> A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( b e. ( RR ^m (/) ) -> A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) ) )
49	48	ralbidv2	|- ( x = (/) -> ( A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) )
50	28 49	imbi12d	|- ( x = (/) -> ( ( a e. ( RR ^m x ) -> A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( a e. ( RR ^m (/) ) -> A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) ) )
51	50	ralbidv2	|- ( x = (/) -> ( A. a e. ( RR ^m x ) A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. a e. ( RR ^m (/) ) A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) ) )
52		oveq2	|- ( x = y -> ( RR ^m x ) = ( RR ^m y ) )
53	52	eleq2d	|- ( x = y -> ( a e. ( RR ^m x ) <-> a e. ( RR ^m y ) ) )
54	52	eleq2d	|- ( x = y -> ( b e. ( RR ^m x ) <-> b e. ( RR ^m y ) ) )
55	52	oveq1d	|- ( x = y -> ( ( RR ^m x ) ^m NN ) = ( ( RR ^m y ) ^m NN ) )
56	55	eleq2d	|- ( x = y -> ( c e. ( ( RR ^m x ) ^m NN ) <-> c e. ( ( RR ^m y ) ^m NN ) ) )
57	55	eleq2d	|- ( x = y -> ( d e. ( ( RR ^m x ) ^m NN ) <-> d e. ( ( RR ^m y ) ^m NN ) ) )
58		ixpeq1	|- ( x = y -> X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) )
59		ixpeq1	|- ( x = y -> X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
60	59	iuneq2d	|- ( x = y -> U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
61	58 60	sseq12d	|- ( x = y -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
62		fveq2	|- ( x = y -> ( L ` x ) = ( L ` y ) )
63	62	oveqd	|- ( x = y -> ( a ( L ` x ) b ) = ( a ( L ` y ) b ) )
64	62	oveqd	|- ( x = y -> ( ( c ` j ) ( L ` x ) ( d ` j ) ) = ( ( c ` j ) ( L ` y ) ( d ` j ) ) )
65	64	mpteq2dv	|- ( x = y -> ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) )
66	65	fveq2d	|- ( x = y -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) )
67	63 66	breq12d	|- ( x = y -> ( ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) <-> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
68	61 67	imbi12d	|- ( x = y -> ( ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
69	57 68	imbi12d	|- ( x = y -> ( ( d e. ( ( RR ^m x ) ^m NN ) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( d e. ( ( RR ^m y ) ^m NN ) -> ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) ) )
70	69	ralbidv2	|- ( x = y -> ( A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
71	56 70	imbi12d	|- ( x = y -> ( ( c e. ( ( RR ^m x ) ^m NN ) -> A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( c e. ( ( RR ^m y ) ^m NN ) -> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) ) )
72	71	ralbidv2	|- ( x = y -> ( A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
73	54 72	imbi12d	|- ( x = y -> ( ( b e. ( RR ^m x ) -> A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( b e. ( RR ^m y ) -> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) ) )
74	73	ralbidv2	|- ( x = y -> ( A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
75	53 74	imbi12d	|- ( x = y -> ( ( a e. ( RR ^m x ) -> A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( a e. ( RR ^m y ) -> A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) ) )
76	75	ralbidv2	|- ( x = y -> ( A. a e. ( RR ^m x ) A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
77		oveq2	|- ( x = ( y u. { z } ) -> ( RR ^m x ) = ( RR ^m ( y u. { z } ) ) )
78	77	eleq2d	|- ( x = ( y u. { z } ) -> ( a e. ( RR ^m x ) <-> a e. ( RR ^m ( y u. { z } ) ) ) )
79	77	eleq2d	|- ( x = ( y u. { z } ) -> ( b e. ( RR ^m x ) <-> b e. ( RR ^m ( y u. { z } ) ) ) )
80	77	oveq1d	|- ( x = ( y u. { z } ) -> ( ( RR ^m x ) ^m NN ) = ( ( RR ^m ( y u. { z } ) ) ^m NN ) )
81	80	eleq2d	|- ( x = ( y u. { z } ) -> ( c e. ( ( RR ^m x ) ^m NN ) <-> c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) )
82	80	eleq2d	|- ( x = ( y u. { z } ) -> ( d e. ( ( RR ^m x ) ^m NN ) <-> d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) )
83		ixpeq1	|- ( x = ( y u. { z } ) -> X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) )
84		ixpeq1	|- ( x = ( y u. { z } ) -> X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
85	84	iuneq2d	|- ( x = ( y u. { z } ) -> U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
86	83 85	sseq12d	|- ( x = ( y u. { z } ) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
87		fveq2	|- ( x = ( y u. { z } ) -> ( L ` x ) = ( L ` ( y u. { z } ) ) )
88	87	oveqd	|- ( x = ( y u. { z } ) -> ( a ( L ` x ) b ) = ( a ( L ` ( y u. { z } ) ) b ) )
89	87	oveqd	|- ( x = ( y u. { z } ) -> ( ( c ` j ) ( L ` x ) ( d ` j ) ) = ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) )
90	89	mpteq2dv	|- ( x = ( y u. { z } ) -> ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) )
91	90	fveq2d	|- ( x = ( y u. { z } ) -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
92	88 91	breq12d	|- ( x = ( y u. { z } ) -> ( ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) <-> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
93	86 92	imbi12d	|- ( x = ( y u. { z } ) -> ( ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
94	82 93	imbi12d	|- ( x = ( y u. { z } ) -> ( ( d e. ( ( RR ^m x ) ^m NN ) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) ) )
95	94	ralbidv2	|- ( x = ( y u. { z } ) -> ( A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
96	81 95	imbi12d	|- ( x = ( y u. { z } ) -> ( ( c e. ( ( RR ^m x ) ^m NN ) -> A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) ) )
97	96	ralbidv2	|- ( x = ( y u. { z } ) -> ( A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
98	79 97	imbi12d	|- ( x = ( y u. { z } ) -> ( ( b e. ( RR ^m x ) -> A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( b e. ( RR ^m ( y u. { z } ) ) -> A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) ) )
99	98	ralbidv2	|- ( x = ( y u. { z } ) -> ( A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
100	78 99	imbi12d	|- ( x = ( y u. { z } ) -> ( ( a e. ( RR ^m x ) -> A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( a e. ( RR ^m ( y u. { z } ) ) -> A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) ) )
101	100	ralbidv2	|- ( x = ( y u. { z } ) -> ( A. a e. ( RR ^m x ) A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. a e. ( RR ^m ( y u. { z } ) ) A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
102		oveq2	|- ( x = X -> ( RR ^m x ) = ( RR ^m X ) )
103	102	eleq2d	|- ( x = X -> ( a e. ( RR ^m x ) <-> a e. ( RR ^m X ) ) )
104	102	eleq2d	|- ( x = X -> ( b e. ( RR ^m x ) <-> b e. ( RR ^m X ) ) )
105	102	oveq1d	|- ( x = X -> ( ( RR ^m x ) ^m NN ) = ( ( RR ^m X ) ^m NN ) )
106	105	eleq2d	|- ( x = X -> ( c e. ( ( RR ^m x ) ^m NN ) <-> c e. ( ( RR ^m X ) ^m NN ) ) )
107	105	eleq2d	|- ( x = X -> ( d e. ( ( RR ^m x ) ^m NN ) <-> d e. ( ( RR ^m X ) ^m NN ) ) )
108		ixpeq1	|- ( x = X -> X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) )
109		ixpeq1	|- ( x = X -> X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
110	109	iuneq2d	|- ( x = X -> U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
111	108 110	sseq12d	|- ( x = X -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
112		fveq2	|- ( x = X -> ( L ` x ) = ( L ` X ) )
113	112	oveqd	|- ( x = X -> ( a ( L ` x ) b ) = ( a ( L ` X ) b ) )
114	112	oveqd	|- ( x = X -> ( ( c ` j ) ( L ` x ) ( d ` j ) ) = ( ( c ` j ) ( L ` X ) ( d ` j ) ) )
115	114	mpteq2dv	|- ( x = X -> ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) )
116	115	fveq2d	|- ( x = X -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) )
117	113 116	breq12d	|- ( x = X -> ( ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) <-> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
118	111 117	imbi12d	|- ( x = X -> ( ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
119	107 118	imbi12d	|- ( x = X -> ( ( d e. ( ( RR ^m x ) ^m NN ) -> ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( d e. ( ( RR ^m X ) ^m NN ) -> ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) ) )
120	119	ralbidv2	|- ( x = X -> ( A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
121	106 120	imbi12d	|- ( x = X -> ( ( c e. ( ( RR ^m x ) ^m NN ) -> A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( c e. ( ( RR ^m X ) ^m NN ) -> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) ) )
122	121	ralbidv2	|- ( x = X -> ( A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
123	104 122	imbi12d	|- ( x = X -> ( ( b e. ( RR ^m x ) -> A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( b e. ( RR ^m X ) -> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) ) )
124	123	ralbidv2	|- ( x = X -> ( A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
125	103 124	imbi12d	|- ( x = X -> ( ( a e. ( RR ^m x ) -> A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) ) <-> ( a e. ( RR ^m X ) -> A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) ) )
126	125	ralbidv2	|- ( x = X -> ( A. a e. ( RR ^m x ) A. b e. ( RR ^m x ) A. c e. ( ( RR ^m x ) ^m NN ) A. d e. ( ( RR ^m x ) ^m NN ) ( X_ k e. x ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. x ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` x ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` x ) ( d ` j ) ) ) ) ) <-> A. a e. ( RR ^m X ) A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
127		fveq1	|- ( a = e -> ( a ` k ) = ( e ` k ) )
128	127	oveq1d	|- ( a = e -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( e ` k ) [,) ( b ` k ) ) )
129	128	fveq2d	|- ( a = e -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) )
130	129	prodeq2ad	|- ( a = e -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) )
131	130	ifeq2d	|- ( a = e -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) ) )
132		fveq1	|- ( b = f -> ( b ` k ) = ( f ` k ) )
133	132	oveq2d	|- ( b = f -> ( ( e ` k ) [,) ( b ` k ) ) = ( ( e ` k ) [,) ( f ` k ) ) )
134	133	fveq2d	|- ( b = f -> ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) )
135	134	prodeq2ad	|- ( b = f -> prod_ k e. x ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) )
136	135	ifeq2d	|- ( b = f -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) ) )
137	131 136	cbvmpov	|- ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( e e. ( RR ^m x ) , f e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) ) )
138	137	mpteq2i	|- ( 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 ) ) ) ) ) ) = ( x e. Fin |-> ( e e. ( RR ^m x ) , f e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) ) ) )
139	1 138	eqtri	|- L = ( x e. Fin |-> ( e e. ( RR ^m x ) , f e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( e ` k ) [,) ( f ` k ) ) ) ) ) )
140		elmapi	|- ( a e. ( RR ^m (/) ) -> a : (/) --> RR )
141	140	adantr	|- ( ( a e. ( RR ^m (/) ) /\ b e. ( RR ^m (/) ) ) -> a : (/) --> RR )
142		elmapi	|- ( b e. ( RR ^m (/) ) -> b : (/) --> RR )
143	142	adantl	|- ( ( a e. ( RR ^m (/) ) /\ b e. ( RR ^m (/) ) ) -> b : (/) --> RR )
144	139 141 143	hoidmv0val	|- ( ( a e. ( RR ^m (/) ) /\ b e. ( RR ^m (/) ) ) -> ( a ( L ` (/) ) b ) = 0 )
145	144	ad5ant23	|- ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> ( a ( L ` (/) ) b ) = 0 )
146		nfv	|- F/ j ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) )
147	9	a1i	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> NN e. _V )
148		icossicc	|- ( 0 [,) +oo ) C_ ( 0 [,] +oo )
149		0fi	|- (/) e. Fin
150	149	a1i	|- ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> (/) e. Fin )
151		ovexd	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( RR ^m (/) ) e. _V )
152	9	a1i	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> NN e. _V )
153		simpl	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> c e. ( ( RR ^m (/) ) ^m NN ) )
154		simpr	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> j e. NN )
155	151 152 153 154	fvmap	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( c ` j ) e. ( RR ^m (/) ) )
156		elmapi	|- ( ( c ` j ) e. ( RR ^m (/) ) -> ( c ` j ) : (/) --> RR )
157	155 156	syl	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( c ` j ) : (/) --> RR )
158	157	adantlr	|- ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( c ` j ) : (/) --> RR )
159		ovexd	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( RR ^m (/) ) e. _V )
160	9	a1i	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> NN e. _V )
161		simpl	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> d e. ( ( RR ^m (/) ) ^m NN ) )
162		simpr	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> j e. NN )
163	159 160 161 162	fvmap	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( d ` j ) e. ( RR ^m (/) ) )
164		elmapi	|- ( ( d ` j ) e. ( RR ^m (/) ) -> ( d ` j ) : (/) --> RR )
165	163 164	syl	|- ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( d ` j ) : (/) --> RR )
166	165	adantll	|- ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( d ` j ) : (/) --> RR )
167	1 150 158 166	hoidmvcl	|- ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) e. ( 0 [,) +oo ) )
168	148 167	sselid	|- ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) e. ( 0 [,] +oo ) )
169	146 147 168	sge0ge0mpt	|- ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
170	169	adantll	|- ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
171	145 170	eqbrtrd	|- ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
172	171	a1d	|- ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
173	172	ralrimiva	|- ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) -> A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
174	173	ralrimiva	|- ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) -> A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
175	174	ralrimiva	|- ( ( ph /\ a e. ( RR ^m (/) ) ) -> A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
176	175	ralrimiva	|- ( ph -> A. a e. ( RR ^m (/) ) A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
177		simpl	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) -> ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) )
178	128	ixpeq2dv	|- ( a = e -> X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) )
179	178	sseq1d	|- ( a = e -> ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
180		oveq1	|- ( a = e -> ( a ( L ` y ) b ) = ( e ( L ` y ) b ) )
181	180	breq1d	|- ( a = e -> ( ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
182	179 181	imbi12d	|- ( a = e -> ( ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
183	182	ralbidv	|- ( a = e -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
184	183	ralbidv	|- ( a = e -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
185	184	ralbidv	|- ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
186	133	ixpeq2dv	|- ( b = f -> X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) = X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) )
187	186	sseq1d	|- ( b = f -> ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
188		oveq2	|- ( b = f -> ( e ( L ` y ) b ) = ( e ( L ` y ) f ) )
189	188	breq1d	|- ( b = f -> ( ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
190	187 189	imbi12d	|- ( b = f -> ( ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
191	190	ralbidv	|- ( b = f -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
192	191	ralbidv	|- ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
193		fveq1	|- ( c = g -> ( c ` j ) = ( g ` j ) )
194	193	fveq1d	|- ( c = g -> ( ( c ` j ) ` k ) = ( ( g ` j ) ` k ) )
195	194	oveq1d	|- ( c = g -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
196	195	ixpeq2dv	|- ( c = g -> X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
197	196	adantr	|- ( ( c = g /\ j e. NN ) -> X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
198	197	iuneq2dv	|- ( c = g -> U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
199	198	sseq2d	|- ( c = g -> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
200	193	oveq1d	|- ( c = g -> ( ( c ` j ) ( L ` y ) ( d ` j ) ) = ( ( g ` j ) ( L ` y ) ( d ` j ) ) )
201	200	mpteq2dv	|- ( c = g -> ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) = ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) )
202	201	fveq2d	|- ( c = g -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) )
203	202	breq2d	|- ( c = g -> ( ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
204	199 203	imbi12d	|- ( c = g -> ( ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
205	204	ralbidv	|- ( c = g -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d 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 ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
206		fveq1	|- ( d = h -> ( d ` j ) = ( h ` j ) )
207	206	fveq1d	|- ( d = h -> ( ( d ` j ) ` k ) = ( ( h ` j ) ` k ) )
208	207	oveq2d	|- ( d = h -> ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
209	208	ixpeq2dv	|- ( d = h -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
210	209	adantr	|- ( ( d = h /\ j e. NN ) -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
211	210	iuneq2dv	|- ( d = h -> U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
212	211	sseq2d	|- ( d = h -> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) ) )
213	206	oveq2d	|- ( d = h -> ( ( g ` j ) ( L ` y ) ( d ` j ) ) = ( ( g ` j ) ( L ` y ) ( h ` j ) ) )
214	213	mpteq2dv	|- ( d = h -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) = ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) )
215	214	fveq2d	|- ( d = h -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) )
216	215	breq2d	|- ( d = h -> ( ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
217	212 216	imbi12d	|- ( d = h -> ( ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( 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 ) ) ) ) ) ) )
218	217	cbvralvw	|- ( A. d 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 ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) )
219	218	a1i	|- ( c = g -> ( A. d 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 ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
220	205 219	bitrd	|- ( c = g -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
221	220	cbvralvw	|- ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) )
222	221	a1i	|- ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
223	192 222	bitrd	|- ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) ) )
224	223	cbvralvw	|- ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` 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 ( ( 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 ) ) ) ) ) )
225	224	a1i	|- ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` 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 ( ( 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 ) ) ) ) ) ) )
226	185 225	bitrd	|- ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` 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 ( ( 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 ) ) ) ) ) ) )
227	226	cbvralvw	|- ( A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> 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 ) ) ) ) ) )
228	227	biimpi	|- ( A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) -> 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 ) ) ) ) ) )
229	228	adantl	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) -> 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 ) ) ) ) ) )
230		simplll	|- ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> ph )
231		eldifi	|- ( z e. ( X \ y ) -> z e. X )
232	231	adantl	|- ( ( ph /\ z e. ( X \ y ) ) -> z e. X )
233	232	adantrl	|- ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) -> z e. X )
234	233	ad2antrr	|- ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> z e. X )
235		simpl	|- ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> a e. ( RR ^m ( y u. { z } ) ) )
236		uneq1	|- ( y = (/) -> ( y u. { z } ) = ( (/) u. { z } ) )
237		0un	|- ( (/) u. { z } ) = { z }
238	237	a1i	|- ( y = (/) -> ( (/) u. { z } ) = { z } )
239	236 238	eqtr2d	|- ( y = (/) -> { z } = ( y u. { z } ) )
240	239	eqcomd	|- ( y = (/) -> ( y u. { z } ) = { z } )
241	240	oveq2d	|- ( y = (/) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
242	241	adantl	|- ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
243	235 242	eleqtrd	|- ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> a e. ( RR ^m { z } ) )
244	243	adantll	|- ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> a e. ( RR ^m { z } ) )
245	230 234 244	jca31	|- ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) )
246	245	adantllr	|- ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) )
247	246	adantlr	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) )
248	247	adantlr	|- ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) )
249		simpl	|- ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> b e. ( RR ^m ( y u. { z } ) ) )
250	241	adantl	|- ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
251	249 250	eleqtrd	|- ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> b e. ( RR ^m { z } ) )
252	251	adantlr	|- ( ( ( b e. ( RR ^m ( y u. { z } ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> b e. ( RR ^m { z } ) )
253	252	adantlll	|- ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> b e. ( RR ^m { z } ) )
254		simpl	|- ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) )
255	241	oveq1d	|- ( y = (/) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
256	255	adantl	|- ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
257	254 256	eleqtrd	|- ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> c e. ( ( RR ^m { z } ) ^m NN ) )
258	257	adantll	|- ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> c e. ( ( RR ^m { z } ) ^m NN ) )
259	248 253 258	jca31	|- ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) )
260	259	adantlr	|- ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) )
261	260	adantlr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) )
262		simpl	|- ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) )
263	255	adantl	|- ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
264	262 263	eleqtrd	|- ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> d e. ( ( RR ^m { z } ) ^m NN ) )
265	264	adantlr	|- ( ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> d e. ( ( RR ^m { z } ) ^m NN ) )
266	265	adantlll	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> d e. ( ( RR ^m { z } ) ^m NN ) )
267		simpl	|- ( ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) /\ y = (/) ) -> X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
268	239	ixpeq1d	|- ( y = (/) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) )
269	268	adantl	|- ( ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) /\ y = (/) ) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) )
270	239	ixpeq1d	|- ( y = (/) -> X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
271	270	adantr	|- ( ( y = (/) /\ i e. NN ) -> X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
272	271	iuneq2dv	|- ( y = (/) -> U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ i e. NN X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
273		fveq2	|- ( i = j -> ( c ` i ) = ( c ` j ) )
274	273	fveq1d	|- ( i = j -> ( ( c ` i ) ` k ) = ( ( c ` j ) ` k ) )
275		fveq2	|- ( i = j -> ( d ` i ) = ( d ` j ) )
276	275	fveq1d	|- ( i = j -> ( ( d ` i ) ` k ) = ( ( d ` j ) ` k ) )
277	274 276	oveq12d	|- ( i = j -> ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
278	277	ixpeq2dv	|- ( i = j -> X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
279	278	cbviunv	|- U_ i e. NN X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) )
280	279	a1i	|- ( y = (/) -> U_ i e. NN X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
281	272 280	eqtrd	|- ( y = (/) -> U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
282	281	adantl	|- ( ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) /\ y = (/) ) -> U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
283	269 282	sseq12d	|- ( ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) /\ y = (/) ) -> ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) <-> X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
284	267 283	mpbird	|- ( ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) /\ y = (/) ) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
285	284	adantll	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
286	261 266 285	jca31	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) )
287		simpr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> y = (/) )
288		fveq1	|- ( a = u -> ( a ` k ) = ( u ` k ) )
289	288	oveq1d	|- ( a = u -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( u ` k ) [,) ( b ` k ) ) )
290	289	fveq2d	|- ( a = u -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) )
291	290	prodeq2ad	|- ( a = u -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) )
292	291	ifeq2d	|- ( a = u -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) ) )
293		fveq2	|- ( k = l -> ( u ` k ) = ( u ` l ) )
294		fveq2	|- ( k = l -> ( b ` k ) = ( b ` l ) )
295	293 294	oveq12d	|- ( k = l -> ( ( u ` k ) [,) ( b ` k ) ) = ( ( u ` l ) [,) ( b ` l ) ) )
296	295	fveq2d	|- ( k = l -> ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) )
297	296	cbvprodv	|- prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) )
298	297	a1i	|- ( b = v -> prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) )
299		fveq1	|- ( b = v -> ( b ` l ) = ( v ` l ) )
300	299	oveq2d	|- ( b = v -> ( ( u ` l ) [,) ( b ` l ) ) = ( ( u ` l ) [,) ( v ` l ) ) )
301	300	fveq2d	|- ( b = v -> ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) = ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
302	301	prodeq2ad	|- ( b = v -> prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
303	298 302	eqtrd	|- ( b = v -> prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
304	303	ifeq2d	|- ( b = v -> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) ) = if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) ) )
305	292 304	cbvmpov	|- ( a e. ( RR ^m x ) , b e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) ) ) = ( u e. ( RR ^m x ) , v e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) ) )
306	305	mpteq2i	|- ( 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 ) ) ) ) ) ) = ( x e. Fin |-> ( u e. ( RR ^m x ) , v e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) ) ) )
307	1 306	eqtri	|- L = ( x e. Fin |-> ( u e. ( RR ^m x ) , v e. ( RR ^m x ) |-> if ( x = (/) , 0 , prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) ) ) )
308		simp-6r	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> z e. X )
309		eqid	|- { z } = { z }
310		elmapi	|- ( a e. ( RR ^m { z } ) -> a : { z } --> RR )
311	310	ad2antlr	|- ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) -> a : { z } --> RR )
312	311	ad3antrrr	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> a : { z } --> RR )
313		elmapi	|- ( b e. ( RR ^m { z } ) -> b : { z } --> RR )
314	313	adantl	|- ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) -> b : { z } --> RR )
315	314	ad3antrrr	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> b : { z } --> RR )
316		elmapi	|- ( c e. ( ( RR ^m { z } ) ^m NN ) -> c : NN --> ( RR ^m { z } ) )
317	316	adantl	|- ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) -> c : NN --> ( RR ^m { z } ) )
318	317	ad2antrr	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> c : NN --> ( RR ^m { z } ) )
319		elmapi	|- ( d e. ( ( RR ^m { z } ) ^m NN ) -> d : NN --> ( RR ^m { z } ) )
320	319	ad2antlr	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> d : NN --> ( RR ^m { z } ) )
321		id	|- ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
322		fveq2	|- ( k = l -> ( a ` k ) = ( a ` l ) )
323	322 294	oveq12d	|- ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) )
324		eqcom	|- ( k = l <-> l = k )
325	324	imbi1i	|- ( ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) )
326		eqcom	|- ( ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) <-> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) )
327	326	imbi2i	|- ( ( l = k -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) ) )
328	325 327	bitri	|- ( ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) ) )
329	323 328	mpbi	|- ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) )
330	329	cbvixpv	|- X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) = X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) )
331	330	a1i	|- ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) -> X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) = X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) )
332	277	ixpeq2dv	|- ( i = j -> X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
333	332	cbviunv	|- U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = U_ j e. NN X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) )
334		fveq2	|- ( k = l -> ( ( c ` j ) ` k ) = ( ( c ` j ) ` l ) )
335		fveq2	|- ( k = l -> ( ( d ` j ) ` k ) = ( ( d ` j ) ` l ) )
336	334 335	oveq12d	|- ( k = l -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
337	336	cbvixpv	|- X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) )
338	337	a1i	|- ( j e. NN -> X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
339	338	iuneq2i	|- U_ j e. NN X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) )
340	333 339	eqtr2i	|- U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) = U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) )
341	340	a1i	|- ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) -> U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) = U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
342	331 341	sseq12d	|- ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) -> ( X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) C_ U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) <-> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) )
343	321 342	mpbird	|- ( X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) -> X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) C_ U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
344	343	adantl	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) C_ U_ j e. NN X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
345	307 308 309 312 315 318 320 344	hoidmv1le	|- ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) -> ( a ( L ` { z } ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) )
346	345	adantr	|- ( ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) /\ y = (/) ) -> ( a ( L ` { z } ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) )
347	236 238	eqtrd	|- ( y = (/) -> ( y u. { z } ) = { z } )
348	347	fveq2d	|- ( y = (/) -> ( L ` ( y u. { z } ) ) = ( L ` { z } ) )
349	348	oveqd	|- ( y = (/) -> ( a ( L ` ( y u. { z } ) ) b ) = ( a ( L ` { z } ) b ) )
350	349	adantl	|- ( ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) /\ y = (/) ) -> ( a ( L ` ( y u. { z } ) ) b ) = ( a ( L ` { z } ) b ) )
351	348	oveqd	|- ( y = (/) -> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) = ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) )
352	351	mpteq2dv	|- ( y = (/) -> ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) )
353	352	fveq2d	|- ( y = (/) -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) )
354	353	adantl	|- ( ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) /\ y = (/) ) -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) )
355	350 354	breq12d	|- ( ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) /\ y = (/) ) -> ( ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) <-> ( a ( L ` { z } ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) ) )
356	346 355	mpbird	|- ( ( ( ( ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) /\ c e. ( ( RR ^m { z } ) ^m NN ) ) /\ d e. ( ( RR ^m { z } ) ^m NN ) ) /\ X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) C_ U_ i e. NN X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) ) /\ y = (/) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
357	286 287 356	syl2anc	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ y = (/) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
358	2	ad8antr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> X e. Fin )
359		simplrl	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 ) ) ) ) ) ) -> y C_ X )
360	359	ad3antrrr	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> y C_ X )
361	360	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> y C_ X )
362		simplrr	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 ) ) ) ) ) ) -> z e. ( X \ y ) )
363	362	ad3antrrr	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> z e. ( X \ y ) )
364	363	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> z e. ( X \ y ) )
365		eqid	|- ( y u. { z } ) = ( y u. { z } )
366		elmapi	|- ( a e. ( RR ^m ( y u. { z } ) ) -> a : ( y u. { z } ) --> RR )
367	366	adantr	|- ( ( a e. ( RR ^m ( y u. { z } ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) -> a : ( y u. { z } ) --> RR )
368	367	ad4ant23	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> a : ( y u. { z } ) --> RR )
369	368	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> a : ( y u. { z } ) --> RR )
370		elmapi	|- ( b e. ( RR ^m ( y u. { z } ) ) -> b : ( y u. { z } ) --> RR )
371	370	adantl	|- ( ( a e. ( RR ^m ( y u. { z } ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) -> b : ( y u. { z } ) --> RR )
372	371	ad4ant23	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> b : ( y u. { z } ) --> RR )
373	372	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> b : ( y u. { z } ) --> RR )
374		elmapi	|- ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> c : NN --> ( RR ^m ( y u. { z } ) ) )
375	374	adantl	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> c : NN --> ( RR ^m ( y u. { z } ) ) )
376	375	ad3antrrr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> c : NN --> ( RR ^m ( y u. { z } ) ) )
377		elmapi	|- ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> d : NN --> ( RR ^m ( y u. { z } ) ) )
378	377	ad2antrr	|- ( ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> d : NN --> ( RR ^m ( y u. { z } ) ) )
379	378	adantlll	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> d : NN --> ( RR ^m ( y u. { z } ) ) )
380		fveq2	|- ( k = l -> ( e ` k ) = ( e ` l ) )
381		fveq2	|- ( k = l -> ( f ` k ) = ( f ` l ) )
382	380 381	oveq12d	|- ( k = l -> ( ( e ` k ) [,) ( f ` k ) ) = ( ( e ` l ) [,) ( f ` l ) ) )
383	382	cbvixpv	|- X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) = X_ l e. y ( ( e ` l ) [,) ( f ` l ) )
384	383	a1i	|- ( h = o -> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) = X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) )
385		fveq2	|- ( j = i -> ( g ` j ) = ( g ` i ) )
386	385	fveq1d	|- ( j = i -> ( ( g ` j ) ` k ) = ( ( g ` i ) ` k ) )
387		fveq2	|- ( j = i -> ( h ` j ) = ( h ` i ) )
388	387	fveq1d	|- ( j = i -> ( ( h ` j ) ` k ) = ( ( h ` i ) ` k ) )
389	386 388	oveq12d	|- ( j = i -> ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) )
390	389	ixpeq2dv	|- ( j = i -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) )
391	390	cbviunv	|- U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = U_ i e. NN X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) )
392	391	a1i	|- ( h = o -> U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = U_ i e. NN X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) )
393		fveq2	|- ( k = l -> ( ( g ` i ) ` k ) = ( ( g ` i ) ` l ) )
394		fveq2	|- ( k = l -> ( ( h ` i ) ` k ) = ( ( h ` i ) ` l ) )
395	393 394	oveq12d	|- ( k = l -> ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) )
396	395	cbvixpv	|- X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) )
397	396	a1i	|- ( h = o -> X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) )
398		fveq1	|- ( h = o -> ( h ` i ) = ( o ` i ) )
399	398	fveq1d	|- ( h = o -> ( ( h ` i ) ` l ) = ( ( o ` i ) ` l ) )
400	399	oveq2d	|- ( h = o -> ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) = ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
401	400	ixpeq2dv	|- ( h = o -> X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
402	397 401	eqtrd	|- ( h = o -> X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
403	402	adantr	|- ( ( h = o /\ i e. NN ) -> X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
404	403	iuneq2dv	|- ( h = o -> U_ i e. NN X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
405	392 404	eqtrd	|- ( h = o -> U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
406	384 405	sseq12d	|- ( h = o -> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) <-> X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) ) )
407	385 387	oveq12d	|- ( j = i -> ( ( g ` j ) ( L ` y ) ( h ` j ) ) = ( ( g ` i ) ( L ` y ) ( h ` i ) ) )
408	407	cbvmptv	|- ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) )
409	408	a1i	|- ( h = o -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) ) )
410	398	oveq2d	|- ( h = o -> ( ( g ` i ) ( L ` y ) ( h ` i ) ) = ( ( g ` i ) ( L ` y ) ( o ` i ) ) )
411	410	mpteq2dv	|- ( h = o -> ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) )
412	409 411	eqtrd	|- ( h = o -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) )
413	412	fveq2d	|- ( h = o -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) = ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) )
414	413	breq2d	|- ( h = o -> ( ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
415	406 414	imbi12d	|- ( h = o -> ( ( 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_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) ) )
416	415	cbvralvw	|- ( 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. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
417	416	ralbii	|- ( 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. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
418	417	ralbii	|- ( 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. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
419	418	ralbii	|- ( 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. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
420	419	biimpi	|- ( 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. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
421	420	adantl	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
422	421	ad6antr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. o e. ( ( RR ^m y ) ^m NN ) ( X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) C_ U_ i e. NN X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) ) )
423	323	cbvixpv	|- X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) = X_ l e. ( y u. { z } ) ( ( a ` l ) [,) ( b ` l ) )
424	336	cbvixpv	|- X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. ( y u. { z } ) ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) )
425	424	a1i	|- ( j = i -> X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. ( y u. { z } ) ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
426		fveq2	|- ( j = i -> ( c ` j ) = ( c ` i ) )
427	426	fveq1d	|- ( j = i -> ( ( c ` j ) ` l ) = ( ( c ` i ) ` l ) )
428		fveq2	|- ( j = i -> ( d ` j ) = ( d ` i ) )
429	428	fveq1d	|- ( j = i -> ( ( d ` j ) ` l ) = ( ( d ` i ) ` l ) )
430	427 429	oveq12d	|- ( j = i -> ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) = ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
431	430	ixpeq2dv	|- ( j = i -> X_ l e. ( y u. { z } ) ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) = X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
432	425 431	eqtrd	|- ( j = i -> X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
433	432	cbviunv	|- U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ i e. NN X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) )
434	423 433	sseq12i	|- ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ l e. ( y u. { z } ) ( ( a ` l ) [,) ( b ` l ) ) C_ U_ i e. NN X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
435	434	biimpi	|- ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> X_ l e. ( y u. { z } ) ( ( a ` l ) [,) ( b ` l ) ) C_ U_ i e. NN X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
436	435	ad2antlr	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> X_ l e. ( y u. { z } ) ( ( a ` l ) [,) ( b ` l ) ) C_ U_ i e. NN X_ l e. ( y u. { z } ) ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
437		neqne	|- ( -. y = (/) -> y =/= (/) )
438	437	adantl	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> y =/= (/) )
439	307 358 361 364 365 369 373 376 379 422 436 438	hoidmvlelem5	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( i e. NN |-> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) ) ) )
440	273 275	oveq12d	|- ( i = j -> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) = ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) )
441	440	cbvmptv	|- ( i e. NN |-> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) )
442	441	fveq2i	|- ( sum^ ` ( i e. NN |-> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) )
443	442	breq2i	|- ( ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( i e. NN |-> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) ) ) <-> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
444	439 443	sylib	|- ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) /\ -. y = (/) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
445	357 444	pm2.61dan	|- ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) )
446	445	ex	|- ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
447	446	ralrimiva	|- ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
448	447	ralrimiva	|- ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) -> A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
449	448	ralrimiva	|- ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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 e. ( RR ^m ( y u. { z } ) ) ) -> A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
450	449	ralrimiva	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ 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. a e. ( RR ^m ( y u. { z } ) ) A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
451	177 229 450	syl2anc	|- ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) -> A. a e. ( RR ^m ( y u. { z } ) ) A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) )
452	451	ex	|- ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) -> ( A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) -> A. a e. ( RR ^m ( y u. { z } ) ) A. b e. ( RR ^m ( y u. { z } ) ) A. c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) A. d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ( X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. ( y u. { z } ) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` ( y u. { z } ) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) ) ) )
453	51 76 101 126 176 452 2	findcard2d	|- ( ph -> A. a e. ( RR ^m X ) A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
454		fveq1	|- ( a = A -> ( a ` k ) = ( A ` k ) )
455	454	oveq1d	|- ( a = A -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( A ` k ) [,) ( b ` k ) ) )
456	455	ixpeq2dv	|- ( a = A -> X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) )
457	456	sseq1d	|- ( a = A -> ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
458		oveq1	|- ( a = A -> ( a ( L ` X ) b ) = ( A ( L ` X ) b ) )
459	458	breq1d	|- ( a = A -> ( ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) <-> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
460	457 459	imbi12d	|- ( a = A -> ( ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
461	460	ralbidv	|- ( a = A -> ( A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
462	461	ralbidv	|- ( a = A -> ( A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
463	462	ralbidv	|- ( a = A -> ( A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
464	463	rspcva	|- ( ( A e. ( RR ^m X ) /\ A. a e. ( RR ^m X ) A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) -> A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
465	26 453 464	syl2anc	|- ( ph -> A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
466		fveq1	|- ( b = B -> ( b ` k ) = ( B ` k ) )
467	466	oveq2d	|- ( b = B -> ( ( A ` k ) [,) ( b ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
468	467	ixpeq2dv	|- ( b = B -> X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
469	468	sseq1d	|- ( b = B -> ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
470		oveq2	|- ( b = B -> ( A ( L ` X ) b ) = ( A ( L ` X ) B ) )
471	470	breq1d	|- ( b = B -> ( ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) <-> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
472	469 471	imbi12d	|- ( b = B -> ( ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
473	472	ralbidv	|- ( b = B -> ( A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
474	473	ralbidv	|- ( b = B -> ( A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
475	474	rspcva	|- ( ( B e. ( RR ^m X ) /\ A. b e. ( RR ^m X ) A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) -> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
476	23 465 475	syl2anc	|- ( ph -> A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
477		fveq1	|- ( c = C -> ( c ` j ) = ( C ` j ) )
478	477	fveq1d	|- ( c = C -> ( ( c ` j ) ` k ) = ( ( C ` j ) ` k ) )
479	478	oveq1d	|- ( c = C -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
480	479	ixpeq2dv	|- ( c = C -> X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
481	480	adantr	|- ( ( c = C /\ j e. NN ) -> X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
482	481	iuneq2dv	|- ( c = C -> U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
483	482	sseq2d	|- ( c = C -> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
484	477	oveq1d	|- ( c = C -> ( ( c ` j ) ( L ` X ) ( d ` j ) ) = ( ( C ` j ) ( L ` X ) ( d ` j ) ) )
485	484	mpteq2dv	|- ( c = C -> ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) )
486	485	fveq2d	|- ( c = C -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) )
487	486	breq2d	|- ( c = C -> ( ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) <-> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
488	483 487	imbi12d	|- ( c = C -> ( ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
489	488	ralbidv	|- ( c = C -> ( A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) )
490	489	rspcva	|- ( ( C e. ( ( RR ^m X ) ^m NN ) /\ A. c e. ( ( RR ^m X ) ^m NN ) A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) -> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
491	17 476 490	syl2anc	|- ( ph -> A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) )
492		fveq1	|- ( d = D -> ( d ` j ) = ( D ` j ) )
493	492	fveq1d	|- ( d = D -> ( ( d ` j ) ` k ) = ( ( D ` j ) ` k ) )
494	493	oveq2d	|- ( d = D -> ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
495	494	ixpeq2dv	|- ( d = D -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
496	495	adantr	|- ( ( d = D /\ j e. NN ) -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
497	496	iuneq2dv	|- ( d = D -> U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
498	497	sseq2d	|- ( d = D -> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) ) )
499	492	oveq2d	|- ( d = D -> ( ( C ` j ) ( L ` X ) ( d ` j ) ) = ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
500	499	mpteq2dv	|- ( d = D -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) )
501	500	fveq2d	|- ( d = D -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
502	501	breq2d	|- ( d = D -> ( ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) <-> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) ) )
503	498 502	imbi12d	|- ( d = D -> ( ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) <-> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) ) ) )
504	503	rspcva	|- ( ( D e. ( ( RR ^m X ) ^m NN ) /\ A. d e. ( ( RR ^m X ) ^m NN ) ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) ) ) -> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) ) )
505	14 491 504	syl2anc	|- ( ph -> ( X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ U_ j e. NN X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) ) )
506	7 505	mpd	|- ( ph -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )