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 0fi 
 |-  (/) e. Fin
150 149 a1i 
 |-  ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> (/) e. Fin )
151 ovexd 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( RR ^m (/) ) e. _V )
152 9 a1i 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> NN e. _V )
153 simpl 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> c e. ( ( RR ^m (/) ) ^m NN ) )
154 simpr 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> j e. NN )
155 151 152 153 154 fvmap 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( c ` j ) e. ( RR ^m (/) ) )
156 elmapi 
 |-  ( ( c ` j ) e. ( RR ^m (/) ) -> ( c ` j ) : (/) --> RR )
157 155 156 syl 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( c ` j ) : (/) --> RR )
158 157 adantlr 
 |-  ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( c ` j ) : (/) --> RR )
159 ovexd 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( RR ^m (/) ) e. _V )
160 9 a1i 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> NN e. _V )
161 simpl 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> d e. ( ( RR ^m (/) ) ^m NN ) )
162 simpr 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> j e. NN )
163 159 160 161 162 fvmap 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( d ` j ) e. ( RR ^m (/) ) )
164 elmapi 
 |-  ( ( d ` j ) e. ( RR ^m (/) ) -> ( d ` j ) : (/) --> RR )
165 163 164 syl 
 |-  ( ( d e. ( ( RR ^m (/) ) ^m NN ) /\ j e. NN ) -> ( d ` j ) : (/) --> RR )
166 165 adantll 
 |-  ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( d ` j ) : (/) --> RR )
167 1 150 158 166 hoidmvcl 
 |-  ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) e. ( 0 [,) +oo ) )
168 148 167 sselid 
 |-  ( ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) /\ j e. NN ) -> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) e. ( 0 [,] +oo ) )
169 146 147 168 sge0ge0mpt 
 |-  ( ( c e. ( ( RR ^m (/) ) ^m NN ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
170 169 adantll 
 |-  ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> 0 <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
171 145 170 eqbrtrd 
 |-  ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) )
172 171 a1d 
 |-  ( ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) /\ d e. ( ( RR ^m (/) ) ^m NN ) ) -> ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
173 172 ralrimiva 
 |-  ( ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) /\ c e. ( ( RR ^m (/) ) ^m NN ) ) -> A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
