Metamath Proof Explorer


Theorem ovn0lem

Description: For any finite dimension, the Lebesgue outer measure of the empty set is zero. This is step (a)(ii) of the proof of Proposition 115D (a) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovn0lem.x
|- ( ph -> X e. Fin )
ovn0lem.n0
|- ( ph -> X =/= (/) )
ovn0lem.m
|- M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) }
ovn0lem.infm
|- ( ph -> inf ( M , RR* , < ) e. ( 0 [,] +oo ) )
ovn0lem.i
|- I = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )
Assertion ovn0lem
|- ( ph -> inf ( M , RR* , < ) = 0 )

Proof

Step Hyp Ref Expression
1 ovn0lem.x
 |-  ( ph -> X e. Fin )
2 ovn0lem.n0
 |-  ( ph -> X =/= (/) )
3 ovn0lem.m
 |-  M = { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) }
4 ovn0lem.infm
 |-  ( ph -> inf ( M , RR* , < ) e. ( 0 [,] +oo ) )
5 ovn0lem.i
 |-  I = ( j e. NN |-> ( l e. X |-> <. 1 , 0 >. ) )
6 iccssxr
 |-  ( 0 [,] +oo ) C_ RR*
7 6 4 sselid
 |-  ( ph -> inf ( M , RR* , < ) e. RR* )
8 0xr
 |-  0 e. RR*
9 8 a1i
 |-  ( ph -> 0 e. RR* )
10 ssrab2
 |-  { z e. RR* | E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) } C_ RR*
11 3 10 eqsstri
 |-  M C_ RR*
12 11 a1i
 |-  ( ph -> M C_ RR* )
13 1re
 |-  1 e. RR
14 0re
 |-  0 e. RR
15 13 14 pm3.2i
 |-  ( 1 e. RR /\ 0 e. RR )
16 opelxp
 |-  ( <. 1 , 0 >. e. ( RR X. RR ) <-> ( 1 e. RR /\ 0 e. RR ) )
17 15 16 mpbir
 |-  <. 1 , 0 >. e. ( RR X. RR )
18 17 a1i
 |-  ( ( ph /\ l e. X ) -> <. 1 , 0 >. e. ( RR X. RR ) )
19 eqid
 |-  ( l e. X |-> <. 1 , 0 >. ) = ( l e. X |-> <. 1 , 0 >. )
20 18 19 fmptd
 |-  ( ph -> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) )
21 reex
 |-  RR e. _V
22 21 21 xpex
 |-  ( RR X. RR ) e. _V
23 22 a1i
 |-  ( ph -> ( RR X. RR ) e. _V )
24 elmapg
 |-  ( ( ( RR X. RR ) e. _V /\ X e. Fin ) -> ( ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) <-> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) ) )
25 23 1 24 syl2anc
 |-  ( ph -> ( ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) <-> ( l e. X |-> <. 1 , 0 >. ) : X --> ( RR X. RR ) ) )
26 20 25 mpbird
 |-  ( ph -> ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) )
27 26 adantr
 |-  ( ( ph /\ j e. NN ) -> ( l e. X |-> <. 1 , 0 >. ) e. ( ( RR X. RR ) ^m X ) )
28 27 5 fmptd
 |-  ( ph -> I : NN --> ( ( RR X. RR ) ^m X ) )
29 ovexd
 |-  ( ph -> ( ( RR X. RR ) ^m X ) e. _V )
30 nnex
 |-  NN e. _V
31 30 a1i
 |-  ( ph -> NN e. _V )
32 elmapg
 |-  ( ( ( ( RR X. RR ) ^m X ) e. _V /\ NN e. _V ) -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) ) )
33 29 31 32 syl2anc
 |-  ( ph -> ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) <-> I : NN --> ( ( RR X. RR ) ^m X ) ) )
34 28 33 mpbird
 |-  ( ph -> I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) )
35 n0
 |-  ( X =/= (/) <-> E. l l e. X )
36 2 35 sylib
 |-  ( ph -> E. l l e. X )
37 36 adantr
 |-  ( ( ph /\ j e. NN ) -> E. l l e. X )
