measinb

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

		Ref	Expression
	Assertion	measinb	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) \in measures (S)$

Proof

Step	Hyp	Ref	Expression
1		simpll	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to M \in measures (S)$
2		measbase	$⊢ M \in measures (S) \to S \in ⋃ ran sigAlgebra$
3	2	ad2antrr	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to S \in ⋃ ran sigAlgebra$
4		simpr	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to x \in S$
5		simplr	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to A \in S$
6		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land x \in S \land A \in S) \to x \cap A \in S$
7	3 4 5 6	syl3anc	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to x \cap A \in S$
8		measvxrge0	$⊢ (M \in measures (S) \land x \cap A \in S) \to M (x \cap A) \in [0, +∞]$
9	1 7 8	syl2anc	$⊢ ((M \in measures (S) \land A \in S) \land x \in S) \to M (x \cap A) \in [0, +∞]$
10	9	fmpttd	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) : S ⟶ [0, +∞]$
11		eqidd	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) = (x \in S ⟼ M (x \cap A))$
12		ineq1	$⊢ x = \emptyset \to x \cap A = \emptyset \cap A$
13		0in	$⊢ \emptyset \cap A = \emptyset$
14	12 13	eqtrdi	$⊢ x = \emptyset \to x \cap A = \emptyset$
15	14	fveq2d	$⊢ x = \emptyset \to M (x \cap A) = M (\emptyset)$
16	15	adantl	$⊢ ((M \in measures (S) \land A \in S) \land x = \emptyset) \to M (x \cap A) = M (\emptyset)$
17		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
18	17	ad2antrr	$⊢ ((M \in measures (S) \land A \in S) \land x = \emptyset) \to M (\emptyset) = 0$
19	16 18	eqtrd	$⊢ ((M \in measures (S) \land A \in S) \land x = \emptyset) \to M (x \cap A) = 0$
20	2	adantr	$⊢ (M \in measures (S) \land A \in S) \to S \in ⋃ ran sigAlgebra$
21		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
22	20 21	syl	$⊢ (M \in measures (S) \land A \in S) \to \emptyset \in S$
23		0red	$⊢ (M \in measures (S) \land A \in S) \to 0 \in ℝ$
24	11 19 22 23	fvmptd	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) (\emptyset) = 0$
25		measinblem	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to M (⋃ z \cap A) = \underset{y \in z}{\sum^{*}} M (y \cap A)$
26		eqidd	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to (x \in S ⟼ M (x \cap A)) = (x \in S ⟼ M (x \cap A))$
27		ineq1	$⊢ x = ⋃ z \to x \cap A = ⋃ z \cap A$
28	27	adantl	$⊢ ((((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \land x = ⋃ z) \to x \cap A = ⋃ z \cap A$
29	28	fveq2d	$⊢ ((((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \land x = ⋃ z) \to M (x \cap A) = M (⋃ z \cap A)$
30		simplll	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to M \in measures (S)$
31	30 2	syl	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to S \in ⋃ ran sigAlgebra$
32		simplr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to z \in 𝒫 S$
33		simprl	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to z ≼ ω$
34		sigaclcu	$⊢ (S \in ⋃ ran sigAlgebra \land z \in 𝒫 S \land z ≼ ω) \to ⋃ z \in S$
35	31 32 33 34	syl3anc	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to ⋃ z \in S$
36		simpllr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to A \in S$
37		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land ⋃ z \in S \land A \in S) \to ⋃ z \cap A \in S$
38	31 35 36 37	syl3anc	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to ⋃ z \cap A \in S$
39		measvxrge0	$⊢ (M \in measures (S) \land ⋃ z \cap A \in S) \to M (⋃ z \cap A) \in [0, +∞]$
40	30 38 39	syl2anc	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to M (⋃ z \cap A) \in [0, +∞]$
41	26 29 35 40	fvmptd	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = M (⋃ z \cap A)$
42		eqidd	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to (x \in S ⟼ M (x \cap A)) = (x \in S ⟼ M (x \cap A))$
43		ineq1	$⊢ x = y \to x \cap A = y \cap A$
44	43	adantl	$⊢ ((((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \land x = y) \to x \cap A = y \cap A$
45	44	fveq2d	$⊢ ((((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \land x = y) \to M (x \cap A) = M (y \cap A)$
46		elpwi	$⊢ z \in 𝒫 S \to z \subseteq S$
47	46	ad2antlr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to z \subseteq S$
48		simpr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to y \in z$
49	47 48	sseldd	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to y \in S$
50		simplll	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to M \in measures (S)$
51	50 2	syl	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to S \in ⋃ ran sigAlgebra$
52		simpllr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to A \in S$
53		inelsiga	$⊢ (S \in ⋃ ran sigAlgebra \land y \in S \land A \in S) \to y \cap A \in S$
54	51 49 52 53	syl3anc	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to y \cap A \in S$
55		measvxrge0	$⊢ (M \in measures (S) \land y \cap A \in S) \to M (y \cap A) \in [0, +∞]$
56	50 54 55	syl2anc	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to M (y \cap A) \in [0, +∞]$
57	42 45 49 56	fvmptd	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land y \in z) \to (x \in S ⟼ M (x \cap A)) (y) = M (y \cap A)$
58	57	esumeq2dv	$⊢ ((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \to \underset{y \in z}{\sum^{}} (x \in S ⟼ M (x \cap A)) (y) = \underset{y \in z}{\sum^{}} M (y \cap A)$
59	58	adantr	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to \underset{y \in z}{\sum^{}} (x \in S ⟼ M (x \cap A)) (y) = \underset{y \in z}{\sum^{}} M (y \cap A)$
60	25 41 59	3eqtr4d	$⊢ (((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \land (z ≼ ω \land \underset{y \in z}{Disj} y)) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = \underset{y \in z}{\sum^{*}} (x \in S ⟼ M (x \cap A)) (y)$
61	60	ex	$⊢ ((M \in measures (S) \land A \in S) \land z \in 𝒫 S) \to ((z ≼ ω \land \underset{y \in z}{Disj} y) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = \underset{y \in z}{\sum^{*}} (x \in S ⟼ M (x \cap A)) (y))$
62	61	ralrimiva	$⊢ (M \in measures (S) \land A \in S) \to \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = \underset{y \in z}{\sum^{*}} (x \in S ⟼ M (x \cap A)) (y))$
63		ismeas	$⊢ S \in ⋃ ran sigAlgebra \to ((x \in S ⟼ M (x \cap A)) \in measures (S) \leftrightarrow ((x \in S ⟼ M (x \cap A)) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x \cap A)) (\emptyset) = 0 \land \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = \underset{y \in z}{\sum^{*}} (x \in S ⟼ M (x \cap A)) (y))))$
64	20 63	syl	$⊢ (M \in measures (S) \land A \in S) \to ((x \in S ⟼ M (x \cap A)) \in measures (S) \leftrightarrow ((x \in S ⟼ M (x \cap A)) : S ⟶ [0, +∞] \land (x \in S ⟼ M (x \cap A)) (\emptyset) = 0 \land \forall z \in 𝒫 S ((z ≼ ω \land \underset{y \in z}{Disj} y) \to (x \in S ⟼ M (x \cap A)) (⋃ z) = \underset{y \in z}{\sum^{*}} (x \in S ⟼ M (x \cap A)) (y))))$
65	10 24 62 64	mpbir3and	$⊢ (M \in measures (S) \land A \in S) \to (x \in S ⟼ M (x \cap A)) \in measures (S)$

Metamath Proof Explorer

Theorem measinb

Proof