Metamath Proof Explorer


Theorem ovnlecvr

Description: Given a subset of multidimensional reals and a set of half-open intervals that covers it, the Lebesgue outer measure of the set is bounded by the generalized sum of the pre-measure of the half-open intervals. The statement would also be true with X the empty set, but covers are not used for the zero-dimensional case. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses ovnlecvr.x φ X Fin
ovnlecvr.n0 φ X
ovnlecvr.l L = i 2 X k X vol . i k
ovnlecvr.i φ I : 2 X
ovnlecvr.ss φ A j k X . I j k
Assertion ovnlecvr φ voln* X A sum^ j L I j

Proof

Step Hyp Ref Expression
1 ovnlecvr.x φ X Fin
2 ovnlecvr.n0 φ X
3 ovnlecvr.l L = i 2 X k X vol . i k
4 ovnlecvr.i φ I : 2 X
5 ovnlecvr.ss φ A j k X . I j k
6 4 ffvelrnda φ j I j 2 X
7 elmapi I j 2 X I j : X 2
8 6 7 syl φ j I j : X 2
9 8 hoissrrn φ j k X . I j k X
10 9 ralrimiva φ j k X . I j k X
11 iunss j k X . I j k X j k X . I j k X
12 10 11 sylibr φ j k X . I j k X
13 5 12 sstrd φ A X
14 eqid z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k = z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k
15 1 2 13 14 ovnn0val φ voln* X A = sup z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k * <
16 ssrab2 z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k *
17 16 a1i φ z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k *
18 nnex V
19 18 a1i φ V
20 icossicc 0 +∞ 0 +∞
21 nfv k φ j
22 1 adantr φ j X Fin
23 21 22 3 8 hoiprodcl2 φ j L I j 0 +∞
24 20 23 sseldi φ j L I j 0 +∞
25 eqid j L I j = j L I j
26 24 25 fmptd φ j L I j : 0 +∞
27 19 26 sge0xrcl φ sum^ j L I j *
28 ovex 2 X V
29 28 18 pm3.2i 2 X V V
30 elmapg 2 X V V I 2 X I : 2 X
31 29 30 ax-mp I 2 X I : 2 X
32 4 31 sylibr φ I 2 X
33 coeq2 i = I j . i = . I j
34 33 fveq1d i = I j . i k = . I j k
35 34 fveq2d i = I j vol . i k = vol . I j k
36 35 prodeq2ad i = I j k X vol . i k = k X vol . I j k
37 prodex k X vol . I j k V
38 37 a1i φ j k X vol . I j k V
39 3 36 6 38 fvmptd3 φ j L I j = k X vol . I j k
40 39 mpteq2dva φ j L I j = j k X vol . I j k
41 40 fveq2d φ sum^ j L I j = sum^ j k X vol . I j k
42 5 41 jca φ A j k X . I j k sum^ j L I j = sum^ j k X vol . I j k
43 nfv k i = I
44 fveq1 i = I i j = I j
45 44 coeq2d i = I . i j = . I j
46 45 fveq1d i = I . i j k = . I j k
47 46 adantr i = I k X . i j k = . I j k
48 43 47 ixpeq2d i = I k X . i j k = k X . I j k
49 48 iuneq2d i = I j k X . i j k = j k X . I j k
50 49 sseq2d i = I A j k X . i j k A j k X . I j k
51 46 fveq2d i = I vol . i j k = vol . I j k
52 51 prodeq2ad i = I k X vol . i j k = k X vol . I j k
53 52 mpteq2dv i = I j k X vol . i j k = j k X vol . I j k
54 53 fveq2d i = I sum^ j k X vol . i j k = sum^ j k X vol . I j k
55 54 eqeq2d i = I sum^ j L I j = sum^ j k X vol . i j k sum^ j L I j = sum^ j k X vol . I j k
56 50 55 anbi12d i = I A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k A j k X . I j k sum^ j L I j = sum^ j k X vol . I j k
57 56 rspcev I 2 X A j k X . I j k sum^ j L I j = sum^ j k X vol . I j k i 2 X A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
58 32 42 57 syl2anc φ i 2 X A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
59 27 58 jca φ sum^ j L I j * i 2 X A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
60 eqeq1 z = sum^ j L I j z = sum^ j k X vol . i j k sum^ j L I j = sum^ j k X vol . i j k
61 60 anbi2d z = sum^ j L I j A j k X . i j k z = sum^ j k X vol . i j k A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
62 61 rexbidv z = sum^ j L I j i 2 X A j k X . i j k z = sum^ j k X vol . i j k i 2 X A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
63 62 elrab sum^ j L I j z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k sum^ j L I j * i 2 X A j k X . i j k sum^ j L I j = sum^ j k X vol . i j k
64 59 63 sylibr φ sum^ j L I j z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k
65 infxrlb z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k * sum^ j L I j z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k sup z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k * < sum^ j L I j
66 17 64 65 syl2anc φ sup z * | i 2 X A j k X . i j k z = sum^ j k X vol . i j k * < sum^ j L I j
67 15 66 eqbrtrd φ voln* X A sum^ j L I j