Metamath Proof Explorer

Theorem ovncvr2

Description: B and T are the left and right side of a cover of A . This cover is made of n-dimensional half-open intervals and approximates the n-dimensional Lebesgue outer volume of A . (Contributed by Glauco Siliprandi, 24-Dec-2020)

Ref Expression
Hypotheses ovncvr2.x 
|- ( ph -> X e. Fin )
ovncvr2.a 
|- ( ph -> A C_ ( RR ^m X ) )
ovncvr2.e 
|- ( ph -> E e. RR+ )
ovncvr2.c 
|- C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
ovncvr2.l 
|- L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
ovncvr2.d 
|- D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
ovncvr2.i 
|- ( ph -> I e. ( ( D ` A ) ` E ) )
ovncvr2.b 
|- B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )
ovncvr2.t 
|- T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )
Assertion ovncvr2 
|- ( ph -> ( ( ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) /\ A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) /\ ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )

Proof

Step Hyp Ref Expression
1 ovncvr2.x 
 |-  ( ph -> X e. Fin )
2 ovncvr2.a 
 |-  ( ph -> A C_ ( RR ^m X ) )
3 ovncvr2.e 
 |-  ( ph -> E e. RR+ )
4 ovncvr2.c 
 |-  C = ( a e. ~P ( RR ^m X ) |-> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
5 ovncvr2.l 
 |-  L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) )
6 ovncvr2.d 
 |-  D = ( a e. ~P ( RR ^m X ) |-> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) )
7 ovncvr2.i 
 |-  ( ph -> I e. ( ( D ` A ) ` E ) )
8 ovncvr2.b 
 |-  B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )
9 ovncvr2.t 
 |-  T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )
10 sseq1 
 |-  ( a = A -> ( a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) ) )