174 173 ralrimiva 
 |-  ( ( ( ph /\ a e. ( RR ^m (/) ) ) /\ b e. ( RR ^m (/) ) ) -> A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
175 174 ralrimiva 
 |-  ( ( ph /\ a e. ( RR ^m (/) ) ) -> A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
176 175 ralrimiva 
 |-  ( ph -> A. a e. ( RR ^m (/) ) A. b e. ( RR ^m (/) ) A. c e. ( ( RR ^m (/) ) ^m NN ) A. d e. ( ( RR ^m (/) ) ^m NN ) ( X_ k e. (/) ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. (/) ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` (/) ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` (/) ) ( d ` j ) ) ) ) ) )
177 simpl 
 |-  ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) -> ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) )
178 128 ixpeq2dv 
 |-  ( a = e -> X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) )
179 178 sseq1d 
 |-  ( a = e -> ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
180 oveq1 
 |-  ( a = e -> ( a ( L ` y ) b ) = ( e ( L ` y ) b ) )
181 180 breq1d 
 |-  ( a = e -> ( ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
182 179 181 imbi12d 
 |-  ( a = e -> ( ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
183 182 ralbidv 
 |-  ( a = e -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
184 183 ralbidv 
 |-  ( a = e -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
185 184 ralbidv 
 |-  ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
186 133 ixpeq2dv 
 |-  ( b = f -> X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) = X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) )
187 186 sseq1d 
 |-  ( b = f -> ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
188 oveq2 
 |-  ( b = f -> ( e ( L ` y ) b ) = ( e ( L ` y ) f ) )
189 188 breq1d 
 |-  ( b = f -> ( ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
190 187 189 imbi12d 
 |-  ( b = f -> ( ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
191 190 ralbidv 
 |-  ( b = f -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
192 191 ralbidv 
 |-  ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
193 fveq1 
 |-  ( c = g -> ( c ` j ) = ( g ` j ) )
194 193 fveq1d 
 |-  ( c = g -> ( ( c ` j ) ` k ) = ( ( g ` j ) ` k ) )
195 194 oveq1d 
 |-  ( c = g -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
196 195 ixpeq2dv 
 |-  ( c = g -> X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
197 196 adantr 
 |-  ( ( c = g /\ j e. NN ) -> X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
198 197 iuneq2dv 
 |-  ( c = g -> U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
199 198 sseq2d 
 |-  ( c = g -> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) ) )
200 193 oveq1d 
 |-  ( c = g -> ( ( c ` j ) ( L ` y ) ( d ` j ) ) = ( ( g ` j ) ( L ` y ) ( d ` j ) ) )
201 200 mpteq2dv 
 |-  ( c = g -> ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) = ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) )
202 201 fveq2d 
 |-  ( c = g -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) )
203 202 breq2d 
 |-  ( c = g -> ( ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) )
204 199 203 imbi12d 
 |-  ( c = g -> ( ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
205 204 ralbidv 
 |-  ( c = g -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) ) )
206 fveq1 
 |-  ( d = h -> ( d ` j ) = ( h ` j ) )
207 206 fveq1d 
 |-  ( d = h -> ( ( d ` j ) ` k ) = ( ( h ` j ) ` k ) )
208 207 oveq2d 
 |-  ( d = h -> ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
209 208 ixpeq2dv 
 |-  ( d = h -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
210 209 adantr 
 |-  ( ( d = h /\ j e. NN ) -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
211 210 iuneq2dv 
 |-  ( d = h -> U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) )
212 211 sseq2d 
 |-  ( d = h -> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) <-> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) ) )
213 206 oveq2d 
 |-  ( d = h -> ( ( g ` j ) ( L ` y ) ( d ` j ) ) = ( ( g ` j ) ( L ` y ) ( h ` j ) ) )
214 213 mpteq2dv 
 |-  ( d = h -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) = ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) )
215 214 fveq2d 
 |-  ( d = h -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) )
216 215 breq2d 
 |-  ( d = h -> ( ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) <-> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
217 212 216 imbi12d 
 |-  ( d = h -> ( ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
218 217 cbvralvw 
 |-  ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
219 218 a1i 
 |-  ( c = g -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
220 205 219 bitrd 
 |-  ( c = g -> ( A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
221 220 cbvralvw 
 |-  ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
222 221 a1i 
 |-  ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
223 192 222 bitrd 
 |-  ( b = f -> ( A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
224 223 cbvralvw 
 |-  ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
225 224 a1i 
 |-  ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( e ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
226 185 225 bitrd 
 |-  ( a = e -> ( A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) )
227 226 cbvralvw 
 |-  ( A. a e. ( RR ^m y ) A. b e. ( RR ^m y ) A. c e. ( ( RR ^m y ) ^m NN ) A. d e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( a ` k ) [,) ( b ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) -> ( a ( L ` y ) b ) <_ ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` y ) ( d ` j ) ) ) ) ) <-> A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) )
228 227 bilani 
 |-  ( ( ( 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 ) ) ) ) ) )
229 simplll 
 |-  ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> ph )
230 eldifi 
 |-  ( z e. ( X \ y ) -> z e. X )
231 230 adantl 
 |-  ( ( ph /\ z e. ( X \ y ) ) -> z e. X )
232 231 adantrl 
 |-  ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) -> z e. X )
233 232 ad2antrr 
 |-  ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> z e. X )
234 simpl 
 |-  ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> a e. ( RR ^m ( y u. { z } ) ) )
235 uneq1 
 |-  ( y = (/) -> ( y u. { z } ) = ( (/) u. { z } ) )
236 0un 
 |-  ( (/) u. { z } ) = { z }
237 236 a1i 
 |-  ( y = (/) -> ( (/) u. { z } ) = { z } )
238 235 237 eqtr2d 
 |-  ( y = (/) -> { z } = ( y u. { z } ) )
239 238 eqcomd 
 |-  ( y = (/) -> ( y u. { z } ) = { z } )
240 239 oveq2d 
 |-  ( y = (/) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
241 240 adantl 
 |-  ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
242 234 241 eleqtrd 
 |-  ( ( a e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> a e. ( RR ^m { z } ) )
243 242 adantll 
 |-  ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ y = (/) ) -> a e. ( RR ^m { z } ) )
244 229 233 243 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 } ) ) )
245 244 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 } ) ) )
246 245 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 } ) ) )
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 } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) )
248 simpl 
 |-  ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> b e. ( RR ^m ( y u. { z } ) ) )
249 240 adantl 
 |-  ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> ( RR ^m ( y u. { z } ) ) = ( RR ^m { z } ) )
250 248 249 eleqtrd 
 |-  ( ( b e. ( RR ^m ( y u. { z } ) ) /\ y = (/) ) -> b e. ( RR ^m { z } ) )
251 250 adantlr 
 |-  ( ( ( b e. ( RR ^m ( y u. { z } ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ y = (/) ) -> b e. ( RR ^m { z } ) )
252 251 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 } ) )
253 simpl 
 |-  ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) )
254 240 oveq1d 
 |-  ( y = (/) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
255 254 adantl 
 |-  ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
256 253 255 eleqtrd 
 |-  ( ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> c e. ( ( RR ^m { z } ) ^m NN ) )
257 256 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 ) )
258 247 252 257 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 ) ) )
259 258 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 ) ) )
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 ) ) /\ 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 ) ) )
261 simpl 
 |-  ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) )
262 254 adantl 
 |-  ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> ( ( RR ^m ( y u. { z } ) ) ^m NN ) = ( ( RR ^m { z } ) ^m NN ) )
263 261 262 eleqtrd 
 |-  ( ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) /\ y = (/) ) -> d e. ( ( RR ^m { z } ) ^m NN ) )
264 263 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 ) )
265 264 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 ) )
266 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 ) ) )
267 238 ixpeq1d 
 |-  ( y = (/) -> X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) )
268 267 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 ) ) )
269 238 ixpeq1d 
 |-  ( y = (/) -> X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. ( y u. { z } ) ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) )
270 269 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 ) ) )
271 270 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 ) ) )
272 fveq2 
 |-  ( i = j -> ( c ` i ) = ( c ` j ) )
273 272 fveq1d 
 |-  ( i = j -> ( ( c ` i ) ` k ) = ( ( c ` j ) ` k ) )
274 fveq2 
 |-  ( i = j -> ( d ` i ) = ( d ` j ) )
275 274 fveq1d 
 |-  ( i = j -> ( ( d ` i ) ` k ) = ( ( d ` j ) ` k ) )
276 273 275 oveq12d 
 |-  ( i = j -> ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
277 276 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 ) ) )
278 277 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 ) )
279 278 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 ) ) )
280 271 279 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 ) ) )
281 280 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 ) ) )
282 268 281 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 ) ) ) )
283 266 282 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 ) ) )
284 283 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 ) ) )
285 260 265 284 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 ) ) ) )
286 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 = (/) )
287 fveq1 
 |-  ( a = u -> ( a ` k ) = ( u ` k ) )
288 287 oveq1d 
 |-  ( a = u -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( u ` k ) [,) ( b ` k ) ) )
289 288 fveq2d 
 |-  ( a = u -> ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) )
290 289 prodeq2ad 
 |-  ( a = u -> prod_ k e. x ( vol ` ( ( a ` k ) [,) ( b ` k ) ) ) = prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) )
