Metamath Proof Explorer

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 0fin 
 |-  (/) 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 ad5ant12 
 |-  ( ( ( ( ( ( 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 ad5ant12 
 |-  ( ( ( ( ( ( ( ( ( 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 ad5ant12 
 |-  ( ( ( ( ( ( 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 ad5ant12 
 |-  ( ( ( ( ( ( ( ( ( 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 ) ) ) ) )