Metamath Proof Explorer

Theorem ovnhoilem1

Description: The Lebesgue outer measure of a multidimensional half-open interval is less than or equal to the product of its length in each dimension. First part of the proof of Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoilem1.x 
|- ( ph -> X e. Fin )
ovnhoilem1.a 
|- ( ph -> A : X --> RR )
ovnhoilem1.b 
|- ( ph -> B : X --> RR )
ovnhoilem1.c 
|- I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
ovnhoilem1.m 
|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
ovnhoilem1.h 
|- H = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
Assertion ovnhoilem1 
|- ( ph -> ( ( voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )

Proof

Step Hyp Ref Expression
1 ovnhoilem1.x 
 |-  ( ph -> X e. Fin )
2 ovnhoilem1.a 
 |-  ( ph -> A : X --> RR )
3 ovnhoilem1.b 
 |-  ( ph -> B : X --> RR )
4 ovnhoilem1.c 
 |-  I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) )
5 ovnhoilem1.m 
 |-  M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) }
6 ovnhoilem1.h 
 |-  H = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
7 4 a1i 
 |-  ( ph -> I = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
8 nfv 
 |-  F/ k ph
9 2 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( A ` k ) e. RR )
10 3 ffvelrnda 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR )
11 10 rexrd 
 |-  ( ( ph /\ k e. X ) -> ( B ` k ) e. RR* )
12 8 9 11 hoissrrn2 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) C_ ( RR ^m X ) )
13 7 12 eqsstrd 
 |-  ( ph -> I C_ ( RR ^m X ) )
14 1 13 5 ovnval2 
 |-  ( ph -> ( ( voln* ` X ) ` I ) = if ( X = (/) , 0 , inf ( M , RR* , < ) ) )
15 iftrue 
 |-  ( X = (/) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) = 0 )
16 15 adantl 
 |-  ( ( ph /\ X = (/) ) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) = 0 )
17 0xr 
 |-  0 e. RR*
18 17 a1i 
 |-  ( ph -> 0 e. RR* )
19 pnfxr 
 |-  +oo e. RR*
20 19 a1i 
 |-  ( ph -> +oo e. RR* )
21 8 1 9 10 hoiprodcl3 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. ( 0 [,) +oo ) )
22 icogelb 
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. ( 0 [,) +oo ) ) -> 0 <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
23 18 20 21 22 syl3anc 
 |-  ( ph -> 0 <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
24 23 adantr 
 |-  ( ( ph /\ X = (/) ) -> 0 <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
25 16 24 eqbrtrd 
 |-  ( ( ph /\ X = (/) ) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
26 iffalse 
 |-  ( -. X = (/) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) = inf ( M , RR* , < ) )
27 26 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) = inf ( M , RR* , < ) )
28 ssrab2 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } C_ RR*
29 5 28 eqsstri 
 |-  M C_ RR*
30 29 a1i 
 |-  ( ( ph /\ -. X = (/) ) -> M C_ RR* )
31 icossxr 
 |-  ( 0 [,) +oo ) C_ RR*
32 31 21 sseldi 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR* )
33 32 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR* )
34 opelxpi 
 |-  ( ( ( A ` k ) e. RR /\ ( B ` k ) e. RR ) -> <. ( A ` k ) , ( B ` k ) >. e. ( RR X. RR ) )
35 9 10 34 syl2anc 
 |-  ( ( ph /\ k e. X ) -> <. ( A ` k ) , ( B ` k ) >. e. ( RR X. RR ) )
36 0re 
 |-  0 e. RR
37 opelxpi 
 |-  ( ( 0 e. RR /\ 0 e. RR ) -> <. 0 , 0 >. e. ( RR X. RR ) )
38 36 36 37 mp2an 
 |-  <. 0 , 0 >. e. ( RR X. RR )
39 38 a1i 
 |-  ( ( ph /\ k e. X ) -> <. 0 , 0 >. e. ( RR X. RR ) )