291 290 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 ) ) ) ) )
292 fveq2 
 |-  ( k = l -> ( u ` k ) = ( u ` l ) )
293 fveq2 
 |-  ( k = l -> ( b ` k ) = ( b ` l ) )
294 292 293 oveq12d 
 |-  ( k = l -> ( ( u ` k ) [,) ( b ` k ) ) = ( ( u ` l ) [,) ( b ` l ) ) )
295 294 fveq2d 
 |-  ( k = l -> ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) )
296 295 cbvprodv 
 |-  prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) )
297 296 a1i 
 |-  ( b = v -> prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) )
298 fveq1 
 |-  ( b = v -> ( b ` l ) = ( v ` l ) )
299 298 oveq2d 
 |-  ( b = v -> ( ( u ` l ) [,) ( b ` l ) ) = ( ( u ` l ) [,) ( v ` l ) ) )
300 299 fveq2d 
 |-  ( b = v -> ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) = ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
301 300 prodeq2ad 
 |-  ( b = v -> prod_ l e. x ( vol ` ( ( u ` l ) [,) ( b ` l ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
302 297 301 eqtrd 
 |-  ( b = v -> prod_ k e. x ( vol ` ( ( u ` k ) [,) ( b ` k ) ) ) = prod_ l e. x ( vol ` ( ( u ` l ) [,) ( v ` l ) ) ) )
303 302 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 ) ) ) ) )
304 291 303 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 ) ) ) ) )
305 304 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 ) ) ) ) ) )
306 1 305 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 ) ) ) ) ) )
307 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 )
308 eqid 
 |-  { z } = { z }
309 elmapi 
 |-  ( a e. ( RR ^m { z } ) -> a : { z } --> RR )
310 309 ad2antlr 
 |-  ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) -> a : { z } --> RR )
311 310 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 )
312 elmapi 
 |-  ( b e. ( RR ^m { z } ) -> b : { z } --> RR )
313 312 adantl 
 |-  ( ( ( ( ph /\ z e. X ) /\ a e. ( RR ^m { z } ) ) /\ b e. ( RR ^m { z } ) ) -> b : { z } --> RR )
314 313 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 )
315 elmapi 
 |-  ( c e. ( ( RR ^m { z } ) ^m NN ) -> c : NN --> ( RR ^m { z } ) )
316 315 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 } ) )
317 316 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 } ) )
318 elmapi 
 |-  ( d e. ( ( RR ^m { z } ) ^m NN ) -> d : NN --> ( RR ^m { z } ) )
319 318 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 } ) )
320 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 ) ) )
321 fveq2 
 |-  ( k = l -> ( a ` k ) = ( a ` l ) )
322 321 293 oveq12d 
 |-  ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) )
323 eqcom 
 |-  ( k = l <-> l = k )
324 323 imbi1i 
 |-  ( ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) )
325 eqcom 
 |-  ( ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) <-> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) )
326 325 imbi2i 
 |-  ( ( l = k -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) ) )
327 324 326 bitri 
 |-  ( ( k = l -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( a ` l ) [,) ( b ` l ) ) ) <-> ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) ) )
328 322 327 mpbi 
 |-  ( l = k -> ( ( a ` l ) [,) ( b ` l ) ) = ( ( a ` k ) [,) ( b ` k ) ) )
329 328 cbvixpv 
 |-  X_ l e. { z } ( ( a ` l ) [,) ( b ` l ) ) = X_ k e. { z } ( ( a ` k ) [,) ( b ` k ) )
330 329 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 ) ) )
331 276 ixpeq2dv 
 |-  ( i = j -> X_ k e. { z } ( ( ( c ` i ) ` k ) [,) ( ( d ` i ) ` k ) ) = X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
332 331 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 ) )
333 fveq2 
 |-  ( k = l -> ( ( c ` j ) ` k ) = ( ( c ` j ) ` l ) )
334 fveq2 
 |-  ( k = l -> ( ( d ` j ) ` k ) = ( ( d ` j ) ` l ) )
335 333 334 oveq12d 
 |-  ( k = l -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
336 335 cbvixpv 
 |-  X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) )
337 336 a1i 
 |-  ( j e. NN -> X_ k e. { z } ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ l e. { z } ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) )
338 337 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 ) )
339 332 338 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 ) )
340 339 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 ) ) )
341 330 340 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 ) ) ) )
342 320 341 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 ) ) )
343 342 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 ) ) )
344 306 307 308 311 314 317 319 343 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 ) ) ) ) )
345 344 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 ) ) ) ) )
346 235 237 eqtrd 
 |-  ( y = (/) -> ( y u. { z } ) = { z } )
347 346 fveq2d 
 |-  ( y = (/) -> ( L ` ( y u. { z } ) ) = ( L ` { z } ) )
348 347 oveqd 
 |-  ( y = (/) -> ( a ( L ` ( y u. { z } ) ) b ) = ( a ( L ` { z } ) b ) )
349 348 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 ) )
350 347 oveqd 
 |-  ( y = (/) -> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) = ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) )
351 350 mpteq2dv 
 |-  ( y = (/) -> ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) )
352 351 fveq2d 
 |-  ( y = (/) -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` { z } ) ( d ` j ) ) ) ) )
353 352 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 ) ) ) ) )
354 349 353 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 ) ) ) ) ) )
355 345 354 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 ) ) ) ) )
356 285 286 355 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 ) ) ) ) )
357 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 )
358 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 )
359 358 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> y C_ X )
360 359 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ 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 )
361 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 ) )
362 361 ad3antrrr 
 |-  ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) -> z e. ( X \ y ) )
363 362 ad3antrrr 
 |-  ( ( ( ( ( ( ( ( ( ph /\ ( y C_ X /\ z e. ( X \ y ) ) ) /\ A. e e. ( RR ^m y ) A. f e. ( RR ^m y ) A. g e. ( ( RR ^m y ) ^m NN ) A. h e. ( ( RR ^m y ) ^m NN ) ( X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) C_ U_ j e. NN X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) -> ( e ( L ` y ) f ) <_ ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) ) ) /\ a e. ( RR ^m ( y u. { z } ) ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) /\ c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) ) /\ 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 ) )
