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	$⊢ (M \in measures (S) \land A \in S) \to (x \in (S \cap 𝒫 A) ⟼ M (x \cap A)) \in measures (S \cap 𝒫 A)$

Proof

Step	Hyp	Ref	Expression
1		resmpt3	$⊢ {(x \in S ⟼ M (x \cap A)) ↾}_{(S \cap 𝒫 A)} = (x \in (S \cap (S \cap 𝒫 A)) ⟼ M (x \cap A))$
2		inin	$⊢ S \cap (S \cap 𝒫 A) = S \cap 𝒫 A$
3		eqid	$⊢ M (x \cap A) = M (x \cap A)$
4	2 3	mpteq12i	$⊢ (x \in (S \cap (S \cap 𝒫 A)) ⟼ M (x \cap A)) = (x \in (S \cap 𝒫 A) ⟼ M (x \cap A))$
5	1 4	eqtri	$⊢ {(x \in S ⟼ M (x \cap A)) ↾}_{(S \cap 𝒫 A)} = (x \in (S \cap 𝒫 A) ⟼ M (x \cap A))$
6		measinb	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) \in measures (S)$
7		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
8		sigainb	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \in sigAlgebra (A)$
9		elrnsiga	$⊢ S \cap 𝒫 A \in sigAlgebra (A) \to S \cap 𝒫 A \in ⋃ ran sigAlgebra$
10	8 9	syl	$⊢ (S \in ⋃ ran sigAlgebra \land A \in S) \to S \cap 𝒫 A \in ⋃ ran sigAlgebra$
11	7 10	sylan	$⊢ (M \in measures (S) \land A \in S) \to S \cap 𝒫 A \in ⋃ ran sigAlgebra$
12		inss1	$⊢ S \cap 𝒫 A \subseteq S$
13	12	a1i	$⊢ (M \in measures (S) \land A \in S) \to S \cap 𝒫 A \subseteq S$
14		measres	$⊢ ((x \in S ⟼ M (x \cap A)) \in measures (S) \land S \cap 𝒫 A \in ⋃ ran sigAlgebra \land S \cap 𝒫 A \subseteq S) \to {(x \in S ⟼ M (x \cap A)) ↾}_{(S \cap 𝒫 A)} \in measures (S \cap 𝒫 A)$
15	6 11 13 14	syl3anc	$⊢ (M \in measures (S) \land A \in S) \to {(x \in S ⟼ M (x \cap A)) ↾}_{(S \cap 𝒫 A)} \in measures (S \cap 𝒫 A)$
16	5 15	eqeltrrid	$⊢ (M \in measures (S) \land A \in S) \to (x \in (S \cap 𝒫 A) ⟼ M (x \cap A)) \in measures (S \cap 𝒫 A)$