40 35 39 ifcld 
 |-  ( ( ph /\ k e. X ) -> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) e. ( RR X. RR ) )
41 40 fmpttd 
 |-  ( ph -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) : X --> ( RR X. RR ) )
42 reex 
 |-  RR e. _V
43 42 42 xpex 
 |-  ( RR X. RR ) e. _V
44 1 43 jctil 
 |-  ( ph -> ( ( RR X. RR ) e. _V /\ X e. Fin ) )
45 elmapg 
 |-  ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) : X --> ( RR X. RR ) ) )
46 44 45 syl 
 |-  ( ph -> ( ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) e. ( ( RR X. RR ) ^m X ) <-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) : X --> ( RR X. RR ) ) )
47 41 46 mpbird 
 |-  ( ph -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) e. ( ( RR X. RR ) ^m X ) )
48 47 adantr 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) e. ( ( RR X. RR ) ^m X ) )
49 48 6 fmptd 
 |-  ( ph -> H : NN --> ( ( RR X. RR ) ^m X ) )
50 ovex 
 |-  ( ( RR X. RR ) ^m X ) e. _V
51 nnex 
 |-  NN e. _V
52 50 51 elmap 
 |-  ( H e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> H : NN --> ( ( RR X. RR ) ^m X ) )
53 49 52 sylibr 
 |-  ( ph -> H e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
54 53 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> H e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
55 eqidd 
 |-  ( ph -> X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
56 35 fmpttd 
 |-  ( ph -> ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) : X --> ( RR X. RR ) )
57 iftrue 
 |-  ( j = 1 -> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) = <. ( A ` k ) , ( B ` k ) >. )
58 57 mpteq2dv 
 |-  ( j = 1 -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) = ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) )
59 1nn 
 |-  1 e. NN
60 59 a1i 
 |-  ( ph -> 1 e. NN )
61 mptexg 
 |-  ( X e. Fin -> ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) e. _V )
62 1 61 syl 
 |-  ( ph -> ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) e. _V )
63 6 58 60 62 fvmptd3 
 |-  ( ph -> ( H ` 1 ) = ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) )
64 63 feq1d 
 |-  ( ph -> ( ( H ` 1 ) : X --> ( RR X. RR ) <-> ( k e. X |-> <. ( A ` k ) , ( B ` k ) >. ) : X --> ( RR X. RR ) ) )
65 56 64 mpbird 
 |-  ( ph -> ( H ` 1 ) : X --> ( RR X. RR ) )
66 65 adantr 
 |-  ( ( ph /\ k e. X ) -> ( H ` 1 ) : X --> ( RR X. RR ) )
67 simpr 
 |-  ( ( ph /\ k e. X ) -> k e. X )
68 66 67 fvovco 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. ( H ` 1 ) ) ` k ) = ( ( 1st ` ( ( H ` 1 ) ` k ) ) [,) ( 2nd ` ( ( H ` 1 ) ` k ) ) ) )
69 35 elexd 
 |-  ( ( ph /\ k e. X ) -> <. ( A ` k ) , ( B ` k ) >. e. _V )
70 63 69 fvmpt2d 
 |-  ( ( ph /\ k e. X ) -> ( ( H ` 1 ) ` k ) = <. ( A ` k ) , ( B ` k ) >. )
71 70 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( ( H ` 1 ) ` k ) ) = ( 1st ` <. ( A ` k ) , ( B ` k ) >. ) )
72 fvex 
 |-  ( A ` k ) e. _V
73 fvex 
 |-  ( B ` k ) e. _V
74 72 73 op1st 
 |-  ( 1st ` <. ( A ` k ) , ( B ` k ) >. ) = ( A ` k )
75 74 a1i 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` <. ( A ` k ) , ( B ` k ) >. ) = ( A ` k ) )
76 71 75 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( 1st ` ( ( H ` 1 ) ` k ) ) = ( A ` k ) )
77 70 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( ( H ` 1 ) ` k ) ) = ( 2nd ` <. ( A ` k ) , ( B ` k ) >. ) )
78 72 73 op2nd 
 |-  ( 2nd ` <. ( A ` k ) , ( B ` k ) >. ) = ( B ` k )
