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 ‘ ( 𝑆 ∩ 𝒫 𝐴 ) ) )