11 10 rabbidv 
 |-  ( a = A -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | a C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
12 ovexd 
 |-  ( ph -> ( RR ^m X ) e. _V )
13 12 2 ssexd 
 |-  ( ph -> A e. _V )
14 elpwg 
 |-  ( A e. _V -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
15 13 14 syl 
 |-  ( ph -> ( A e. ~P ( RR ^m X ) <-> A C_ ( RR ^m X ) ) )
16 2 15 mpbird 
 |-  ( ph -> A e. ~P ( RR ^m X ) )
17 ovex 
 |-  ( ( ( RR X. RR ) ^m X ) ^m NN ) e. _V
18 17 rabex 
 |-  { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V
19 18 a1i 
 |-  ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } e. _V )
20 4 11 16 19 fvmptd3 
 |-  ( ph -> ( C ` A ) = { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
21 ssrab2 
 |-  { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN )
22 21 a1i 
 |-  ( ph -> { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
23 20 22 eqsstrd 
 |-  ( ph -> ( C ` A ) C_ ( ( ( RR X. RR ) ^m X ) ^m NN ) )
24 fveq2 
 |-  ( a = A -> ( C ` a ) = ( C ` A ) )
25 24 eleq2d 
 |-  ( a = A -> ( i e. ( C ` a ) <-> i e. ( C ` A ) ) )
26 fveq2 
 |-  ( a = A -> ( ( voln* ` X ) ` a ) = ( ( voln* ` X ) ` A ) )
27 26 oveq1d 
 |-  ( a = A -> ( ( ( voln* ` X ) ` a ) +e r ) = ( ( ( voln* ` X ) ` A ) +e r ) )
28 27 breq2d 
 |-  ( a = A -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) ) )
29 25 28 anbi12d 
 |-  ( a = A -> ( ( i e. ( C ` a ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) ) <-> ( i e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) ) ) )
30 29 rabbidva2 
 |-  ( a = A -> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } )
31 30 mpteq2dv 
 |-  ( a = A -> ( r e. RR+ |-> { i e. ( C ` a ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` a ) +e r ) } ) = ( r e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } ) )
32 rpex 
 |-  RR+ e. _V
33 32 mptex 
 |-  ( r e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } ) e. _V
34 33 a1i 
 |-  ( ph -> ( r e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } ) e. _V )
35 6 31 16 34 fvmptd3 
 |-  ( ph -> ( D ` A ) = ( r e. RR+ |-> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } ) )
36 oveq2 
 |-  ( r = E -> ( ( ( voln* ` X ) ` A ) +e r ) = ( ( ( voln* ` X ) ` A ) +e E ) )
37 36 breq2d 
 |-  ( r = E -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
38 37 rabbidv 
 |-  ( r = E -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
39 38 adantl 
 |-  ( ( ph /\ r = E ) -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e r ) } = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
40 fvex 
 |-  ( C ` A ) e. _V
41 40 rabex 
 |-  { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V
42 41 a1i 
 |-  ( ph -> { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } e. _V )
43 35 39 3 42 fvmptd 
 |-  ( ph -> ( ( D ` A ) ` E ) = { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
44 7 43 eleqtrd 
 |-  ( ph -> I e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } )
45 fveq1 
 |-  ( i = I -> ( i ` j ) = ( I ` j ) )
46 45 fveq2d 
 |-  ( i = I -> ( L ` ( i ` j ) ) = ( L ` ( I ` j ) ) )
47 46 mpteq2dv 
 |-  ( i = I -> ( j e. NN |-> ( L ` ( i ` j ) ) ) = ( j e. NN |-> ( L ` ( I ` j ) ) ) )
48 47 fveq2d 
 |-  ( i = I -> ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) = ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) )
49 48 breq1d 
 |-  ( i = I -> ( ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) <-> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
50 49 elrab 
 |-  ( I e. { i e. ( C ` A ) | ( sum^ ` ( j e. NN |-> ( L ` ( i ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) } <-> ( I e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
51 44 50 sylib 
 |-  ( ph -> ( I e. ( C ` A ) /\ ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )
52 51 simpld 
 |-  ( ph -> I e. ( C ` A ) )
53 23 52 sseldd 
 |-  ( ph -> I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
54 elmapi 
 |-  ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) -> I : NN --> ( ( RR X. RR ) ^m X ) )
55 53 54 syl 
 |-  ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )
56 55 adantr 
 |-  ( ( ph /\ j e. NN ) -> I : NN --> ( ( RR X. RR ) ^m X ) )
57 simpr 
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
58 56 57 ffvelcdmd 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) e. ( ( RR X. RR ) ^m X ) )
59 elmapi 
 |-  ( ( I ` j ) e. ( ( RR X. RR ) ^m X ) -> ( I ` j ) : X --> ( RR X. RR ) )
60 58 59 syl 
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
61 60 ffvelcdmda 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( I ` j ) ` k ) e. ( RR X. RR ) )
62 xp1st 
 |-  ( ( ( I ` j ) ` k ) e. ( RR X. RR ) -> ( 1st ` ( ( I ` j ) ` k ) ) e. RR )
63 61 62 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) e. RR )
64 63 fmpttd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) : X --> RR )
65 reex 
 |-  RR e. _V
66 65 a1i 
 |-  ( ph -> RR e. _V )
67 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
68 66 1 67 syl2anc 
 |-  ( ph -> ( ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
69 68 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
70 64 69 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) )
71 70 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) ) : NN --> ( RR ^m X ) )
72 8 a1i 
 |-  ( ph -> B = ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) ) )
73 72 feq1d 
 |-  ( ph -> ( B : NN --> ( RR ^m X ) <-> ( j e. NN |-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) ) : NN --> ( RR ^m X ) ) )
74 71 73 mpbird 
 |-  ( ph -> B : NN --> ( RR ^m X ) )
75 xp2nd 
 |-  ( ( ( I ` j ) ` k ) e. ( RR X. RR ) -> ( 2nd ` ( ( I ` j ) ` k ) ) e. RR )
76 61 75 syl 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) e. RR )
77 76 fmpttd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) : X --> RR )
78 elmapg 
 |-  ( ( RR e. _V /\ X e. Fin ) -> ( ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
79 66 1 78 syl2anc 
 |-  ( ph -> ( ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
80 79 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) <-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
81 77 80 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. ( RR ^m X ) )
82 81 fmpttd 
 |-  ( ph -> ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) ) : NN --> ( RR ^m X ) )
83 9 a1i 
 |-  ( ph -> T = ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) ) )
84 83 feq1d 
 |-  ( ph -> ( T : NN --> ( RR ^m X ) <-> ( j e. NN |-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) ) : NN --> ( RR ^m X ) ) )
85 82 84 mpbird 
 |-  ( ph -> T : NN --> ( RR ^m X ) )
86 74 85 jca 
 |-  ( ph -> ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) )
87 52 20 eleqtrd 
 |-  ( ph -> I e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } )
88 fveq1 
 |-  ( l = I -> ( l ` j ) = ( I ` j ) )
89 88 coeq2d 
 |-  ( l = I -> ( [,) o. ( l ` j ) ) = ( [,) o. ( I ` j ) ) )
90 89 fveq1d 
 |-  ( l = I -> ( ( [,) o. ( l ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
91 90 ixpeq2dv 
 |-  ( l = I -> X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
92 91 adantr 
 |-  ( ( l = I /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
93 92 iuneq2dv 
 |-  ( l = I -> U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
94 93 sseq2d 
 |-  ( l = I -> ( A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) <-> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) ) )
95 94 elrab 
 |-  ( I e. { l e. ( ( ( RR X. RR ) ^m X ) ^m NN ) | A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( l ` j ) ) ` k ) } <-> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) ) )
96 87 95 sylib 
 |-  ( ph -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) ) )
97 96 simprd 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) )
98 60 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( I ` j ) : X --> ( RR X. RR ) )
99 simpr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> k e. X )
100 98 99 fvovco 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) )
101 mptexg 
 |-  ( X e. Fin -> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. _V )
102 1 101 syl 
 |-  ( ph -> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. _V )
103 102 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. _V )
104 72 103 fvmpt2d 
 |-  ( ( ph /\ j e. NN ) -> ( B ` j ) = ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )
