Step | Hyp | Ref
| Expression |
1 | | sibfof.1 |
. . . . . . . 8
|
2 | | sibfof.0 |
. . . . . . . . . . 11
|
3 | | sitgval.b |
. . . . . . . . . . . 12
|
4 | | sitgval.j |
. . . . . . . . . . . 12
|
5 | 3, 4 | tpsuni 20740 |
. . . . . . . . . . 11
|
6 | 2, 5 | syl 17 |
. . . . . . . . . 10
|
7 | 6 | sqxpeqd 5141 |
. . . . . . . . 9
|
8 | 7 | feq2d 6031 |
. . . . . . . 8
|
9 | 1, 8 | mpbid 222 |
. . . . . . 7
|
10 | 9 | fovrnda 6805 |
. . . . . 6
|
11 | | sitgval.s |
. . . . . . 7
sigaGen |
12 | | sitgval.0 |
. . . . . . 7
|
13 | | sitgval.x |
. . . . . . 7
|
14 | | sitgval.h |
. . . . . . 7
RRHomScalar |
15 | | sitgval.1 |
. . . . . . 7
|
16 | | sitgval.2 |
. . . . . . 7
measures |
17 | | sibfmbl.1 |
. . . . . . 7
sitg |
18 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibff 30398 |
. . . . . 6
|
19 | | sibfof.2 |
. . . . . . 7
sitg |
20 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibff 30398 |
. . . . . 6
|
21 | | dmexg 7097 |
. . . . . . 7
measures |
22 | | uniexg 6955 |
. . . . . . 7
|
23 | 16, 21, 22 | 3syl 18 |
. . . . . 6
|
24 | | inidm 3822 |
. . . . . 6
|
25 | 10, 18, 20, 23, 23, 24 | off 6912 |
. . . . 5
|
26 | | sibfof.3 |
. . . . . . . 8
|
27 | | sibfof.c |
. . . . . . . . 9
|
28 | | eqid 2622 |
. . . . . . . . 9
|
29 | 27, 28 | tpsuni 20740 |
. . . . . . . 8
|
30 | 26, 29 | syl 17 |
. . . . . . 7
|
31 | | fvex 6201 |
. . . . . . . 8
|
32 | | unisg 30206 |
. . . . . . . 8
sigaGen |
33 | 31, 32 | ax-mp 5 |
. . . . . . 7
sigaGen |
34 | 30, 33 | syl6eqr 2674 |
. . . . . 6
sigaGen |
35 | 34 | feq3d 6032 |
. . . . 5
sigaGen |
36 | 25, 35 | mpbid 222 |
. . . 4
sigaGen |
37 | 31 | a1i 11 |
. . . . . . 7
|
38 | 37 | sgsiga 30205 |
. . . . . 6
sigaGen sigAlgebra |
39 | | uniexg 6955 |
. . . . . 6
sigaGen sigAlgebra sigaGen |
40 | 38, 39 | syl 17 |
. . . . 5
sigaGen |
41 | 40, 23 | elmapd 7871 |
. . . 4
sigaGen sigaGen |
42 | 36, 41 | mpbird 247 |
. . 3
sigaGen |
43 | | inundif 4046 |
. . . . . . 7
|
44 | 43 | imaeq2i 5464 |
. . . . . 6
|
45 | | ffun 6048 |
. . . . . . . 8
|
46 | | unpreima 6341 |
. . . . . . . 8
|
47 | 25, 45, 46 | 3syl 18 |
. . . . . . 7
|
48 | 47 | adantr 481 |
. . . . . 6
sigaGen
|
49 | 44, 48 | syl5eqr 2670 |
. . . . 5
sigaGen
|
50 | | dmmeas 30264 |
. . . . . . . 8
measures sigAlgebra |
51 | 16, 50 | syl 17 |
. . . . . . 7
sigAlgebra |
52 | 51 | adantr 481 |
. . . . . 6
sigaGen sigAlgebra |
53 | | imaiun 6503 |
. . . . . . . 8
|
54 | | iunid 4575 |
. . . . . . . . 9
|
55 | 54 | imaeq2i 5464 |
. . . . . . . 8
|
56 | 53, 55 | eqtr3i 2646 |
. . . . . . 7
|
57 | | inss2 3834 |
. . . . . . . . . 10
|
58 | 6 | feq3d 6032 |
. . . . . . . . . . . . . . 15
|
59 | 18, 58 | mpbird 247 |
. . . . . . . . . . . . . 14
|
60 | 6 | feq3d 6032 |
. . . . . . . . . . . . . . 15
|
61 | 20, 60 | mpbird 247 |
. . . . . . . . . . . . . 14
|
62 | | ffn 6045 |
. . . . . . . . . . . . . . 15
|
63 | 1, 62 | syl 17 |
. . . . . . . . . . . . . 14
|
64 | 59, 61, 23, 63 | ofpreima2 29466 |
. . . . . . . . . . . . 13
|
65 | 64 | adantr 481 |
. . . . . . . . . . . 12
|
66 | 51 | adantr 481 |
. . . . . . . . . . . . 13
sigAlgebra |
67 | 51 | ad2antrr 762 |
. . . . . . . . . . . . . . 15
sigAlgebra |
68 | | simpll 790 |
. . . . . . . . . . . . . . . 16
|
69 | | inss1 3833 |
. . . . . . . . . . . . . . . . . 18
|
70 | | cnvimass 5485 |
. . . . . . . . . . . . . . . . . . . 20
|
71 | | fdm 6051 |
. . . . . . . . . . . . . . . . . . . . 21
|
72 | 1, 71 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
|
73 | 70, 72 | syl5sseq 3653 |
. . . . . . . . . . . . . . . . . . 19
|
74 | 73 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
|
75 | 69, 74 | syl5ss 3614 |
. . . . . . . . . . . . . . . . 17
|
76 | 75 | sselda 3603 |
. . . . . . . . . . . . . . . 16
|
77 | 51 | adantr 481 |
. . . . . . . . . . . . . . . . 17
sigAlgebra |
78 | | sibfof.4 |
. . . . . . . . . . . . . . . . . . . 20
|
79 | 78 | sgsiga 30205 |
. . . . . . . . . . . . . . . . . . 19
sigaGen
sigAlgebra |
80 | 11, 79 | syl5eqel 2705 |
. . . . . . . . . . . . . . . . . 18
sigAlgebra |
81 | 80 | adantr 481 |
. . . . . . . . . . . . . . . . 17
sigAlgebra |
82 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfmbl 30397 |
. . . . . . . . . . . . . . . . . 18
MblFnM |
83 | 82 | adantr 481 |
. . . . . . . . . . . . . . . . 17
MblFnM |
84 | 4 | tpstop 20741 |
. . . . . . . . . . . . . . . . . . . . 21
|
85 | | cldssbrsiga 30250 |
. . . . . . . . . . . . . . . . . . . . 21
sigaGen |
86 | 2, 84, 85 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . 20
sigaGen |
87 | 86 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
sigaGen |
88 | 78 | adantr 481 |
. . . . . . . . . . . . . . . . . . . 20
|
89 | | xp1st 7198 |
. . . . . . . . . . . . . . . . . . . . . 22
|
90 | 89 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
91 | 6 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . 21
|
92 | 90, 91 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
|
93 | | eqid 2622 |
. . . . . . . . . . . . . . . . . . . . 21
|
94 | 93 | t1sncld 21130 |
. . . . . . . . . . . . . . . . . . . 20
|
95 | 88, 92, 94 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
96 | 87, 95 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
sigaGen |
97 | 96, 11 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
|
98 | 77, 81, 83, 97 | mbfmcnvima 30319 |
. . . . . . . . . . . . . . . 16
|
99 | 68, 76, 98 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
100 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfmbl 30397 |
. . . . . . . . . . . . . . . . . 18
MblFnM |
101 | 100 | adantr 481 |
. . . . . . . . . . . . . . . . 17
MblFnM |
102 | | xp2nd 7199 |
. . . . . . . . . . . . . . . . . . . . . 22
|
103 | 102 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
|
104 | 103, 91 | eleqtrd 2703 |
. . . . . . . . . . . . . . . . . . . 20
|
105 | 93 | t1sncld 21130 |
. . . . . . . . . . . . . . . . . . . 20
|
106 | 88, 104, 105 | syl2anc 693 |
. . . . . . . . . . . . . . . . . . 19
|
107 | 87, 106 | sseldd 3604 |
. . . . . . . . . . . . . . . . . 18
sigaGen |
108 | 107, 11 | syl6eleqr 2712 |
. . . . . . . . . . . . . . . . 17
|
109 | 77, 81, 101, 108 | mbfmcnvima 30319 |
. . . . . . . . . . . . . . . 16
|
110 | 68, 76, 109 | syl2anc 693 |
. . . . . . . . . . . . . . 15
|
111 | | inelsiga 30198 |
. . . . . . . . . . . . . . 15
sigAlgebra
|
112 | 67, 99, 110, 111 | syl3anc 1326 |
. . . . . . . . . . . . . 14
|
113 | 112 | ralrimiva 2966 |
. . . . . . . . . . . . 13
|
114 | 3, 4, 11, 12, 13, 14, 15, 16, 17 | sibfrn 30399 |
. . . . . . . . . . . . . . . . 17
|
115 | 3, 4, 11, 12, 13, 14, 15, 16, 19 | sibfrn 30399 |
. . . . . . . . . . . . . . . . 17
|
116 | | xpfi 8231 |
. . . . . . . . . . . . . . . . 17
|
117 | 114, 115,
116 | syl2anc 693 |
. . . . . . . . . . . . . . . 16
|
118 | | inss2 3834 |
. . . . . . . . . . . . . . . 16
|
119 | | ssdomg 8001 |
. . . . . . . . . . . . . . . 16
|
120 | 117, 118,
119 | mpisyl 21 |
. . . . . . . . . . . . . . 15
|
121 | | isfinite 8549 |
. . . . . . . . . . . . . . . . 17
|
122 | 121 | biimpi 206 |
. . . . . . . . . . . . . . . 16
|
123 | | sdomdom 7983 |
. . . . . . . . . . . . . . . 16
|
124 | 117, 122,
123 | 3syl 18 |
. . . . . . . . . . . . . . 15
|
125 | | domtr 8009 |
. . . . . . . . . . . . . . 15
|
126 | 120, 124,
125 | syl2anc 693 |
. . . . . . . . . . . . . 14
|
127 | 126 | adantr 481 |
. . . . . . . . . . . . 13
|
128 | | nfcv 2764 |
. . . . . . . . . . . . . 14
|
129 | 128 | sigaclcuni 30181 |
. . . . . . . . . . . . 13
sigAlgebra |
130 | 66, 113, 127, 129 | syl3anc 1326 |
. . . . . . . . . . . 12
|
131 | 65, 130 | eqeltrd 2701 |
. . . . . . . . . . 11
|
132 | 131 | ralrimiva 2966 |
. . . . . . . . . 10
|
133 | | ssralv 3666 |
. . . . . . . . . 10
|
134 | 57, 132, 133 | mpsyl 68 |
. . . . . . . . 9
|
135 | 134 | adantr 481 |
. . . . . . . 8
sigaGen
|
136 | | ffun 6048 |
. . . . . . . . . . . . . 14
|
137 | 1, 136 | syl 17 |
. . . . . . . . . . . . 13
|
138 | | imafi 8259 |
. . . . . . . . . . . . 13
|
139 | 137, 117,
138 | syl2anc 693 |
. . . . . . . . . . . 12
|
140 | 18, 20, 9, 23 | ofrn2 29442 |
. . . . . . . . . . . 12
|
141 | | ssfi 8180 |
. . . . . . . . . . . 12
|
142 | 139, 140,
141 | syl2anc 693 |
. . . . . . . . . . 11
|
143 | | ssdomg 8001 |
. . . . . . . . . . 11
|
144 | 142, 57, 143 | mpisyl 21 |
. . . . . . . . . 10
|
145 | | isfinite 8549 |
. . . . . . . . . . . 12
|
146 | 142, 145 | sylib 208 |
. . . . . . . . . . 11
|
147 | | sdomdom 7983 |
. . . . . . . . . . 11
|
148 | 146, 147 | syl 17 |
. . . . . . . . . 10
|
149 | | domtr 8009 |
. . . . . . . . . 10
|
150 | 144, 148,
149 | syl2anc 693 |
. . . . . . . . 9
|
151 | 150 | adantr 481 |
. . . . . . . 8
sigaGen
|
152 | | nfcv 2764 |
. . . . . . . . 9
|
153 | 152 | sigaclcuni 30181 |
. . . . . . . 8
sigAlgebra
|
154 | 52, 135, 151, 153 | syl3anc 1326 |
. . . . . . 7
sigaGen
|
155 | 56, 154 | syl5eqelr 2706 |
. . . . . 6
sigaGen
|
156 | | difpreima 6343 |
. . . . . . . . . 10
|
157 | 25, 45, 156 | 3syl 18 |
. . . . . . . . 9
|
158 | | cnvimarndm 5486 |
. . . . . . . . . . 11
|
159 | 158 | difeq2i 3725 |
. . . . . . . . . 10
|
160 | | cnvimass 5485 |
. . . . . . . . . . 11
|
161 | | ssdif0 3942 |
. . . . . . . . . . 11
|
162 | 160, 161 | mpbi 220 |
. . . . . . . . . 10
|
163 | 159, 162 | eqtri 2644 |
. . . . . . . . 9
|
164 | 157, 163 | syl6eq 2672 |
. . . . . . . 8
|
165 | | 0elsiga 30177 |
. . . . . . . . 9
sigAlgebra |
166 | 16, 50, 165 | 3syl 18 |
. . . . . . . 8
|
167 | 164, 166 | eqeltrd 2701 |
. . . . . . 7
|
168 | 167 | adantr 481 |
. . . . . 6
sigaGen
|
169 | | unelsiga 30197 |
. . . . . 6
sigAlgebra
|
170 | 52, 155, 168, 169 | syl3anc 1326 |
. . . . 5
sigaGen
|
171 | 49, 170 | eqeltrd 2701 |
. . . 4
sigaGen |
172 | 171 | ralrimiva 2966 |
. . 3
sigaGen |
173 | 51, 38 | ismbfm 30314 |
. . 3
MblFnMsigaGen
sigaGen
sigaGen |
174 | 42, 172, 173 | mpbir2and 957 |
. 2
MblFnMsigaGen |
175 | 64 | adantr 481 |
. . . . . . 7
|
176 | 175 | fveq2d 6195 |
. . . . . 6
|
177 | | measbasedom 30265 |
. . . . . . . . 9
measures
measures |
178 | 16, 177 | sylib 208 |
. . . . . . . 8
measures |
179 | 178 | adantr 481 |
. . . . . . 7
measures |
180 | | eldifi 3732 |
. . . . . . . 8
|
181 | 180, 113 | sylan2 491 |
. . . . . . 7
|
182 | 126 | adantr 481 |
. . . . . . 7
|
183 | | sneq 4187 |
. . . . . . . . . . 11
|
184 | 183 | imaeq2d 5466 |
. . . . . . . . . 10
|
185 | | sneq 4187 |
. . . . . . . . . . 11
|
186 | 185 | imaeq2d 5466 |
. . . . . . . . . 10
|
187 | | ffun 6048 |
. . . . . . . . . . . 12
|
188 | 18, 187 | syl 17 |
. . . . . . . . . . 11
|
189 | | sndisj 4644 |
. . . . . . . . . . 11
Disj |
190 | | disjpreima 29397 |
. . . . . . . . . . 11
Disj Disj |
191 | 188, 189,
190 | sylancl 694 |
. . . . . . . . . 10
Disj
|
192 | | ffun 6048 |
. . . . . . . . . . . 12
|
193 | 20, 192 | syl 17 |
. . . . . . . . . . 11
|
194 | | sndisj 4644 |
. . . . . . . . . . 11
Disj |
195 | | disjpreima 29397 |
. . . . . . . . . . 11
Disj Disj |
196 | 193, 194,
195 | sylancl 694 |
. . . . . . . . . 10
Disj
|
197 | 184, 186,
191, 196 | disjxpin 29401 |
. . . . . . . . 9
Disj
|
198 | | disjss1 4626 |
. . . . . . . . 9
Disj Disj |
199 | 118, 197,
198 | mpsyl 68 |
. . . . . . . 8
Disj
|
200 | 199 | adantr 481 |
. . . . . . 7
Disj |
201 | | measvuni 30277 |
. . . . . . 7
measures Disj
Σ*
|
202 | 179, 181,
182, 200, 201 | syl112anc 1330 |
. . . . . 6
Σ*
|
203 | | ssfi 8180 |
. . . . . . . . 9
|
204 | 117, 118,
203 | sylancl 694 |
. . . . . . . 8
|
205 | 204 | adantr 481 |
. . . . . . 7
|
206 | | simpll 790 |
. . . . . . . 8
|
207 | | simpr 477 |
. . . . . . . . . 10
|
208 | 118, 207 | sseldi 3601 |
. . . . . . . . 9
|
209 | | xp1st 7198 |
. . . . . . . . 9
|
210 | 208, 209 | syl 17 |
. . . . . . . 8
|
211 | | xp2nd 7199 |
. . . . . . . . 9
|
212 | 208, 211 | syl 17 |
. . . . . . . 8
|
213 | | oveq12 6659 |
. . . . . . . . . . . . . . . 16
|
214 | | sibfof.5 |
. . . . . . . . . . . . . . . 16
|
215 | 213, 214 | sylan9eqr 2678 |
. . . . . . . . . . . . . . 15
|
216 | 215 | ex 450 |
. . . . . . . . . . . . . 14
|
217 | 216 | necon3ad 2807 |
. . . . . . . . . . . . 13
|
218 | | neorian 2888 |
. . . . . . . . . . . . 13
|
219 | 217, 218 | syl6ibr 242 |
. . . . . . . . . . . 12
|
220 | 219 | adantr 481 |
. . . . . . . . . . 11
|
221 | 220 | ralrimivva 2971 |
. . . . . . . . . 10
|
222 | 206, 221 | syl 17 |
. . . . . . . . 9
|
223 | 69 | a1i 11 |
. . . . . . . . . . . . 13
|
224 | 223 | sselda 3603 |
. . . . . . . . . . . 12
|
225 | | fniniseg 6338 |
. . . . . . . . . . . . 13
|
226 | 206, 63, 225 | 3syl 18 |
. . . . . . . . . . . 12
|
227 | 224, 226 | mpbid 222 |
. . . . . . . . . . 11
|
228 | | simpr 477 |
. . . . . . . . . . . 12
|
229 | | 1st2nd2 7205 |
. . . . . . . . . . . . . . 15
|
230 | 229 | fveq2d 6195 |
. . . . . . . . . . . . . 14
|
231 | | df-ov 6653 |
. . . . . . . . . . . . . 14
|
232 | 230, 231 | syl6eqr 2674 |
. . . . . . . . . . . . 13
|
233 | 232 | adantr 481 |
. . . . . . . . . . . 12
|
234 | 228, 233 | eqtr3d 2658 |
. . . . . . . . . . 11
|
235 | 227, 234 | syl 17 |
. . . . . . . . . 10
|
236 | | simplr 792 |
. . . . . . . . . . . 12
|
237 | 236 | eldifbd 3587 |
. . . . . . . . . . 11
|
238 | | velsn 4193 |
. . . . . . . . . . . 12
|
239 | 238 | necon3bbii 2841 |
. . . . . . . . . . 11
|
240 | 237, 239 | sylib 208 |
. . . . . . . . . 10
|
241 | 235, 240 | eqnetrrd 2862 |
. . . . . . . . 9
|
242 | 180, 76 | sylanl2 683 |
. . . . . . . . . . 11
|
243 | 242, 89 | syl 17 |
. . . . . . . . . 10
|
244 | 242, 102 | syl 17 |
. . . . . . . . . 10
|
245 | | oveq1 6657 |
. . . . . . . . . . . . 13
|
246 | 245 | neeq1d 2853 |
. . . . . . . . . . . 12
|
247 | | neeq1 2856 |
. . . . . . . . . . . . 13
|
248 | 247 | orbi1d 739 |
. . . . . . . . . . . 12
|
249 | 246, 248 | imbi12d 334 |
. . . . . . . . . . 11
|
250 | | oveq2 6658 |
. . . . . . . . . . . . 13
|
251 | 250 | neeq1d 2853 |
. . . . . . . . . . . 12
|
252 | | neeq1 2856 |
. . . . . . . . . . . . 13
|
253 | 252 | orbi2d 738 |
. . . . . . . . . . . 12
|
254 | 251, 253 | imbi12d 334 |
. . . . . . . . . . 11
|
255 | 249, 254 | rspc2v 3322 |
. . . . . . . . . 10
|
256 | 243, 244,
255 | syl2anc 693 |
. . . . . . . . 9
|
257 | 222, 241,
256 | mp2d 49 |
. . . . . . . 8
|
258 | 3, 4, 11, 12, 13, 14, 15, 16, 17, 19, 2, 78 | sibfinima 30401 |
. . . . . . . 8
|
259 | 206, 210,
212, 257, 258 | syl31anc 1329 |
. . . . . . 7
|
260 | 205, 259 | esumpfinval 30137 |
. . . . . 6
Σ*
|
261 | 176, 202,
260 | 3eqtrd 2660 |
. . . . 5
|
262 | | rge0ssre 12280 |
. . . . . . 7
|
263 | 262, 259 | sseldi 3601 |
. . . . . 6
|
264 | 205, 263 | fsumrecl 14465 |
. . . . 5
|
265 | 261, 264 | eqeltrd 2701 |
. . . 4
|
266 | 179 | adantr 481 |
. . . . . . 7
measures |
267 | 180, 112 | sylanl2 683 |
. . . . . . 7
|
268 | | measge0 30270 |
. . . . . . 7
measures
|
269 | 266, 267,
268 | syl2anc 693 |
. . . . . 6
|
270 | 205, 263,
269 | fsumge0 14527 |
. . . . 5
|
271 | 270, 261 | breqtrrd 4681 |
. . . 4
|
272 | | elrege0 12278 |
. . . 4
|
273 | 265, 271,
272 | sylanbrc 698 |
. . 3
|
274 | 273 | ralrimiva 2966 |
. 2
|
275 | | eqid 2622 |
. . 3
sigaGen sigaGen |
276 | | eqid 2622 |
. . 3
|
277 | | eqid 2622 |
. . 3
|
278 | | eqid 2622 |
. . 3
RRHomScalar RRHomScalar |
279 | 27, 28, 275, 276, 277, 278, 26, 16 | issibf 30395 |
. 2
sitg MblFnMsigaGen
|
280 | 174, 142,
274, 279 | mpbir3and 1245 |
1
sitg |