38 nfv
 |-  F/ k ( ( ph /\ j e. NN ) /\ l e. X )
39 nfcv
 |-  F/_ k ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) )
40 1 ad2antrr
 |-  ( ( ( ph /\ j e. NN ) /\ l e. X ) -> X e. Fin )
41 28 ffvelrnda
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) e. ( ( RR X. RR ) ^m X ) )
42 elmapi
 |-  ( ( I ` j ) e. ( ( RR X. RR ) ^m X ) -> ( I ` j ) : X --> ( RR X. RR ) )
43 41 42 syl
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) : X --> ( RR X. RR ) )
44 43 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( I ` j ) : X --> ( RR X. RR ) )
45 simpr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> k e. X )
46 44 45 fvovco
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) )
47 simpr
 |-  ( ( ph /\ j e. NN ) -> j e. NN )
48 27 elexd
 |-  ( ( ph /\ j e. NN ) -> ( l e. X |-> <. 1 , 0 >. ) e. _V )
49 5 fvmpt2
 |-  ( ( j e. NN /\ ( l e. X |-> <. 1 , 0 >. ) e. _V ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
50 47 48 49 syl2anc
 |-  ( ( ph /\ j e. NN ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
51 50 adantr
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( I ` j ) = ( l e. X |-> <. 1 , 0 >. ) )
52 eqidd
 |-  ( ( ( ( ph /\ j e. NN ) /\ k e. X ) /\ l = k ) -> <. 1 , 0 >. = <. 1 , 0 >. )
53 17 elexi
 |-  <. 1 , 0 >. e. _V
54 53 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> <. 1 , 0 >. e. _V )
55 51 52 45 54 fvmptd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( I ` j ) ` k ) = <. 1 , 0 >. )
56 55 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) = ( 1st ` <. 1 , 0 >. ) )
57 13 elexi
 |-  1 e. _V
58 8 elexi
 |-  0 e. _V
59 57 58 op1st
 |-  ( 1st ` <. 1 , 0 >. ) = 1
60 59 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` <. 1 , 0 >. ) = 1 )
61 56 60 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1st ` ( ( I ` j ) ` k ) ) = 1 )
62 55 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) = ( 2nd ` <. 1 , 0 >. ) )
63 57 58 op2nd
 |-  ( 2nd ` <. 1 , 0 >. ) = 0
64 63 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` <. 1 , 0 >. ) = 0 )
65 62 64 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 2nd ` ( ( I ` j ) ` k ) ) = 0 )
66 61 65 oveq12d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( 1st ` ( ( I ` j ) ` k ) ) [,) ( 2nd ` ( ( I ` j ) ` k ) ) ) = ( 1 [,) 0 ) )
67 0le1
 |-  0 <_ 1
68 1xr
 |-  1 e. RR*
69 ico0
 |-  ( ( 1 e. RR* /\ 0 e. RR* ) -> ( ( 1 [,) 0 ) = (/) <-> 0 <_ 1 ) )
70 68 8 69 mp2an
 |-  ( ( 1 [,) 0 ) = (/) <-> 0 <_ 1 )
71 67 70 mpbir
 |-  ( 1 [,) 0 ) = (/)
72 71 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( 1 [,) 0 ) = (/) )
73 46 66 72 3eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( ( [,) o. ( I ` j ) ) ` k ) = (/) )
74 73 fveq2d
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` (/) ) )
75 vol0
 |-  ( vol ` (/) ) = 0
76 75 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` (/) ) = 0 )
77 74 76 eqtrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
78 0cn
 |-  0 e. CC
79 78 a1i
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> 0 e. CC )
80 77 79 eqeltrd
 |-  ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. CC )
81 80 adantlr
 |-  ( ( ( ( ph /\ j e. NN ) /\ l e. X ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) e. CC )
82 2fveq3
 |-  ( k = l -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) )
83 simpr
 |-  ( ( ( ph /\ j e. NN ) /\ l e. X ) -> l e. X )
84 eleq1w
 |-  ( k = l -> ( k e. X <-> l e. X ) )
85 84 anbi2d
 |-  ( k = l -> ( ( ( ph /\ j e. NN ) /\ k e. X ) <-> ( ( ph /\ j e. NN ) /\ l e. X ) ) )
86 82 eqeq1d
 |-  ( k = l -> ( ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 <-> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 ) )
87 85 86 imbi12d
 |-  ( k = l -> ( ( ( ( ph /\ j e. NN ) /\ k e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) <-> ( ( ( ph /\ j e. NN ) /\ l e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 ) ) )
88 87 77 chvarvv
 |-  ( ( ( ph /\ j e. NN ) /\ l e. X ) -> ( vol ` ( ( [,) o. ( I ` j ) ) ` l ) ) = 0 )
