Metamath Proof Explorer


Theorem ovnhoi

Description: The Lebesgue outer measure of a multidimensional half-open interval is its dimensional volume (the product of its length in each dimension, when the dimension is nonzero). Proposition 115D (b) of Fremlin1 p. 30. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses ovnhoi.x φ X Fin
ovnhoi.a φ A : X
ovnhoi.b φ B : X
ovnhoi.c I = k X A k B k
ovnhoi.l L = x Fin a x , b x if x = 0 k x vol a k b k
Assertion ovnhoi φ voln* X I = A L X B

Proof

Step Hyp Ref Expression
1 ovnhoi.x φ X Fin
2 ovnhoi.a φ A : X
3 ovnhoi.b φ B : X
4 ovnhoi.c I = k X A k B k
5 ovnhoi.l L = x Fin a x , b x if x = 0 k x vol a k b k
6 4 a1i φ I = k X A k B k
7 nfv k φ
8 2 ffvelrnda φ k X A k
9 3 ffvelrnda φ k X B k
10 9 rexrd φ k X B k *
11 7 8 10 hoissrrn2 φ k X A k B k X
12 6 11 eqsstrd φ I X
13 1 12 ovnxrcl φ voln* X I *
14 icossxr 0 +∞ *
15 5 1 2 3 hoidmvcl φ A L X B 0 +∞
16 14 15 sseldi φ A L X B *
17 fveq2 X = voln* X = voln*
18 17 fveq1d X = voln* X I = voln* I
19 18 adantl φ X = voln* X I = voln* I
20 ixpeq1 X = k X A k B k = k A k B k
21 ixp0x k A k B k =
22 21 a1i X = k A k B k =
23 20 22 eqtrd X = k X A k B k =
24 23 adantl φ X = k X A k B k =
25 4 a1i φ X = I = k X A k B k
26 reex V
27 mapdm0 V =
28 26 27 ax-mp =
29 28 a1i φ X = =
30 24 25 29 3eqtr4d φ X = I =
31 eqimss I = I
32 30 31 syl φ X = I
33 32 ovn0val φ X = voln* I = 0
34 19 33 eqtrd φ X = voln* X I = 0
35 0red φ X = 0
36 34 35 eqeltrd φ X = voln* X I
37 eqidd φ X = 0 = 0
38 fveq2 X = L X = L
39 38 oveqd X = A L X B = A L B
40 39 adantl φ X = A L X B = A L B
41 2 adantr φ X = A : X
42 simpr φ X = X =
43 42 feq2d φ X = A : X A :
44 41 43 mpbid φ X = A :
45 3 adantr φ X = B : X
46 42 feq2d φ X = B : X B :
47 45 46 mpbid φ X = B :
48 5 44 47 hoidmv0val φ X = A L B = 0
49 40 48 eqtrd φ X = A L X B = 0
50 37 34 49 3eqtr4d φ X = voln* X I = A L X B
51 36 50 eqled φ X = voln* X I A L X B
52 eqid z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k = z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k
53 eqeq1 n = j n = 1 j = 1
54 53 ifbid n = j if n = 1 A k B k 0 0 = if j = 1 A k B k 0 0
55 54 mpteq2dv n = j k X if n = 1 A k B k 0 0 = k X if j = 1 A k B k 0 0
56 55 cbvmptv n k X if n = 1 A k B k 0 0 = j k X if j = 1 A k B k 0 0
57 1 2 3 4 52 56 ovnhoilem1 φ voln* X I k X vol A k B k
58 57 adantr φ ¬ X = voln* X I k X vol A k B k
59 1 adantr φ ¬ X = X Fin
60 neqne ¬ X = X
61 60 adantl φ ¬ X = X
62 2 adantr φ ¬ X = A : X
63 3 adantr φ ¬ X = B : X
64 5 59 61 62 63 hoidmvn0val φ ¬ X = A L X B = k X vol A k B k
65 64 eqcomd φ ¬ X = k X vol A k B k = A L X B
66 58 65 breqtrd φ ¬ X = voln* X I A L X B
67 51 66 pm2.61dan φ voln* X I A L X B
68 49 35 eqeltrd φ X = A L X B
69 50 eqcomd φ X = A L X B = voln* X I
70 68 69 eqled φ X = A L X B voln* X I
71 fveq1 a = c a k = c k
72 71 fvoveq1d a = c vol a k b k = vol c k b k
73 72 prodeq2ad a = c k x vol a k b k = k x vol c k b k
74 73 ifeq2d a = c if x = 0 k x vol a k b k = if x = 0 k x vol c k b k
75 fveq1 b = d b k = d k
76 75 oveq2d b = d c k b k = c k d k
77 76 fveq2d b = d vol c k b k = vol c k d k
78 77 prodeq2ad b = d k x vol c k b k = k x vol c k d k
79 78 ifeq2d b = d if x = 0 k x vol c k b k = if x = 0 k x vol c k d k
80 74 79 cbvmpov a x , b x if x = 0 k x vol a k b k = c x , d x if x = 0 k x vol c k d k
81 80 a1i x = y a x , b x if x = 0 k x vol a k b k = c x , d x if x = 0 k x vol c k d k
82 oveq2 x = y x = y
83 eqeq1 x = y x = y =
84 prodeq1 x = y k x vol c k d k = k y vol c k d k
85 83 84 ifbieq2d x = y if x = 0 k x vol c k d k = if y = 0 k y vol c k d k
86 82 82 85 mpoeq123dv x = y c x , d x if x = 0 k x vol c k d k = c y , d y if y = 0 k y vol c k d k
87 81 86 eqtrd x = y a x , b x if x = 0 k x vol a k b k = c y , d y if y = 0 k y vol c k d k
88 87 cbvmptv x Fin a x , b x if x = 0 k x vol a k b k = y Fin c y , d y if y = 0 k y vol c k d k
89 5 88 eqtri L = y Fin c y , d y if y = 0 k y vol c k d k
90 eqeq1 w = z w = sum^ j k X vol . h j k z = sum^ j k X vol . h j k
91 90 anbi2d w = z I j k X . h j k w = sum^ j k X vol . h j k I j k X . h j k z = sum^ j k X vol . h j k
92 91 rexbidv w = z h 2 X I j k X . h j k w = sum^ j k X vol . h j k h 2 X I j k X . h j k z = sum^ j k X vol . h j k
93 simpl h = i j h = i
94 93 fveq1d h = i j h j = i j
95 94 coeq2d h = i j . h j = . i j
96 95 fveq1d h = i j . h j k = . i j k
97 96 ixpeq2dv h = i j k X . h j k = k X . i j k
98 97 iuneq2dv h = i j k X . h j k = j k X . i j k
99 98 sseq2d h = i I j k X . h j k I j k X . i j k
100 simpl h = i k X h = i
101 100 fveq1d h = i k X h j = i j
102 101 coeq2d h = i k X . h j = . i j
103 102 fveq1d h = i k X . h j k = . i j k
104 103 fveq2d h = i k X vol . h j k = vol . i j k
105 104 prodeq2dv h = i k X vol . h j k = k X vol . i j k
106 105 mpteq2dv h = i j k X vol . h j k = j k X vol . i j k
107 106 fveq2d h = i sum^ j k X vol . h j k = sum^ j k X vol . i j k
108 107 eqeq2d h = i z = sum^ j k X vol . h j k z = sum^ j k X vol . i j k
109 99 108 anbi12d h = i I j k X . h j k z = sum^ j k X vol . h j k I j k X . i j k z = sum^ j k X vol . i j k
110 109 cbvrexvw h 2 X I j k X . h j k z = sum^ j k X vol . h j k i 2 X I j k X . i j k z = sum^ j k X vol . i j k
111 110 a1i w = z h 2 X I j k X . h j k z = sum^ j k X vol . h j k i 2 X I j k X . i j k z = sum^ j k X vol . i j k
112 92 111 bitrd w = z h 2 X I j k X . h j k w = sum^ j k X vol . h j k i 2 X I j k X . i j k z = sum^ j k X vol . i j k
113 112 cbvrabv w * | h 2 X I j k X . h j k w = sum^ j k X vol . h j k = z * | i 2 X I j k X . i j k z = sum^ j k X vol . i j k
114 simpl j = n l X j = n
115 114 fveq2d j = n l X i j = i n
116 115 fveq1d j = n l X i j l = i n l
117 116 fveq2d j = n l X 1 st i j l = 1 st i n l
118 117 mpteq2dva j = n l X 1 st i j l = l X 1 st i n l
119 118 cbvmptv j l X 1 st i j l = n l X 1 st i n l
120 119 mpteq2i i 2 X j l X 1 st i j l = i 2 X n l X 1 st i n l
121 116 fveq2d j = n l X 2 nd i j l = 2 nd i n l
122 121 mpteq2dva j = n l X 2 nd i j l = l X 2 nd i n l
123 122 cbvmptv j l X 2 nd i j l = n l X 2 nd i n l
124 123 mpteq2i i 2 X j l X 2 nd i j l = i 2 X n l X 2 nd i n l
125 59 61 62 63 4 89 113 120 124 ovnhoilem2 φ ¬ X = A L X B voln* X I
126 70 125 pm2.61dan φ A L X B voln* X I
127 13 16 67 126 xrletrid φ voln* X I = A L X B