364 eqid 
 |-  ( y u. { z } ) = ( y u. { z } )
365 elmapi 
 |-  ( a e. ( RR ^m ( y u. { z } ) ) -> a : ( y u. { z } ) --> RR )
366 365 adantr 
 |-  ( ( a e. ( RR ^m ( y u. { z } ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) -> a : ( y u. { z } ) --> RR )
367 366 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 )
368 367 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 )
369 elmapi 
 |-  ( b e. ( RR ^m ( y u. { z } ) ) -> b : ( y u. { z } ) --> RR )
370 369 adantl 
 |-  ( ( a e. ( RR ^m ( y u. { z } ) ) /\ b e. ( RR ^m ( y u. { z } ) ) ) -> b : ( y u. { z } ) --> RR )
371 370 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 )
372 371 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 )
373 elmapi 
 |-  ( c e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> c : NN --> ( RR ^m ( y u. { z } ) ) )
374 373 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 } ) ) )
375 374 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 } ) ) )
376 elmapi 
 |-  ( d e. ( ( RR ^m ( y u. { z } ) ) ^m NN ) -> d : NN --> ( RR ^m ( y u. { z } ) ) )
377 376 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 } ) ) )
378 377 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 } ) ) )
379 fveq2 
 |-  ( k = l -> ( e ` k ) = ( e ` l ) )
