Metamath Proof Explorer


Theorem measinb2

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

Ref Expression
Assertion measinb2 ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ∈ ( measures ‘ ( 𝑆 ∩ 𝒫 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 resmpt3 ( ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ↾ ( 𝑆 ∩ 𝒫 𝐴 ) ) = ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑆 ∩ 𝒫 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) )
2 inin ( 𝑆 ∩ ( 𝑆 ∩ 𝒫 𝐴 ) ) = ( 𝑆 ∩ 𝒫 𝐴 )
3 eqid ( 𝑀 ‘ ( 𝑥𝐴 ) ) = ( 𝑀 ‘ ( 𝑥𝐴 ) )
4 2 3 mpteq12i ( 𝑥 ∈ ( 𝑆 ∩ ( 𝑆 ∩ 𝒫 𝐴 ) ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) )
5 1 4 eqtri ( ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ↾ ( 𝑆 ∩ 𝒫 𝐴 ) ) = ( 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) )
6 measinb ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) )
7 measbase ( 𝑀 ∈ ( measures ‘ 𝑆 ) → 𝑆 ran sigAlgebra )
8 sigainb ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) )
9 elrnsiga ( ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ( sigAlgebra ‘ 𝐴 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ran sigAlgebra )
10 8 9 syl ( ( 𝑆 ran sigAlgebra ∧ 𝐴𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ran sigAlgebra )
11 7 10 sylan ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ran sigAlgebra )
12 inss1 ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝑆
13 12 a1i ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝑆 )
14 measres ( ( ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ∈ ( measures ‘ 𝑆 ) ∧ ( 𝑆 ∩ 𝒫 𝐴 ) ∈ ran sigAlgebra ∧ ( 𝑆 ∩ 𝒫 𝐴 ) ⊆ 𝑆 ) → ( ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ↾ ( 𝑆 ∩ 𝒫 𝐴 ) ) ∈ ( measures ‘ ( 𝑆 ∩ 𝒫 𝐴 ) ) )
15 6 11 13 14 syl3anc ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( ( 𝑥𝑆 ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ↾ ( 𝑆 ∩ 𝒫 𝐴 ) ) ∈ ( measures ‘ ( 𝑆 ∩ 𝒫 𝐴 ) ) )
16 5 15 eqeltrrid ( ( 𝑀 ∈ ( measures ‘ 𝑆 ) ∧ 𝐴𝑆 ) → ( 𝑥 ∈ ( 𝑆 ∩ 𝒫 𝐴 ) ↦ ( 𝑀 ‘ ( 𝑥𝐴 ) ) ) ∈ ( measures ‘ ( 𝑆 ∩ 𝒫 𝐴 ) ) )