Description: Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Assertion | measinb | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | simpll | |
|
2 | measbase | |
|
3 | 2 | ad2antrr | |
4 | simpr | |
|
5 | simplr | |
|
6 | inelsiga | |
|
7 | 3 4 5 6 | syl3anc | |
8 | measvxrge0 | |
|
9 | 1 7 8 | syl2anc | |
10 | 9 | fmpttd | |
11 | eqidd | |
|
12 | ineq1 | |
|
13 | 0in | |
|
14 | 12 13 | eqtrdi | |
15 | 14 | fveq2d | |
16 | 15 | adantl | |
17 | measvnul | |
|
18 | 17 | ad2antrr | |
19 | 16 18 | eqtrd | |
20 | 2 | adantr | |
21 | 0elsiga | |
|
22 | 20 21 | syl | |
23 | 0red | |
|
24 | 11 19 22 23 | fvmptd | |
25 | measinblem | |
|
26 | eqidd | |
|
27 | ineq1 | |
|
28 | 27 | adantl | |
29 | 28 | fveq2d | |
30 | simplll | |
|
31 | 30 2 | syl | |
32 | simplr | |
|
33 | simprl | |
|
34 | sigaclcu | |
|
35 | 31 32 33 34 | syl3anc | |
36 | simpllr | |
|
37 | inelsiga | |
|
38 | 31 35 36 37 | syl3anc | |
39 | measvxrge0 | |
|
40 | 30 38 39 | syl2anc | |
41 | 26 29 35 40 | fvmptd | |
42 | eqidd | |
|
43 | ineq1 | |
|
44 | 43 | adantl | |
45 | 44 | fveq2d | |
46 | elpwi | |
|
47 | 46 | ad2antlr | |
48 | simpr | |
|
49 | 47 48 | sseldd | |
50 | simplll | |
|
51 | 50 2 | syl | |
52 | simpllr | |
|
53 | inelsiga | |
|
54 | 51 49 52 53 | syl3anc | |
55 | measvxrge0 | |
|
56 | 50 54 55 | syl2anc | |
57 | 42 45 49 56 | fvmptd | |
58 | 57 | esumeq2dv | |
59 | 58 | adantr | |
60 | 25 41 59 | 3eqtr4d | |
61 | 60 | ex | |
62 | 61 | ralrimiva | |
63 | ismeas | |
|
64 | 20 63 | syl | |
65 | 10 24 62 64 | mpbir3and | |