380 fveq2 
 |-  ( k = l -> ( f ` k ) = ( f ` l ) )
381 379 380 oveq12d 
 |-  ( k = l -> ( ( e ` k ) [,) ( f ` k ) ) = ( ( e ` l ) [,) ( f ` l ) ) )
382 381 cbvixpv 
 |-  X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) = X_ l e. y ( ( e ` l ) [,) ( f ` l ) )
383 382 a1i 
 |-  ( h = o -> X_ k e. y ( ( e ` k ) [,) ( f ` k ) ) = X_ l e. y ( ( e ` l ) [,) ( f ` l ) ) )
384 fveq2 
 |-  ( j = i -> ( g ` j ) = ( g ` i ) )
385 384 fveq1d 
 |-  ( j = i -> ( ( g ` j ) ` k ) = ( ( g ` i ) ` k ) )
386 fveq2 
 |-  ( j = i -> ( h ` j ) = ( h ` i ) )
387 386 fveq1d 
 |-  ( j = i -> ( ( h ` j ) ` k ) = ( ( h ` i ) ` k ) )
388 385 387 oveq12d 
 |-  ( j = i -> ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) )
389 388 ixpeq2dv 
 |-  ( j = i -> X_ k e. y ( ( ( g ` j ) ` k ) [,) ( ( h ` j ) ` k ) ) = X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) )
390 389 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 ) )
391 390 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 ) ) )
392 fveq2 
 |-  ( k = l -> ( ( g ` i ) ` k ) = ( ( g ` i ) ` l ) )
393 fveq2 
 |-  ( k = l -> ( ( h ` i ) ` k ) = ( ( h ` i ) ` l ) )
394 392 393 oveq12d 
 |-  ( k = l -> ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) )
395 394 cbvixpv 
 |-  X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) )
396 395 a1i 
 |-  ( h = o -> X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) )
397 fveq1 
 |-  ( h = o -> ( h ` i ) = ( o ` i ) )
