Metamath Proof Explorer


Theorem measinb

Description: Building a measure restricted to the intersection with a given set. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measinb MmeasuresSASxSMxAmeasuresS

Proof

Step Hyp Ref Expression
1 simpll MmeasuresSASxSMmeasuresS
2 measbase MmeasuresSSransigAlgebra
3 2 ad2antrr MmeasuresSASxSSransigAlgebra
4 simpr MmeasuresSASxSxS
5 simplr MmeasuresSASxSAS
6 inelsiga SransigAlgebraxSASxAS
7 3 4 5 6 syl3anc MmeasuresSASxSxAS
8 measvxrge0 MmeasuresSxASMxA0+∞
9 1 7 8 syl2anc MmeasuresSASxSMxA0+∞
10 9 fmpttd MmeasuresSASxSMxA:S0+∞
11 eqidd MmeasuresSASxSMxA=xSMxA
12 ineq1 x=xA=A
13 0in A=
14 12 13 eqtrdi x=xA=
15 14 fveq2d x=MxA=M
16 15 adantl MmeasuresSASx=MxA=M
17 measvnul MmeasuresSM=0
18 17 ad2antrr MmeasuresSASx=M=0
19 16 18 eqtrd MmeasuresSASx=MxA=0
20 2 adantr MmeasuresSASSransigAlgebra
21 0elsiga SransigAlgebraS
22 20 21 syl MmeasuresSASS
23 0red MmeasuresSAS0
24 11 19 22 23 fvmptd MmeasuresSASxSMxA=0
25 measinblem MmeasuresSASz𝒫SzωDisjyzyMzA=*yzMyA
26 eqidd MmeasuresSASz𝒫SzωDisjyzyxSMxA=xSMxA
27 ineq1 x=zxA=zA
28 27 adantl MmeasuresSASz𝒫SzωDisjyzyx=zxA=zA
29 28 fveq2d MmeasuresSASz𝒫SzωDisjyzyx=zMxA=MzA
30 simplll MmeasuresSASz𝒫SzωDisjyzyMmeasuresS
31 30 2 syl MmeasuresSASz𝒫SzωDisjyzySransigAlgebra
32 simplr MmeasuresSASz𝒫SzωDisjyzyz𝒫S
33 simprl MmeasuresSASz𝒫SzωDisjyzyzω
34 sigaclcu SransigAlgebraz𝒫SzωzS
35 31 32 33 34 syl3anc MmeasuresSASz𝒫SzωDisjyzyzS
36 simpllr MmeasuresSASz𝒫SzωDisjyzyAS
37 inelsiga SransigAlgebrazSASzAS
38 31 35 36 37 syl3anc MmeasuresSASz𝒫SzωDisjyzyzAS
39 measvxrge0 MmeasuresSzASMzA0+∞
40 30 38 39 syl2anc MmeasuresSASz𝒫SzωDisjyzyMzA0+∞
41 26 29 35 40 fvmptd MmeasuresSASz𝒫SzωDisjyzyxSMxAz=MzA
42 eqidd MmeasuresSASz𝒫SyzxSMxA=xSMxA
43 ineq1 x=yxA=yA
44 43 adantl MmeasuresSASz𝒫Syzx=yxA=yA
45 44 fveq2d MmeasuresSASz𝒫Syzx=yMxA=MyA
46 elpwi z𝒫SzS
47 46 ad2antlr MmeasuresSASz𝒫SyzzS
48 simpr MmeasuresSASz𝒫Syzyz
49 47 48 sseldd MmeasuresSASz𝒫SyzyS
50 simplll MmeasuresSASz𝒫SyzMmeasuresS
51 50 2 syl MmeasuresSASz𝒫SyzSransigAlgebra
52 simpllr MmeasuresSASz𝒫SyzAS
53 inelsiga SransigAlgebraySASyAS
54 51 49 52 53 syl3anc MmeasuresSASz𝒫SyzyAS
55 measvxrge0 MmeasuresSyASMyA0+∞
56 50 54 55 syl2anc MmeasuresSASz𝒫SyzMyA0+∞
57 42 45 49 56 fvmptd MmeasuresSASz𝒫SyzxSMxAy=MyA
58 57 esumeq2dv MmeasuresSASz𝒫S*yzxSMxAy=*yzMyA
59 58 adantr MmeasuresSASz𝒫SzωDisjyzy*yzxSMxAy=*yzMyA
60 25 41 59 3eqtr4d MmeasuresSASz𝒫SzωDisjyzyxSMxAz=*yzxSMxAy
61 60 ex MmeasuresSASz𝒫SzωDisjyzyxSMxAz=*yzxSMxAy
62 61 ralrimiva MmeasuresSASz𝒫SzωDisjyzyxSMxAz=*yzxSMxAy
63 ismeas SransigAlgebraxSMxAmeasuresSxSMxA:S0+∞xSMxA=0z𝒫SzωDisjyzyxSMxAz=*yzxSMxAy
64 20 63 syl MmeasuresSASxSMxAmeasuresSxSMxA:S0+∞xSMxA=0z𝒫SzωDisjyzyxSMxAz=*yzxSMxAy
65 10 24 62 64 mpbir3and MmeasuresSASxSMxAmeasuresS