Metamath Proof Explorer


Theorem hoidmv1lelem3

Description: The dimensional volume of a 1-dimensional half-open interval is less than or equal the generalized sum of the dimensional volumes of countable half-open intervals that cover it. This is the nonempty, finite generalized sum, sub case in Lemma 114B of Fremlin1 p. 23. (Contributed by Glauco Siliprandi, 21-Nov-2020)

Ref Expression
Hypotheses hoidmv1lelem3.a φ A
hoidmv1lelem3.b φ B
hoidmv1lelem3.l φ A < B
hoidmv1lelem3.c φ C :
hoidmv1lelem3.d φ D :
hoidmv1lelem3.x φ A B j C j D j
hoidmv1lelem3.r φ sum^ j vol C j D j
hoidmv1lelem3.u U = z A B | z A sum^ j vol C j if D j z D j z
hoidmv1lelem3.s S = sup U <
Assertion hoidmv1lelem3 φ B A sum^ j vol C j D j

Proof

Step Hyp Ref Expression
1 hoidmv1lelem3.a φ A
2 hoidmv1lelem3.b φ B
3 hoidmv1lelem3.l φ A < B
4 hoidmv1lelem3.c φ C :
5 hoidmv1lelem3.d φ D :
6 hoidmv1lelem3.x φ A B j C j D j
7 hoidmv1lelem3.r φ sum^ j vol C j D j
8 hoidmv1lelem3.u U = z A B | z A sum^ j vol C j if D j z D j z
9 hoidmv1lelem3.s S = sup U <
10 2 1 resubcld φ B A
11 nnex V
12 11 a1i φ V
13 icossicc 0 +∞ 0 +∞
14 0xr 0 *
15 14 a1i φ j 0 *
16 pnfxr +∞ *
17 16 a1i φ j +∞ *
18 4 ffvelrnda φ j C j
19 5 ffvelrnda φ j D j
20 2 adantr φ j B
21 19 20 ifcld φ j if D j B D j B
22 volicore C j if D j B D j B vol C j if D j B D j B
23 18 21 22 syl2anc φ j vol C j if D j B D j B
24 23 rexrd φ j vol C j if D j B D j B *
25 21 rexrd φ j if D j B D j B *
26 icombl C j if D j B D j B * C j if D j B D j B dom vol
27 18 25 26 syl2anc φ j C j if D j B D j B dom vol
28 volge0 C j if D j B D j B dom vol 0 vol C j if D j B D j B
29 27 28 syl φ j 0 vol C j if D j B D j B
30 23 ltpnfd φ j vol C j if D j B D j B < +∞
31 15 17 24 29 30 elicod φ j vol C j if D j B D j B 0 +∞
32 13 31 sseldi φ j vol C j if D j B D j B 0 +∞
33 eqid j vol C j if D j B D j B = j vol C j if D j B D j B
34 32 33 fmptd φ j vol C j if D j B D j B : 0 +∞
35 12 34 sge0xrcl φ sum^ j vol C j if D j B D j B *
36 16 a1i φ +∞ *
37 7 rexrd φ sum^ j vol C j D j *
38 nfv j φ
39 volf vol : dom vol 0 +∞
40 39 a1i φ j vol : dom vol 0 +∞
41 19 rexrd φ j D j *
42 icombl C j D j * C j D j dom vol
43 18 41 42 syl2anc φ j C j D j dom vol
44 40 43 ffvelrnd φ j vol C j D j 0 +∞
45 18 rexrd φ j C j *
46 18 leidd φ j C j C j
47 min1 D j B if D j B D j B D j
48 19 20 47 syl2anc φ j if D j B D j B D j
49 icossico C j * D j * C j C j if D j B D j B D j C j if D j B D j B C j D j
50 45 41 46 48 49 syl22anc φ j C j if D j B D j B C j D j
51 volss C j if D j B D j B dom vol C j D j dom vol C j if D j B D j B C j D j vol C j if D j B D j B vol C j D j
52 27 43 50 51 syl3anc φ j vol C j if D j B D j B vol C j D j
53 38 12 32 44 52 sge0lempt φ sum^ j vol C j if D j B D j B sum^ j vol C j D j
54 7 ltpnfd φ sum^ j vol C j D j < +∞
55 35 37 36 53 54 xrlelttrd φ sum^ j vol C j if D j B D j B < +∞
56 35 36 55 xrltned φ sum^ j vol C j if D j B D j B +∞
57 56 neneqd φ ¬ sum^ j vol C j if D j B D j B = +∞
58 12 34 sge0repnf φ sum^ j vol C j if D j B D j B ¬ sum^ j vol C j if D j B D j B = +∞
59 57 58 mpbird φ sum^ j vol C j if D j B D j B
60 2 rexrd φ B *
61 1 2 iccssred φ A B
62 ssrab2 z A B | z A sum^ j vol C j if D j z D j z A B
63 8 62 eqsstri U A B
64 1 2 3 4 5 7 8 9 hoidmv1lelem1 φ S U A U x y U y x
65 64 simp1d φ S U
66 63 65 sseldi φ S A B
67 61 66 sseldd φ S
68 67 rexrd φ S *
69 simpl φ ¬ B S φ
70 simpr φ ¬ B S ¬ B S
71 69 67 syl φ ¬ B S S
72 69 2 syl φ ¬ B S B
73 71 72 ltnled φ ¬ B S S < B ¬ B S
74 70 73 mpbird φ ¬ B S S < B
75 6 adantr φ S < B A B j C j D j
76 1 rexrd φ A *
77 76 adantr φ S < B A *
78 60 adantr φ S < B B *
79 68 adantr φ S < B S *
80 63 61 sstrid φ U
81 65 ne0d φ U
82 64 simp3d φ x y U y x
83 64 simp2d φ A U
84 suprub U U x y U y x A U A sup U <
85 80 81 82 83 84 syl31anc φ A sup U <
86 85 9 breqtrrdi φ A S
87 86 adantr φ S < B A S
88 simpr φ S < B S < B
89 77 78 79 87 88 elicod φ S < B S A B
90 75 89 sseldd φ S < B S j C j D j
91 eliun S j C j D j j S C j D j
92 90 91 sylib φ S < B j S C j D j
93 1 adantr φ S < B A
94 93 3ad2ant1 φ S < B j S C j D j A
95 2 adantr φ S < B B
96 95 3ad2ant1 φ S < B j S C j D j B
97 4 adantr φ S < B C :
98 97 3ad2ant1 φ S < B j S C j D j C :
99 5 adantr φ S < B D :
100 99 3ad2ant1 φ S < B j S C j D j D :
101 fveq2 i = j C i = C j
102 fveq2 i = j D i = D j
103 101 102 oveq12d i = j C i D i = C j D j
104 103 fveq2d i = j vol C i D i = vol C j D j
105 104 cbvmptv i vol C i D i = j vol C j D j
106 105 fveq2i sum^ i vol C i D i = sum^ j vol C j D j
107 106 7 eqeltrid φ sum^ i vol C i D i
108 107 adantr φ S < B sum^ i vol C i D i
109 108 3ad2ant1 φ S < B j S C j D j sum^ i vol C i D i
110 102 breq1d i = j D i z D j z
111 110 102 ifbieq1d i = j if D i z D i z = if D j z D j z
112 101 111 oveq12d i = j C i if D i z D i z = C j if D j z D j z
113 112 fveq2d i = j vol C i if D i z D i z = vol C j if D j z D j z
114 113 cbvmptv i vol C i if D i z D i z = j vol C j if D j z D j z
115 114 eqcomi j vol C j if D j z D j z = i vol C i if D i z D i z
116 115 fveq2i sum^ j vol C j if D j z D j z = sum^ i vol C i if D i z D i z
117 116 breq2i z A sum^ j vol C j if D j z D j z z A sum^ i vol C i if D i z D i z
118 117 rabbii z A B | z A sum^ j vol C j if D j z D j z = z A B | z A sum^ i vol C i if D i z D i z
119 8 118 eqtri U = z A B | z A sum^ i vol C i if D i z D i z
120 65 adantr φ S < B S U
121 120 3ad2ant1 φ S < B j S C j D j S U
122 87 3ad2ant1 φ S < B j S C j D j A S
123 88 3ad2ant1 φ S < B j S C j D j S < B
124 simp2 φ S < B j S C j D j j
125 simp3 φ S < B j S C j D j S C j D j
126 eqid if D j B D j B = if D j B D j B
127 94 96 98 100 109 119 121 122 123 124 125 126 hoidmv1lelem2 φ S < B j S C j D j u U S < u
128 127 3exp φ S < B j S C j D j u U S < u
129 128 rexlimdv φ S < B j S C j D j u U S < u
130 92 129 mpd φ S < B u U S < u
131 69 74 130 syl2anc φ ¬ B S u U S < u
132 61 adantr φ u U A B
133 63 132 sstrid φ u U U
134 81 adantr φ u U U
135 1 2 jca φ A B
136 135 adantr φ u U A B
137 63 a1i φ u U U A B
138 65 adantr φ u U S U
139 iccsupr A B U A B S U U U x y U y x
140 136 137 138 139 syl3anc φ u U U U x y U y x
141 140 simp3d φ u U x y U y x
142 simpr φ u U u U
143 suprub U U x y U y x u U u sup U <
144 133 134 141 142 143 syl31anc φ u U u sup U <
145 144 9 breqtrrdi φ u U u S
146 145 ralrimiva φ u U u S
147 63 sseli u U u A B
148 147 adantl φ u U u A B
149 132 148 sseldd φ u U u
150 67 adantr φ u U S
151 149 150 lenltd φ u U u S ¬ S < u
152 151 ralbidva φ u U u S u U ¬ S < u
153 146 152 mpbid φ u U ¬ S < u
154 ralnex u U ¬ S < u ¬ u U S < u
155 153 154 sylib φ ¬ u U S < u
156 155 adantr φ ¬ B S ¬ u U S < u
157 131 156 condan φ B S
158 iccleub A * B * S A B S B
159 76 60 66 158 syl3anc φ S B
160 60 68 157 159 xrletrid φ B = S
161 160 65 eqeltrd φ B U
162 161 8 eleqtrdi φ B z A B | z A sum^ j vol C j if D j z D j z
163 oveq1 z = B z A = B A
164 breq2 z = B D j z D j B
165 id z = B z = B
166 164 165 ifbieq2d z = B if D j z D j z = if D j B D j B
167 166 oveq2d z = B C j if D j z D j z = C j if D j B D j B
168 167 fveq2d z = B vol C j if D j z D j z = vol C j if D j B D j B
169 168 mpteq2dv z = B j vol C j if D j z D j z = j vol C j if D j B D j B
170 169 fveq2d z = B sum^ j vol C j if D j z D j z = sum^ j vol C j if D j B D j B
171 163 170 breq12d z = B z A sum^ j vol C j if D j z D j z B A sum^ j vol C j if D j B D j B
172 171 elrab B z A B | z A sum^ j vol C j if D j z D j z B A B B A sum^ j vol C j if D j B D j B
173 162 172 sylib φ B A B B A sum^ j vol C j if D j B D j B
174 173 simprd φ B A sum^ j vol C j if D j B D j B
175 10 59 7 174 53 letrd φ B A sum^ j vol C j D j