398 397 fveq1d 
 |-  ( h = o -> ( ( h ` i ) ` l ) = ( ( o ` i ) ` l ) )
399 398 oveq2d 
 |-  ( h = o -> ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) = ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
400 399 ixpeq2dv 
 |-  ( h = o -> X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( h ` i ) ` l ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
401 396 400 eqtrd 
 |-  ( h = o -> X_ k e. y ( ( ( g ` i ) ` k ) [,) ( ( h ` i ) ` k ) ) = X_ l e. y ( ( ( g ` i ) ` l ) [,) ( ( o ` i ) ` l ) ) )
402 401 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 ) ) )
403 402 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 ) ) )
404 391 403 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 ) ) )
405 383 404 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 ) ) ) )
406 384 386 oveq12d 
 |-  ( j = i -> ( ( g ` j ) ( L ` y ) ( h ` j ) ) = ( ( g ` i ) ( L ` y ) ( h ` i ) ) )
407 406 cbvmptv 
 |-  ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) )
408 407 a1i 
 |-  ( h = o -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) ) )
409 397 oveq2d 
 |-  ( h = o -> ( ( g ` i ) ( L ` y ) ( h ` i ) ) = ( ( g ` i ) ( L ` y ) ( o ` i ) ) )
410 409 mpteq2dv 
 |-  ( h = o -> ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( h ` i ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) )
411 408 410 eqtrd 
 |-  ( h = o -> ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) = ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) )
412 411 fveq2d 
 |-  ( h = o -> ( sum^ ` ( j e. NN |-> ( ( g ` j ) ( L ` y ) ( h ` j ) ) ) ) = ( sum^ ` ( i e. NN |-> ( ( g ` i ) ( L ` y ) ( o ` i ) ) ) ) )
413 412 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 ) ) ) ) ) )
414 405 413 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 ) ) ) ) ) ) )
415 414 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 ) ) ) ) ) )
416 415 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 ) ) ) ) ) )
417 416 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 ) ) ) ) ) )
418 417 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 ) ) ) ) ) )
419 418 bilani 
 |-  ( ( ( 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 ) ) ) ) ) )
420 419 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 ) ) ) ) ) )
421 322 cbvixpv 
 |-  X_ k e. ( y u. { z } ) ( ( a ` k ) [,) ( b ` k ) ) = X_ l e. ( y u. { z } ) ( ( a ` l ) [,) ( b ` l ) )
422 335 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 ) )
423 422 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 ) ) )
424 fveq2 
 |-  ( j = i -> ( c ` j ) = ( c ` i ) )
425 424 fveq1d 
 |-  ( j = i -> ( ( c ` j ) ` l ) = ( ( c ` i ) ` l ) )
426 fveq2 
 |-  ( j = i -> ( d ` j ) = ( d ` i ) )
427 426 fveq1d 
 |-  ( j = i -> ( ( d ` j ) ` l ) = ( ( d ` i ) ` l ) )
428 425 427 oveq12d 
 |-  ( j = i -> ( ( ( c ` j ) ` l ) [,) ( ( d ` j ) ` l ) ) = ( ( ( c ` i ) ` l ) [,) ( ( d ` i ) ` l ) ) )
429 428 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 ) ) )
430 423 429 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 ) ) )
431 430 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 ) )
432 421 431 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 ) ) )
433 432 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 ) ) )
434 433 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 ) ) )
435 neqne 
 |-  ( -. y = (/) -> y =/= (/) )
436 435 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 =/= (/) )
437 306 357 360 363 364 368 372 375 378 420 434 436 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 ) ) ) ) )
438 272 274 oveq12d 
 |-  ( i = j -> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) = ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) )
439 438 cbvmptv 
 |-  ( i e. NN |-> ( ( c ` i ) ( L ` ( y u. { z } ) ) ( d ` i ) ) ) = ( j e. NN |-> ( ( c ` j ) ( L ` ( y u. { z } ) ) ( d ` j ) ) )
440 439 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 ) ) ) )
441 440 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 ) ) ) ) )
442 437 441 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 ) ) ) ) )
443 356 442 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 ) ) ) ) )
444 443 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 ) ) ) ) ) )
445 444 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 ) ) ) ) ) )
446 445 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 ) ) ) ) ) )
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 } ) ) ) -> 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 ) ) ) ) ) )
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. 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 ) ) ) ) ) )
449 177 228 448 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 ) ) ) ) ) )
450 449 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 ) ) ) ) ) ) )
451 51 76 101 126 176 450 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 ) ) ) ) ) )
452 fveq1 
 |-  ( a = A -> ( a ` k ) = ( A ` k ) )
453 452 oveq1d 
 |-  ( a = A -> ( ( a ` k ) [,) ( b ` k ) ) = ( ( A ` k ) [,) ( b ` k ) ) )
454 453 ixpeq2dv 
 |-  ( a = A -> X_ k e. X ( ( a ` k ) [,) ( b ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) )
455 454 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 ) ) ) )
456 oveq1 
 |-  ( a = A -> ( a ( L ` X ) b ) = ( A ( L ` X ) b ) )
