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 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑀 ↾ 𝑇 ) ∈ ( measures ‘ 𝑇 ) )

Proof

Step Hyp Ref Expression
1 simp2 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ∈ ∪ ran sigAlgebra )
2 measfrge0 ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
3 2 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → 𝑀 : 𝑆 ⟶ ( 0 [,] +∞ ) )
4 simp3 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → 𝑇 ⊆ 𝑆 )
5 3 4 fssresd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑀 ↾ 𝑇 ) : 𝑇 ⟶ ( 0 [,] +∞ ) )
6 0elsiga ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ∅ ∈ 𝑇 )
7 fvres ⊢ ( ∅ ∈ 𝑇 → ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
8 1 6 7 3syl ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = ( 𝑀 ‘ ∅ ) )
9 measvnul ⊢ ( 𝑀 ∈ ( measures ‘ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )
10 9 3ad2ant1 ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑀 ‘ ∅ ) = 0 )
11 8 10 eqtrd ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = 0 )
12 simp11 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑀 ∈ ( measures ‘ 𝑆 ) )
13 simp13 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑇 ⊆ 𝑆 )
14 simp2 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ∈ 𝒫 𝑇 )
15 sspw ⊢ ( 𝑇 ⊆ 𝑆 → 𝒫 𝑇 ⊆ 𝒫 𝑆 )
16 15 sselda ⊢ ( ( 𝑇 ⊆ 𝑆 ∧ 𝑥 ∈ 𝒫 𝑇 ) → 𝑥 ∈ 𝒫 𝑆 )
17 13 14 16 syl2anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ∈ 𝒫 𝑆 )
18 simp3 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) )
19 measvun ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑆 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
20 12 17 18 19 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( 𝑀 ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
21 1 3ad2ant1 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑇 ∈ ∪ ran sigAlgebra )
22 simp3l ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → 𝑥 ≼ ω )
23 sigaclcu ⊢ ( ( 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑥 ∈ 𝒫 𝑇 ∧ 𝑥 ≼ ω ) → ∪ 𝑥 ∈ 𝑇 )
24 21 14 22 23 syl3anc ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ∪ 𝑥 ∈ 𝑇 )
25 24 fvresd ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = ( 𝑀 ‘ ∪ 𝑥 ) )
26 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝑇 → 𝑥 ⊆ 𝑇 )
27 26 sselda ⊢ ( ( 𝑥 ∈ 𝒫 𝑇 ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑇 )
28 27 adantll ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ) ∧ 𝑦 ∈ 𝑥 ) → 𝑦 ∈ 𝑇 )
29 28 fvresd ⊢ ( ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ) ∧ 𝑦 ∈ 𝑥 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) = ( 𝑀 ‘ 𝑦 ) )
30 29 esumeq2dv ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ) → Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
31 30 3adant3 ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) = Σ* 𝑦 ∈ 𝑥 ( 𝑀 ‘ 𝑦 ) )
32 20 25 31 3eqtr4d ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ∧ ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) )
33 32 3expia ⊢ ( ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) ∧ 𝑥 ∈ 𝒫 𝑇 ) → ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) ) )
34 33 ralrimiva ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ∀ 𝑥 ∈ 𝒫 𝑇 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) ) )
35 5 11 34 3jca ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( ( 𝑀 ↾ 𝑇 ) : 𝑇 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) ) ) )
36 ismeas ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ( ( 𝑀 ↾ 𝑇 ) ∈ ( measures ‘ 𝑇 ) ↔ ( ( 𝑀 ↾ 𝑇 ) : 𝑇 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) ) ) ) )
37 36 biimprd ⊢ ( 𝑇 ∈ ∪ ran sigAlgebra → ( ( ( 𝑀 ↾ 𝑇 ) : 𝑇 ⟶ ( 0 [,] +∞ ) ∧ ( ( 𝑀 ↾ 𝑇 ) ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑇 ( ( 𝑥 ≼ ω ∧ Disj 𝑦 ∈ 𝑥 𝑦 ) → ( ( 𝑀 ↾ 𝑇 ) ‘ ∪ 𝑥 ) = Σ* 𝑦 ∈ 𝑥 ( ( 𝑀 ↾ 𝑇 ) ‘ 𝑦 ) ) ) → ( 𝑀 ↾ 𝑇 ) ∈ ( measures ‘ 𝑇 ) ) )
38 1 35 37 sylc ⊢ ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝑇 ∈ ∪ ran sigAlgebra ∧ 𝑇 ⊆ 𝑆 ) → ( 𝑀 ↾ 𝑇 ) ∈ ( measures ‘ 𝑇 ) )