79 78 a1i 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` <. ( A ` k ) , ( B ` k ) >. ) = ( B ` k ) )
80 77 79 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( 2nd ` ( ( H ` 1 ) ` k ) ) = ( B ` k ) )
81 76 80 oveq12d 
 |-  ( ( ph /\ k e. X ) -> ( ( 1st ` ( ( H ` 1 ) ` k ) ) [,) ( 2nd ` ( ( H ` 1 ) ` k ) ) ) = ( ( A ` k ) [,) ( B ` k ) ) )
82 68 81 eqtrd 
 |-  ( ( ph /\ k e. X ) -> ( ( [,) o. ( H ` 1 ) ) ` k ) = ( ( A ` k ) [,) ( B ` k ) ) )
83 82 ixpeq2dva 
 |-  ( ph -> X_ k e. X ( ( [,) o. ( H ` 1 ) ) ` k ) = X_ k e. X ( ( A ` k ) [,) ( B ` k ) ) )
84 55 7 83 3eqtr4d 
 |-  ( ph -> I = X_ k e. X ( ( [,) o. ( H ` 1 ) ) ` k ) )
85 fveq2 
 |-  ( j = 1 -> ( H ` j ) = ( H ` 1 ) )
86 85 coeq2d 
 |-  ( j = 1 -> ( [,) o. ( H ` j ) ) = ( [,) o. ( H ` 1 ) ) )
87 86 fveq1d 
 |-  ( j = 1 -> ( ( [,) o. ( H ` j ) ) ` k ) = ( ( [,) o. ( H ` 1 ) ) ` k ) )
88 87 ixpeq2dv 
 |-  ( j = 1 -> X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( H ` 1 ) ) ` k ) )
89 88 ssiun2s 
 |-  ( 1 e. NN -> X_ k e. X ( ( [,) o. ( H ` 1 ) ) ` k ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) )
90 59 89 ax-mp 
 |-  X_ k e. X ( ( [,) o. ( H ` 1 ) ) ` k ) C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k )
91 84 90 eqsstrdi 
 |-  ( ph -> I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) )
92 91 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) )
93 82 fveq2d 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) = ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
94 93 eqcomd 
 |-  ( ( ph /\ k e. X ) -> ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
95 94 prodeq2dv 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
96 95 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
97 1red 
 |-  ( ph -> 1 e. RR )
98 icossicc 
 |-  ( 0 [,) +oo ) C_ ( 0 [,] +oo )
99 8 1 65 hoiprodcl 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) e. ( 0 [,) +oo ) )
100 98 99 sseldi 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) e. ( 0 [,] +oo ) )
101 87 fveq2d 
 |-  ( j = 1 -> ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
102 101 prodeq2ad 
 |-  ( j = 1 -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
103 97 100 102 sge0snmpt 
 |-  ( ph -> ( sum^ ` ( j e. { 1 } |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) )
104 103 eqcomd 
 |-  ( ph -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) = ( sum^ ` ( j e. { 1 } |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) )
105 104 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` 1 ) ) ` k ) ) = ( sum^ ` ( j e. { 1 } |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) )
106 nfv 
 |-  F/ j ( ph /\ -. X = (/) )
107 51 a1i 
 |-  ( ( ph /\ -. X = (/) ) -> NN e. _V )
108 snssi 
 |-  ( 1 e. NN -> { 1 } C_ NN )
109 59 108 ax-mp 
 |-  { 1 } C_ NN
110 109 a1i 
 |-  ( ( ph /\ -. X = (/) ) -> { 1 } C_ NN )
111 nfv 
 |-  F/ k ( ( ph /\ -. X = (/) ) /\ j e. { 1 } )
112 1 ad2antrr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. { 1 } ) -> X e. Fin )
113 simpl 
 |-  ( ( ph /\ j e. { 1 } ) -> ph )
114 elsni 
 |-  ( j e. { 1 } -> j = 1 )
115 114 adantl 
 |-  ( ( ph /\ j e. { 1 } ) -> j = 1 )
116 65 adantr 
 |-  ( ( ph /\ j = 1 ) -> ( H ` 1 ) : X --> ( RR X. RR ) )
117 85 adantl 
 |-  ( ( ph /\ j = 1 ) -> ( H ` j ) = ( H ` 1 ) )
118 117 feq1d 
 |-  ( ( ph /\ j = 1 ) -> ( ( H ` j ) : X --> ( RR X. RR ) <-> ( H ` 1 ) : X --> ( RR X. RR ) ) )
119 116 118 mpbird 
 |-  ( ( ph /\ j = 1 ) -> ( H ` j ) : X --> ( RR X. RR ) )
120 113 115 119 syl2anc 
 |-  ( ( ph /\ j e. { 1 } ) -> ( H ` j ) : X --> ( RR X. RR ) )
121 120 adantlr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. { 1 } ) -> ( H ` j ) : X --> ( RR X. RR ) )
122 111 112 121 hoiprodcl 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. { 1 } ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) e. ( 0 [,) +oo ) )
123 98 122 sseldi 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. { 1 } ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) e. ( 0 [,] +oo ) )
124 39 fmpttd 
 |-  ( ph -> ( k e. X |-> <. 0 , 0 >. ) : X --> ( RR X. RR ) )
125 124 adantr 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( k e. X |-> <. 0 , 0 >. ) : X --> ( RR X. RR ) )
126 simpl 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ph )
127 eldifi 
 |-  ( j e. ( NN \ { 1 } ) -> j e. NN )
128 127 adantl 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> j e. NN )
129 6 a1i 
 |-  ( ph -> H = ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) ) )
130 48 elexd 
 |-  ( ( ph /\ j e. NN ) -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) e. _V )
131 129 130 fvmpt2d 
 |-  ( ( ph /\ j e. NN ) -> ( H ` j ) = ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
132 126 128 131 syl2anc 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( H ` j ) = ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
133 eldifsni 
 |-  ( j e. ( NN \ { 1 } ) -> j =/= 1 )
134 133 neneqd 
 |-  ( j e. ( NN \ { 1 } ) -> -. j = 1 )
135 134 iffalsed 
 |-  ( j e. ( NN \ { 1 } ) -> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) = <. 0 , 0 >. )
136 135 mpteq2dv 
 |-  ( j e. ( NN \ { 1 } ) -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) = ( k e. X |-> <. 0 , 0 >. ) )
137 136 adantl 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) = ( k e. X |-> <. 0 , 0 >. ) )
138 132 137 eqtrd 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( H ` j ) = ( k e. X |-> <. 0 , 0 >. ) )
139 138 feq1d 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( ( H ` j ) : X --> ( RR X. RR ) <-> ( k e. X |-> <. 0 , 0 >. ) : X --> ( RR X. RR ) ) )
140 125 139 mpbird 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> ( H ` j ) : X --> ( RR X. RR ) )
141 140 adantr 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( H ` j ) : X --> ( RR X. RR ) )
142 simpr 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> k e. X )
143 141 142 fvovco 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( ( [,) o. ( H ` j ) ) ` k ) = ( ( 1st ` ( ( H ` j ) ` k ) ) [,) ( 2nd ` ( ( H ` j ) ` k ) ) ) )
144 38 elexi 
 |-  <. 0 , 0 >. e. _V
145 144 a1i 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> <. 0 , 0 >. e. _V )
146 138 145 fvmpt2d 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( ( H ` j ) ` k ) = <. 0 , 0 >. )
147 146 fveq2d 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 1st ` ( ( H ` j ) ` k ) ) = ( 1st ` <. 0 , 0 >. ) )
148 17 elexi 
 |-  0 e. _V
149 148 148 op1st 
 |-  ( 1st ` <. 0 , 0 >. ) = 0
150 149 a1i 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 1st ` <. 0 , 0 >. ) = 0 )
151 147 150 eqtrd 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 1st ` ( ( H ` j ) ` k ) ) = 0 )
152 146 fveq2d 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 2nd ` ( ( H ` j ) ` k ) ) = ( 2nd ` <. 0 , 0 >. ) )
153 148 148 op2nd 
 |-  ( 2nd ` <. 0 , 0 >. ) = 0
154 153 a1i 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 2nd ` <. 0 , 0 >. ) = 0 )
155 152 154 eqtrd 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 2nd ` ( ( H ` j ) ` k ) ) = 0 )
156 151 155 oveq12d 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( ( 1st ` ( ( H ` j ) ` k ) ) [,) ( 2nd ` ( ( H ` j ) ` k ) ) ) = ( 0 [,) 0 ) )
157 0le0 
 |-  0 <_ 0
158 ico0 
 |-  ( ( 0 e. RR* /\ 0 e. RR* ) -> ( ( 0 [,) 0 ) = (/) <-> 0 <_ 0 ) )
159 17 17 158 mp2an 
 |-  ( ( 0 [,) 0 ) = (/) <-> 0 <_ 0 )
160 157 159 mpbir 
 |-  ( 0 [,) 0 ) = (/)
161 160 a1i 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( 0 [,) 0 ) = (/) )
162 143 156 161 3eqtrd 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( ( [,) o. ( H ` j ) ) ` k ) = (/) )
163 162 fveq2d 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = ( vol ` (/) ) )
164 vol0 
 |-  ( vol ` (/) ) = 0
165 164 a1i 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( vol ` (/) ) = 0 )
166 163 165 eqtrd 
 |-  ( ( ( ph /\ j e. ( NN \ { 1 } ) ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = 0 )
167 166 prodeq2dv 
 |-  ( ( ph /\ j e. ( NN \ { 1 } ) ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = prod_ k e. X 0 )
168 167 adantlr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. ( NN \ { 1 } ) ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = prod_ k e. X 0 )
169 0cnd 
 |-  ( ph -> 0 e. CC )
170 fprodconst 
 |-  ( ( X e. Fin /\ 0 e. CC ) -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
171 1 169 170 syl2anc 
 |-  ( ph -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
172 171 ad2antrr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. ( NN \ { 1 } ) ) -> prod_ k e. X 0 = ( 0 ^ ( # ` X ) ) )
173 neqne 
 |-  ( -. X = (/) -> X =/= (/) )
174 173 adantl 
 |-  ( ( ph /\ -. X = (/) ) -> X =/= (/) )
175 1 adantr 
 |-  ( ( ph /\ -. X = (/) ) -> X e. Fin )
176 hashnncl 
 |-  ( X e. Fin -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
177 175 176 syl 
 |-  ( ( ph /\ -. X = (/) ) -> ( ( # ` X ) e. NN <-> X =/= (/) ) )
178 174 177 mpbird 
 |-  ( ( ph /\ -. X = (/) ) -> ( # ` X ) e. NN )
179 0exp 
 |-  ( ( # ` X ) e. NN -> ( 0 ^ ( # ` X ) ) = 0 )
180 178 179 syl 
 |-  ( ( ph /\ -. X = (/) ) -> ( 0 ^ ( # ` X ) ) = 0 )
181 180 adantr 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. ( NN \ { 1 } ) ) -> ( 0 ^ ( # ` X ) ) = 0 )
182 168 172 181 3eqtrd 
 |-  ( ( ( ph /\ -. X = (/) ) /\ j e. ( NN \ { 1 } ) ) -> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) = 0 )
183 106 107 110 123 182 sge0ss 
 |-  ( ( ph /\ -. X = (/) ) -> ( sum^ ` ( j e. { 1 } |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) )
184 96 105 183 3eqtrd 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) )
185 92 184 jca 
 |-  ( ( ph /\ -. X = (/) ) -> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) ) )
186 nfcv 
 |-  F/_ k i
187 nfcv 
 |-  F/_ k NN
188 nfmpt1 
 |-  F/_ k ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) )
189 187 188 nfmpt 
 |-  F/_ k ( j e. NN |-> ( k e. X |-> if ( j = 1 , <. ( A ` k ) , ( B ` k ) >. , <. 0 , 0 >. ) ) )
190 6 189 nfcxfr 
 |-  F/_ k H
191 186 190 nfeq 
 |-  F/ k i = H
192 fveq1 
 |-  ( i = H -> ( i ` j ) = ( H ` j ) )
193 192 coeq2d 
 |-  ( i = H -> ( [,) o. ( i ` j ) ) = ( [,) o. ( H ` j ) ) )
194 193 fveq1d 
 |-  ( i = H -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( H ` j ) ) ` k ) )
195 194 adantr 
 |-  ( ( i = H /\ k e. X ) -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( H ` j ) ) ` k ) )
196 191 195 ixpeq2d 
 |-  ( i = H -> X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) )
197 196 iuneq2d 
 |-  ( i = H -> U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) = U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) )
198 197 sseq2d 
 |-  ( i = H -> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) <-> I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) ) )
199 194 fveq2d 
 |-  ( i = H -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) )
200 199 a1d 
 |-  ( i = H -> ( k e. X -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) )
201 191 200 ralrimi 
 |-  ( i = H -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) )
202 201 prodeq2d 
 |-  ( i = H -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) )
203 202 mpteq2dv 
 |-  ( i = H -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) )
204 203 fveq2d 
 |-  ( i = H -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) )
205 204 eqeq2d 
 |-  ( i = H -> ( prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) ) )
206 198 205 anbi12d 
 |-  ( i = H -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) ) ) )
207 206 rspcev 
 |-  ( ( H e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( H ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( H ` j ) ) ` k ) ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
208 54 185 207 syl2anc 
 |-  ( ( ph /\ -. X = (/) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
209 33 208 jca 
 |-  ( ( ph /\ -. X = (/) ) -> ( prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
210 eqeq1 
 |-  ( z = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
211 210 anbi2d 
 |-  ( z = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) -> ( ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
212 211 rexbidv 
 |-  ( z = prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
213 212 elrab 
 |-  ( prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } <-> ( prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) ) )
214 209 213 sylibr 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } )
215 5 eqcomi 
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = M
216 215 a1i 
 |-  ( ( ph /\ -. X = (/) ) -> { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) ( I C_ U_ j e. NN X_ k e. X ( ( [,) o. ( i ` j ) ) ` k ) /\ z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) } = M )
217 214 216 eleqtrd 
 |-  ( ( ph /\ -. X = (/) ) -> prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. M )
218 infxrlb 
 |-  ( ( M C_ RR* /\ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) e. M ) -> inf ( M , RR* , < ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
219 30 217 218 syl2anc 
 |-  ( ( ph /\ -. X = (/) ) -> inf ( M , RR* , < ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
220 27 219 eqbrtrd 
 |-  ( ( ph /\ -. X = (/) ) -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
221 25 220 pm2.61dan 
 |-  ( ph -> if ( X = (/) , 0 , inf ( M , RR* , < ) ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )
222 14 221 eqbrtrd 
 |-  ( ph -> ( ( voln* ` X ) ` I ) <_ prod_ k e. X ( vol ` ( ( A ` k ) [,) ( B ` k ) ) ) )