457 456 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 ) ) ) ) ) )
458 455 457 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 ) ) ) ) ) ) )
459 458 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 ) ) ) ) ) ) )
460 459 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 ) ) ) ) ) ) )
461 460 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 ) ) ) ) ) ) )
462 461 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 ) ) ) ) ) )
463 26 451 462 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 ) ) ) ) ) )
464 fveq1 
 |-  ( b = B -> ( b ` k ) = ( B ` k ) )
465 464 oveq2d 
 |-  ( b = B -> ( ( A ` k ) [,) ( b ` k ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
466 465 ixpeq2dv 
 |-  ( b = B -> X_ k e. X ( ( A ` k ) [,) ( b ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
467 466 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 ) ) ) )
468 oveq2 
 |-  ( b = B -> ( A ( L ` X ) b ) = ( A ( L ` X ) B ) )
469 468 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 ) ) ) ) ) )
470 467 469 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 ) ) ) ) ) ) )
471 470 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 ) ) ) ) ) ) )
472 471 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 ) ) ) ) ) ) )
473 472 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 ) ) ) ) ) )
474 23 463 473 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 ) ) ) ) ) )
475 fveq1 
 |-  ( c = C -> ( c ` j ) = ( C ` j ) )
476 475 fveq1d 
 |-  ( c = C -> ( ( c ` j ) ` k ) = ( ( C ` j ) ` k ) )
477 476 oveq1d 
 |-  ( c = C -> ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
478 477 ixpeq2dv 
 |-  ( c = C -> X_ k e. X ( ( ( c ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) )
479 478 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 ) ) )
480 479 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 ) ) )
481 480 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 ) ) ) )
482 475 oveq1d 
 |-  ( c = C -> ( ( c ` j ) ( L ` X ) ( d ` j ) ) = ( ( C ` j ) ( L ` X ) ( d ` j ) ) )
483 482 mpteq2dv 
 |-  ( c = C -> ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) )
484 483 fveq2d 
 |-  ( c = C -> ( sum^ ` ( j e. NN |-> ( ( c ` j ) ( L ` X ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) )
485 484 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 ) ) ) ) ) )
486 481 485 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 ) ) ) ) ) ) )
487 486 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 ) ) ) ) ) ) )
488 487 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 ) ) ) ) ) )
489 17 474 488 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 ) ) ) ) ) )
490 fveq1 
 |-  ( d = D -> ( d ` j ) = ( D ` j ) )
491 490 fveq1d 
 |-  ( d = D -> ( ( d ` j ) ` k ) = ( ( D ` j ) ` k ) )
492 491 oveq2d 
 |-  ( d = D -> ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
493 492 ixpeq2dv 
 |-  ( d = D -> X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( d ` j ) ` k ) ) = X_ k e. X ( ( ( C ` j ) ` k ) [,) ( ( D ` j ) ` k ) ) )
494 493 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 ) ) )
495 494 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 ) ) )
496 495 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 ) ) ) )
497 490 oveq2d 
 |-  ( d = D -> ( ( C ` j ) ( L ` X ) ( d ` j ) ) = ( ( C ` j ) ( L ` X ) ( D ` j ) ) )
498 497 mpteq2dv 
 |-  ( d = D -> ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) = ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) )
499 498 fveq2d 
 |-  ( d = D -> ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( d ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )
500 499 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 ) ) ) ) ) )
501 496 500 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 ) ) ) ) ) ) )
502 501 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 ) ) ) ) ) )
503 14 489 502 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 ) ) ) ) ) )
504 7 503 mpd 
 |-  ( ph -> ( A ( L ` X ) B ) <_ ( sum^ ` ( j e. NN |-> ( ( C ` j ) ( L ` X ) ( D ` j ) ) ) ) )