Metamath Proof Explorer


Theorem sxbrsigalem2

Description: The sigma-algebra generated by the dyadic closed-below, open-above rectangular subsets of ( RR X. RR ) is a subset of the sigma-algebra generated by the closed half-spaces of ( RR X. RR ) . The proof goes by noting the fact that the dyadic rectangles are intersections of a 'vertical band' and an 'horizontal band', which themselves are differences of closed half-spaces. (Contributed by Thierry Arnoux, 17-Sep-2017)

Ref Expression
Hypotheses sxbrsiga.0 J = topGen ran .
dya2ioc.1 I = x , n x 2 n x + 1 2 n
dya2ioc.2 R = u ran I , v ran I u × v
Assertion sxbrsigalem2 𝛔 ran R 𝛔 ran e e +∞ × ran f × f +∞

Proof

Step Hyp Ref Expression
1 sxbrsiga.0 J = topGen ran .
2 dya2ioc.1 I = x , n x 2 n x + 1 2 n
3 dya2ioc.2 R = u ran I , v ran I u × v
4 1 2 3 dya2iocucvr ran R = 2
5 sxbrsigalem0 ran e e +∞ × ran f × f +∞ = 2
6 4 5 eqtr4i ran R = ran e e +∞ × ran f × f +∞
7 vex u V
8 vex v V
9 7 8 xpex u × v V
10 3 9 elrnmpo d ran R u ran I v ran I d = u × v
11 simpr u ran I v ran I d = u × v d = u × v
12 1 2 dya2icobrsiga ran I 𝔅
13 brsigasspwrn 𝔅 𝒫
14 12 13 sstri ran I 𝒫
15 14 sseli u ran I u 𝒫
16 15 elpwid u ran I u
17 14 sseli v ran I v 𝒫
18 17 elpwid v ran I v
19 xpinpreima2 u v u × v = 1 st 2 -1 u 2 nd 2 -1 v
20 16 18 19 syl2an u ran I v ran I u × v = 1 st 2 -1 u 2 nd 2 -1 v
21 reex V
22 21 mptex e e +∞ × V
23 22 rnex ran e e +∞ × V
24 21 mptex f × f +∞ V
25 24 rnex ran f × f +∞ V
26 23 25 unex ran e e +∞ × ran f × f +∞ V
27 26 a1i ran e e +∞ × ran f × f +∞ V
28 27 sgsiga 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra
29 28 mptru 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra
30 29 a1i u ran I v ran I 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra
31 1stpreima u 1 st 2 -1 u = u ×
32 16 31 syl u ran I 1 st 2 -1 u = u ×
33 ovex x 2 n x + 1 2 n V
34 2 33 elrnmpo u ran I x n u = x 2 n x + 1 2 n
35 simpr x n u = x 2 n x + 1 2 n u = x 2 n x + 1 2 n
36 35 xpeq1d x n u = x 2 n x + 1 2 n u × = x 2 n x + 1 2 n ×
37 simpl x n x
38 37 zred x n x
39 2rp 2 +
40 39 a1i x n 2 +
41 simpr x n n
42 40 41 rpexpcld x n 2 n +
43 38 42 rerpdivcld x n x 2 n
44 43 rexrd x n x 2 n *
45 1red x n 1
46 38 45 readdcld x n x + 1
47 46 42 rerpdivcld x n x + 1 2 n
48 47 rexrd x n x + 1 2 n *
49 pnfxr +∞ *
50 49 a1i x n +∞ *
51 38 lep1d x n x x + 1
52 38 46 42 51 lediv1dd x n x 2 n x + 1 2 n
53 pnfge x + 1 2 n * x + 1 2 n +∞
54 48 53 syl x n x + 1 2 n +∞
55 difico x 2 n * x + 1 2 n * +∞ * x 2 n x + 1 2 n x + 1 2 n +∞ x 2 n +∞ x + 1 2 n +∞ = x 2 n x + 1 2 n
56 44 48 50 52 54 55 syl32anc x n x 2 n +∞ x + 1 2 n +∞ = x 2 n x + 1 2 n
57 56 xpeq1d x n x 2 n +∞ x + 1 2 n +∞ × = x 2 n x + 1 2 n ×
58 difxp1 x 2 n +∞ x + 1 2 n +∞ × = x 2 n +∞ × x + 1 2 n +∞ ×
59 57 58 eqtr3di x n x 2 n x + 1 2 n × = x 2 n +∞ × x + 1 2 n +∞ ×
60 29 a1i x n 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra
61 ssun1 ran e e +∞ × ran e e +∞ × ran f × f +∞
62 eqid x 2 n +∞ × = x 2 n +∞ ×
63 oveq1 e = x 2 n e +∞ = x 2 n +∞
64 63 xpeq1d e = x 2 n e +∞ × = x 2 n +∞ ×
65 64 rspceeqv x 2 n x 2 n +∞ × = x 2 n +∞ × e x 2 n +∞ × = e +∞ ×
66 43 62 65 sylancl x n e x 2 n +∞ × = e +∞ ×
67 eqid e e +∞ × = e e +∞ ×
68 ovex e +∞ V
69 68 21 xpex e +∞ × V
70 67 69 elrnmpti x 2 n +∞ × ran e e +∞ × e x 2 n +∞ × = e +∞ ×
71 66 70 sylibr x n x 2 n +∞ × ran e e +∞ ×
72 61 71 sselid x n x 2 n +∞ × ran e e +∞ × ran f × f +∞
73 elsigagen ran e e +∞ × ran f × f +∞ V x 2 n +∞ × ran e e +∞ × ran f × f +∞ x 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
74 26 72 73 sylancr x n x 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
75 eqid x + 1 2 n +∞ × = x + 1 2 n +∞ ×
76 oveq1 e = x + 1 2 n e +∞ = x + 1 2 n +∞
77 76 xpeq1d e = x + 1 2 n e +∞ × = x + 1 2 n +∞ ×
78 77 rspceeqv x + 1 2 n x + 1 2 n +∞ × = x + 1 2 n +∞ × e x + 1 2 n +∞ × = e +∞ ×
79 47 75 78 sylancl x n e x + 1 2 n +∞ × = e +∞ ×
80 67 69 elrnmpti x + 1 2 n +∞ × ran e e +∞ × e x + 1 2 n +∞ × = e +∞ ×
81 79 80 sylibr x n x + 1 2 n +∞ × ran e e +∞ ×
82 61 81 sselid x n x + 1 2 n +∞ × ran e e +∞ × ran f × f +∞
83 elsigagen ran e e +∞ × ran f × f +∞ V x + 1 2 n +∞ × ran e e +∞ × ran f × f +∞ x + 1 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
84 26 82 83 sylancr x n x + 1 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
85 difelsiga 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra x 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞ x + 1 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞ x 2 n +∞ × x + 1 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
86 60 74 84 85 syl3anc x n x 2 n +∞ × x + 1 2 n +∞ × 𝛔 ran e e +∞ × ran f × f +∞
87 59 86 eqeltrd x n x 2 n x + 1 2 n × 𝛔 ran e e +∞ × ran f × f +∞
88 87 adantr x n u = x 2 n x + 1 2 n x 2 n x + 1 2 n × 𝛔 ran e e +∞ × ran f × f +∞
89 36 88 eqeltrd x n u = x 2 n x + 1 2 n u × 𝛔 ran e e +∞ × ran f × f +∞
90 89 ex x n u = x 2 n x + 1 2 n u × 𝛔 ran e e +∞ × ran f × f +∞
91 90 rexlimivv x n u = x 2 n x + 1 2 n u × 𝛔 ran e e +∞ × ran f × f +∞
92 34 91 sylbi u ran I u × 𝛔 ran e e +∞ × ran f × f +∞
93 32 92 eqeltrd u ran I 1 st 2 -1 u 𝛔 ran e e +∞ × ran f × f +∞
94 93 adantr u ran I v ran I 1 st 2 -1 u 𝛔 ran e e +∞ × ran f × f +∞
95 2ndpreima v 2 nd 2 -1 v = × v
96 18 95 syl v ran I 2 nd 2 -1 v = × v
97 2 33 elrnmpo v ran I x n v = x 2 n x + 1 2 n
98 simpr x n v = x 2 n x + 1 2 n v = x 2 n x + 1 2 n
99 98 xpeq2d x n v = x 2 n x + 1 2 n × v = × x 2 n x + 1 2 n
100 56 xpeq2d x n × x 2 n +∞ x + 1 2 n +∞ = × x 2 n x + 1 2 n
101 difxp2 × x 2 n +∞ x + 1 2 n +∞ = × x 2 n +∞ × x + 1 2 n +∞
102 100 101 eqtr3di x n × x 2 n x + 1 2 n = × x 2 n +∞ × x + 1 2 n +∞
103 ssun2 ran f × f +∞ ran e e +∞ × ran f × f +∞
104 eqid × x 2 n +∞ = × x 2 n +∞
105 oveq1 f = x 2 n f +∞ = x 2 n +∞
106 105 xpeq2d f = x 2 n × f +∞ = × x 2 n +∞
107 106 rspceeqv x 2 n × x 2 n +∞ = × x 2 n +∞ f × x 2 n +∞ = × f +∞
108 43 104 107 sylancl x n f × x 2 n +∞ = × f +∞
109 eqid f × f +∞ = f × f +∞
110 ovex f +∞ V
111 21 110 xpex × f +∞ V
112 109 111 elrnmpti × x 2 n +∞ ran f × f +∞ f × x 2 n +∞ = × f +∞
113 108 112 sylibr x n × x 2 n +∞ ran f × f +∞
114 103 113 sselid x n × x 2 n +∞ ran e e +∞ × ran f × f +∞
115 elsigagen ran e e +∞ × ran f × f +∞ V × x 2 n +∞ ran e e +∞ × ran f × f +∞ × x 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
116 26 114 115 sylancr x n × x 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
117 eqid × x + 1 2 n +∞ = × x + 1 2 n +∞
118 oveq1 f = x + 1 2 n f +∞ = x + 1 2 n +∞
119 118 xpeq2d f = x + 1 2 n × f +∞ = × x + 1 2 n +∞
120 119 rspceeqv x + 1 2 n × x + 1 2 n +∞ = × x + 1 2 n +∞ f × x + 1 2 n +∞ = × f +∞
121 47 117 120 sylancl x n f × x + 1 2 n +∞ = × f +∞
122 109 111 elrnmpti × x + 1 2 n +∞ ran f × f +∞ f × x + 1 2 n +∞ = × f +∞
123 121 122 sylibr x n × x + 1 2 n +∞ ran f × f +∞
124 103 123 sselid x n × x + 1 2 n +∞ ran e e +∞ × ran f × f +∞
125 elsigagen ran e e +∞ × ran f × f +∞ V × x + 1 2 n +∞ ran e e +∞ × ran f × f +∞ × x + 1 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
126 26 124 125 sylancr x n × x + 1 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
127 difelsiga 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra × x 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞ × x + 1 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞ × x 2 n +∞ × x + 1 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
128 60 116 126 127 syl3anc x n × x 2 n +∞ × x + 1 2 n +∞ 𝛔 ran e e +∞ × ran f × f +∞
129 102 128 eqeltrd x n × x 2 n x + 1 2 n 𝛔 ran e e +∞ × ran f × f +∞
130 129 adantr x n v = x 2 n x + 1 2 n × x 2 n x + 1 2 n 𝛔 ran e e +∞ × ran f × f +∞
131 99 130 eqeltrd x n v = x 2 n x + 1 2 n × v 𝛔 ran e e +∞ × ran f × f +∞
132 131 ex x n v = x 2 n x + 1 2 n × v 𝛔 ran e e +∞ × ran f × f +∞
133 132 rexlimivv x n v = x 2 n x + 1 2 n × v 𝛔 ran e e +∞ × ran f × f +∞
134 97 133 sylbi v ran I × v 𝛔 ran e e +∞ × ran f × f +∞
135 96 134 eqeltrd v ran I 2 nd 2 -1 v 𝛔 ran e e +∞ × ran f × f +∞
136 135 adantl u ran I v ran I 2 nd 2 -1 v 𝛔 ran e e +∞ × ran f × f +∞
137 inelsiga 𝛔 ran e e +∞ × ran f × f +∞ ran sigAlgebra 1 st 2 -1 u 𝛔 ran e e +∞ × ran f × f +∞ 2 nd 2 -1 v 𝛔 ran e e +∞ × ran f × f +∞ 1 st 2 -1 u 2 nd 2 -1 v 𝛔 ran e e +∞ × ran f × f +∞
138 30 94 136 137 syl3anc u ran I v ran I 1 st 2 -1 u 2 nd 2 -1 v 𝛔 ran e e +∞ × ran f × f +∞
139 20 138 eqeltrd u ran I v ran I u × v 𝛔 ran e e +∞ × ran f × f +∞
140 139 adantr u ran I v ran I d = u × v u × v 𝛔 ran e e +∞ × ran f × f +∞
141 11 140 eqeltrd u ran I v ran I d = u × v d 𝛔 ran e e +∞ × ran f × f +∞
142 141 ex u ran I v ran I d = u × v d 𝛔 ran e e +∞ × ran f × f +∞
143 142 rexlimivv u ran I v ran I d = u × v d 𝛔 ran e e +∞ × ran f × f +∞
144 10 143 sylbi d ran R d 𝛔 ran e e +∞ × ran f × f +∞
145 144 ssriv ran R 𝛔 ran e e +∞ × ran f × f +∞
146 sigagenss2 ran R = ran e e +∞ × ran f × f +∞ ran R 𝛔 ran e e +∞ × ran f × f +∞ ran e e +∞ × ran f × f +∞ V 𝛔 ran R 𝛔 ran e e +∞ × ran f × f +∞
147 6 145 26 146 mp3an 𝛔 ran R 𝛔 ran e e +∞ × ran f × f +∞