Metamath Proof Explorer


Theorem hoicvrrex

Description: Any subset of the multidimensional reals can be covered by a countable set of half-open intervals, see Definition 115A (b) of Fremlin1 p. 29. (Contributed by Glauco Siliprandi, 11-Oct-2020)

Ref Expression
Hypotheses hoicvrrex.fi φ X Fin
hoicvrrex.y φ Y X
Assertion hoicvrrex φ i 2 X Y j k X . i j k +∞ = sum^ j k X vol . i j k

Proof

Step Hyp Ref Expression
1 hoicvrrex.fi φ X Fin
2 hoicvrrex.y φ Y X
3 nnre j j
4 3 renegcld j j
5 opelxpi j j j j 2
6 4 3 5 syl2anc j j j 2
7 6 ad2antlr φ j k X j j 2
8 eqid k X j j = k X j j
9 7 8 fmptd φ j k X j j : X 2
10 reex V
11 10 10 xpex 2 V
12 11 a1i φ 2 V
13 elmapg 2 V X Fin k X j j 2 X k X j j : X 2
14 12 1 13 syl2anc φ k X j j 2 X k X j j : X 2
15 14 adantr φ j k X j j 2 X k X j j : X 2
16 9 15 mpbird φ j k X j j 2 X
17 eqid j k X j j = j k X j j
18 16 17 fmptd φ j k X j j : 2 X
19 ovex 2 X V
20 nnex V
21 19 20 elmap j k X j j 2 X j k X j j : 2 X
22 18 21 sylibr φ j k X j j 2 X
23 eqid j l X j j = j l X j j
24 23 1 hoicvr φ X j k X . j l X j j j k
25 eqidd l = k j j = j j
26 25 cbvmptv l X j j = k X j j
27 26 mpteq2i j l X j j = j k X j j
28 27 a1i φ j l X j j = j k X j j
29 28 fveq1d φ j l X j j j = j k X j j j
30 29 coeq2d φ . j l X j j j = . j k X j j j
31 30 fveq1d φ . j l X j j j k = . j k X j j j k
32 31 ixpeq2dv φ k X . j l X j j j k = k X . j k X j j j k
33 32 iuneq2d φ j k X . j l X j j j k = j k X . j k X j j j k
34 24 33 sseqtrd φ X j k X . j k X j j j k
35 2 34 sstrd φ Y j k X . j k X j j j k
36 simpr φ j j
37 16 elexd φ j k X j j V
38 17 fvmpt2 j k X j j V j k X j j j = k X j j
39 36 37 38 syl2anc φ j j k X j j j = k X j j
40 39 7 fmpt3d φ j j k X j j j : X 2
41 40 adantr φ j k X j k X j j j : X 2
42 simpr φ j k X k X
43 41 42 fvovco φ j k X . j k X j j j k = 1 st j k X j j j k 2 nd j k X j j j k
44 39 fveq1d φ j j k X j j j k = k X j j k
45 44 adantr φ j k X j k X j j j k = k X j j k
46 simpr φ k X k X
47 opex j j V
48 47 a1i φ k X j j V
49 8 fvmpt2 k X j j V k X j j k = j j
50 46 48 49 syl2anc φ k X k X j j k = j j
51 50 adantlr φ j k X k X j j k = j j
52 45 51 eqtrd φ j k X j k X j j j k = j j
53 52 fveq2d φ j k X 1 st j k X j j j k = 1 st j j
54 negex j V
55 vex j V
56 54 55 op1st 1 st j j = j
57 56 a1i φ j k X 1 st j j = j
58 53 57 eqtrd φ j k X 1 st j k X j j j k = j
59 52 fveq2d φ j k X 2 nd j k X j j j k = 2 nd j j
60 54 55 op2nd 2 nd j j = j
61 60 a1i φ j k X 2 nd j j = j
62 59 61 eqtrd φ j k X 2 nd j k X j j j k = j
63 58 62 oveq12d φ j k X 1 st j k X j j j k 2 nd j k X j j j k = j j
64 43 63 eqtrd φ j k X . j k X j j j k = j j
65 64 fveq2d φ j k X vol . j k X j j j k = vol j j
66 volico j j vol j j = if j < j j j 0
67 4 3 66 syl2anc j vol j j = if j < j j j 0
68 nnrp j j +
69 neglt j + j < j
70 68 69 syl j j < j
71 70 iftrued j if j < j j j 0 = j j
72 3 recnd j j
73 72 72 subnegd j j j = j + j
74 72 2timesd j 2 j = j + j
75 73 74 eqtr4d j j j = 2 j
76 67 71 75 3eqtrd j vol j j = 2 j
77 76 ad2antlr φ j k X vol j j = 2 j
78 65 77 eqtrd φ j k X vol . j k X j j j k = 2 j
79 78 prodeq2dv φ j k X vol . j k X j j j k = k X 2 j
80 1 adantr φ j X Fin
81 2cnd φ j 2
82 72 adantl φ j j
83 81 82 mulcld φ j 2 j
84 fprodconst X Fin 2 j k X 2 j = 2 j X
85 80 83 84 syl2anc φ j k X 2 j = 2 j X
86 79 85 eqtrd φ j k X vol . j k X j j j k = 2 j X
87 86 mpteq2dva φ j k X vol . j k X j j j k = j 2 j X
88 87 fveq2d φ sum^ j k X vol . j k X j j j k = sum^ j 2 j X
89 20 a1i φ V
90 68 ssriv +
91 ioorp 0 +∞ = +
92 91 eqcomi + = 0 +∞
93 90 92 sseqtri 0 +∞
94 ioossicc 0 +∞ 0 +∞
95 93 94 sstri 0 +∞
96 2nn 2
97 96 a1i φ j 2
98 97 36 nnmulcld φ j 2 j
99 hashcl X Fin X 0
100 1 99 syl φ X 0
101 100 adantr φ j X 0
102 nnexpcl 2 j X 0 2 j X
103 98 101 102 syl2anc φ j 2 j X
104 95 103 sseldi φ j 2 j X 0 +∞
105 eqid j 2 j X = j 2 j X
106 104 105 fmptd φ j 2 j X : 0 +∞
107 89 106 sge0xrcl φ sum^ j 2 j X *
108 pnfxr +∞ *
109 108 a1i φ +∞ *
110 1nn 1
111 95 110 sselii 1 0 +∞
112 111 a1i φ j 1 0 +∞
113 eqid j 1 = j 1
114 112 113 fmptd φ j 1 : 0 +∞
115 89 114 sge0xrcl φ sum^ j 1 *
116 nnnfi ¬ Fin
117 116 a1i φ ¬ Fin
118 1rp 1 +
119 118 a1i φ 1 +
120 89 117 119 sge0rpcpnf φ sum^ j 1 = +∞
121 120 eqcomd φ +∞ = sum^ j 1
122 109 121 xreqled φ +∞ sum^ j 1
123 nfv j φ
124 114 fvmptelrn φ j 1 0 +∞
125 103 nnge1d φ j 1 2 j X
126 123 89 124 104 125 sge0lempt φ sum^ j 1 sum^ j 2 j X
127 109 115 107 122 126 xrletrd φ +∞ sum^ j 2 j X
128 107 127 xrgepnfd φ sum^ j 2 j X = +∞
129 eqidd φ +∞ = +∞
130 88 128 129 3eqtrrd φ +∞ = sum^ j k X vol . j k X j j j k
131 35 130 jca φ Y j k X . j k X j j j k +∞ = sum^ j k X vol . j k X j j j k
132 nfcv _ j i
133 nfmpt1 _ j j k X j j
134 132 133 nfeq j i = j k X j j
135 nfcv _ k i
136 nfcv _ k
137 nfmpt1 _ k k X j j
138 136 137 nfmpt _ k j k X j j
139 135 138 nfeq k i = j k X j j
140 fveq1 i = j k X j j i j = j k X j j j
141 140 coeq2d i = j k X j j . i j = . j k X j j j
142 141 fveq1d i = j k X j j . i j k = . j k X j j j k
143 142 adantr i = j k X j j k X . i j k = . j k X j j j k
144 139 143 ixpeq2d i = j k X j j k X . i j k = k X . j k X j j j k
145 144 adantr i = j k X j j j k X . i j k = k X . j k X j j j k
146 134 145 iuneq2df i = j k X j j j k X . i j k = j k X . j k X j j j k
147 146 sseq2d i = j k X j j Y j k X . i j k Y j k X . j k X j j j k
148 142 fveq2d i = j k X j j vol . i j k = vol . j k X j j j k
149 148 a1d i = j k X j j k X vol . i j k = vol . j k X j j j k
150 139 149 ralrimi i = j k X j j k X vol . i j k = vol . j k X j j j k
151 150 adantr i = j k X j j j k X vol . i j k = vol . j k X j j j k
152 151 prodeq2d i = j k X j j j k X vol . i j k = k X vol . j k X j j j k
153 134 152 mpteq2da i = j k X j j j k X vol . i j k = j k X vol . j k X j j j k
154 153 fveq2d i = j k X j j sum^ j k X vol . i j k = sum^ j k X vol . j k X j j j k
155 154 eqeq2d i = j k X j j +∞ = sum^ j k X vol . i j k +∞ = sum^ j k X vol . j k X j j j k
156 147 155 anbi12d i = j k X j j Y j k X . i j k +∞ = sum^ j k X vol . i j k Y j k X . j k X j j j k +∞ = sum^ j k X vol . j k X j j j k
157 156 rspcev j k X j j 2 X Y j k X . j k X j j j k +∞ = sum^ j k X vol . j k X j j j k i 2 X Y j k X . i j k +∞ = sum^ j k X vol . i j k
158 22 131 157 syl2anc φ i 2 X Y j k X . i j k +∞ = sum^ j k X vol . i j k