105 fvexd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) e. _V )
106 104 105 fvmpt2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( B ` j ) ` k ) = ( 1st ` ( ( I ` j ) ` k ) ) )
107 106 eqcomd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) = ( ( B ` j ) ` k ) )
108 mptexg 
 |-  ( X e. Fin -> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. _V )
109 1 108 syl 
 |-  ( ph -> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. _V )
110 109 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. _V )
111 83 110 fvmpt2d 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) = ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )
112 fvexd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) e. _V )
113 111 112 fvmpt2d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( T ` j ) ` k ) = ( 2nd ` ( ( I ` j ) ` k ) ) )
114 113 eqcomd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) = ( ( T ` j ) ` k ) )
115 107 114 oveq12d 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) = ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
116 100 115 eqtrd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
117 116 ixpeq2dva 
 |-  ( ( ph /\ j e. NN ) -> X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) = X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
118 117 iuneq2dv 
 |-  ( ph -> U_ j e. NN X_ k e. X ( ( [,) o. ( I ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
119 97 118 sseqtrd 
 |-  ( ph -> A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
120 5 a1i 
 |-  ( ( ph /\ j e. NN ) -> L = ( h e. ( ( RR X. RR ) ^m X ) |-> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) ) )
121 coeq2 
 |-  ( h = ( I ` j ) -> ( [,) o. h ) = ( [,) o. ( I ` j ) ) )
122 121 fveq1d 
 |-  ( h = ( I ` j ) -> ( ( [,) o. h ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
123 122 ad2antlr 
 |-  ( ( ( ph /\ h = ( I ` j ) ) /\ k e. X ) -> ( ( [,) o. h ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
124 123 adantllr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) /\ k e. X ) -> ( ( [,) o. h ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
125 100 adantlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) )
126 115 adantlr 
 |-  ( ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) /\ k e. X ) -> ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) = ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
127 124 125 126 3eqtrd 
 |-  ( ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) /\ k e. X ) -> ( ( [,) o. h ) ` k ) = ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) )
128 127 fveq2d 
 |-  ( ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) /\ k e. X ) -> ( vol ` ( ( [,) o. h ) ` k ) ) = ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) )
129 128 prodeq2dv 
 |-  ( ( ( ph /\ j e. NN ) /\ h = ( I ` j ) ) -> prod_ k e. X ( vol ` ( ( [,) o. h ) ` k ) ) = prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) )
130 1 adantr 
 |-  ( ( ph /\ j e. NN ) -> X e. Fin )
131 8 fvmpt2 
 |-  ( ( j e. NN /\ ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) e. _V ) -> ( B ` j ) = ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )
132 57 103 131 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( B ` j ) = ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) )
133 132 feq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( B ` j ) : X --> RR <-> ( k e. X |-> ( 1st ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
134 64 133 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( B ` j ) : X --> RR )
135 134 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( B ` j ) : X --> RR )
136 135 99 ffvelcdmd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( B ` j ) ` k ) e. RR )
137 9 fvmpt2 
 |-  ( ( j e. NN /\ ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) e. _V ) -> ( T ` j ) = ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )
138 57 110 137 syl2anc 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) = ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) )
139 138 feq1d 
 |-  ( ( ph /\ j e. NN ) -> ( ( T ` j ) : X --> RR <-> ( k e. X |-> ( 2nd ` ( ( I ` j ) ` k ) ) ) : X --> RR ) )
140 77 139 mpbird 
 |-  ( ( ph /\ j e. NN ) -> ( T ` j ) : X --> RR )
141 140 adantr 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( T ` j ) : X --> RR )
142 141 99 ffvelcdmd 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( T ` j ) ` k ) e. RR )
143 volicore 
 |-  ( ( ( ( B ` j ) ` k ) e. RR /\ ( ( T ` j ) ` k ) e. RR ) -> ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) e. RR )
144 136 142 143 syl2anc 
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) e. RR )
145 130 144 fprodrecl 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) e. RR )
146 120 129 58 145 fvmptd 
 |-  ( ( ph /\ j e. NN ) -> ( L ` ( I ` j ) ) = prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) )
147 146 eqcomd 
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) = ( L ` ( I ` j ) ) )
148 147 mpteq2dva 
 |-  ( ph -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) = ( j e. NN |-> ( L ` ( I ` j ) ) ) )
149 148 fveq2d 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) = ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) )
150 51 simprd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> ( L ` ( I ` j ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
151 149 150 eqbrtrd 
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) )
152 86 119 151 jca31 
 |-  ( ph -> ( ( ( B : NN --> ( RR ^m X ) /\ T : NN --> ( RR ^m X ) ) /\ A C_ U_ j e. NN X_ k e. X ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) /\ ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( ( B ` j ) ` k ) [,) ( ( T ` j ) ` k ) ) ) ) ) <_ ( ( ( voln* ` X ) ` A ) +e E ) ) )