89 38 39 40 81 82 83 88 fprod0
 |-  ( ( ( ph /\ j e. NN ) /\ l e. X ) -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
90 89 ex
 |-  ( ( ph /\ j e. NN ) -> ( l e. X -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) )
91 90 exlimdv
 |-  ( ( ph /\ j e. NN ) -> ( E. l l e. X -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 ) )
92 37 91 mpd
 |-  ( ( ph /\ j e. NN ) -> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) = 0 )
93 92 mpteq2dva
 |-  ( ph -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) = ( j e. NN |-> 0 ) )
94 93 fveq2d
 |-  ( ph -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> 0 ) ) )
95 nfv
 |-  F/ j ph
96 95 31 sge0z
 |-  ( ph -> ( sum^ ` ( j e. NN |-> 0 ) ) = 0 )
97 eqidd
 |-  ( ph -> 0 = 0 )
98 94 96 97 3eqtrrd
 |-  ( ph -> 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
99 fveq1
 |-  ( i = I -> ( i ` j ) = ( I ` j ) )
100 99 coeq2d
 |-  ( i = I -> ( [,) o. ( i ` j ) ) = ( [,) o. ( I ` j ) ) )
101 100 fveq1d
 |-  ( i = I -> ( ( [,) o. ( i ` j ) ) ` k ) = ( ( [,) o. ( I ` j ) ) ` k ) )
102 101 fveq2d
 |-  ( i = I -> ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
103 102 ralrimivw
 |-  ( i = I -> A. k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
104 103 prodeq2d
 |-  ( i = I -> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) = prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) )
105 104 mpteq2dv
 |-  ( i = I -> ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) = ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) )
106 105 fveq2d
 |-  ( i = I -> ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) )
107 106 rspceeqv
 |-  ( ( I e. ( ( ( RR X. RR ) ^m X ) ^m NN ) /\ 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( I ` j ) ) ` k ) ) ) ) ) -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
108 34 98 107 syl2anc
 |-  ( ph -> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) )
109 9 108 jca
 |-  ( ph -> ( 0 e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
110 eqeq1
 |-  ( z = 0 -> ( z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
111 110 rexbidv
 |-  ( z = 0 -> ( E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) z = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) <-> E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
112 111 3 elrab2
 |-  ( 0 e. M <-> ( 0 e. RR* /\ E. i e. ( ( ( RR X. RR ) ^m X ) ^m NN ) 0 = ( sum^ ` ( j e. NN |-> prod_ k e. X ( vol ` ( ( [,) o. ( i ` j ) ) ` k ) ) ) ) ) )
113 109 112 sylibr
 |-  ( ph -> 0 e. M )
114 infxrlb
 |-  ( ( M C_ RR* /\ 0 e. M ) -> inf ( M , RR* , < ) <_ 0 )
115 12 113 114 syl2anc
 |-  ( ph -> inf ( M , RR* , < ) <_ 0 )
116 pnfxr
 |-  +oo e. RR*
117 116 a1i
 |-  ( ph -> +oo e. RR* )
118 iccgelb
 |-  ( ( 0 e. RR* /\ +oo e. RR* /\ inf ( M , RR* , < ) e. ( 0 [,] +oo ) ) -> 0 <_ inf ( M , RR* , < ) )
119 9 117 4 118 syl3anc
 |-  ( ph -> 0 <_ inf ( M , RR* , < ) )
120 7 9 115 119 xrletrid
 |-  ( ph -> inf ( M , RR* , < ) = 0 )