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 φ X Fin
ovn0lem.n0 φ X
ovn0lem.m M = z * | i 2 X z = sum^ j k X vol . i j k
ovn0lem.infm φ sup M * < 0 +∞
ovn0lem.i I = j l X 1 0
Assertion ovn0lem φ sup M * < = 0

Proof

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