Metamath Proof Explorer


Theorem measres

Description: Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion measres M measures S T ran sigAlgebra T S M T measures T

Proof

Step Hyp Ref Expression
1 simp2 M measures S T ran sigAlgebra T S T ran sigAlgebra
2 measfrge0 M measures S M : S 0 +∞
3 2 3ad2ant1 M measures S T ran sigAlgebra T S M : S 0 +∞
4 simp3 M measures S T ran sigAlgebra T S T S
5 3 4 fssresd M measures S T ran sigAlgebra T S M T : T 0 +∞
6 0elsiga T ran sigAlgebra T
7 fvres T M T = M
8 1 6 7 3syl M measures S T ran sigAlgebra T S M T = M
9 measvnul M measures S M = 0
10 9 3ad2ant1 M measures S T ran sigAlgebra T S M = 0
11 8 10 eqtrd M measures S T ran sigAlgebra T S M T = 0
12 simp11 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M measures S
13 simp13 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y T S
14 simp2 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y x 𝒫 T
15 sspw T S 𝒫 T 𝒫 S
16 15 sselda T S x 𝒫 T x 𝒫 S
17 13 14 16 syl2anc M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y x 𝒫 S
18 simp3 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y x ω Disj y x y
19 measvun M measures S x 𝒫 S x ω Disj y x y M x = * y x M y
20 12 17 18 19 syl3anc M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M x = * y x M y
21 1 3ad2ant1 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y T ran sigAlgebra
22 simp3l M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y x ω
23 sigaclcu T ran sigAlgebra x 𝒫 T x ω x T
24 21 14 22 23 syl3anc M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y x T
25 24 fvresd M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M T x = M x
26 elpwi x 𝒫 T x T
27 26 sselda x 𝒫 T y x y T
28 27 adantll M measures S T ran sigAlgebra T S x 𝒫 T y x y T
29 28 fvresd M measures S T ran sigAlgebra T S x 𝒫 T y x M T y = M y
30 29 esumeq2dv M measures S T ran sigAlgebra T S x 𝒫 T * y x M T y = * y x M y
31 30 3adant3 M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y * y x M T y = * y x M y
32 20 25 31 3eqtr4d M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M T x = * y x M T y
33 32 3expia M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M T x = * y x M T y
34 33 ralrimiva M measures S T ran sigAlgebra T S x 𝒫 T x ω Disj y x y M T x = * y x M T y
35 5 11 34 3jca M measures S T ran sigAlgebra T S M T : T 0 +∞ M T = 0 x 𝒫 T x ω Disj y x y M T x = * y x M T y
36 ismeas T ran sigAlgebra M T measures T M T : T 0 +∞ M T = 0 x 𝒫 T x ω Disj y x y M T x = * y x M T y
37 36 biimprd T ran sigAlgebra M T : T 0 +∞ M T = 0 x 𝒫 T x ω Disj y x y M T x = * y x M T y M T measures T
38 1 35 37 sylc M measures S T ran sigAlgebra T S M T measures T