measres

Description: Building a measure restricted to a smaller sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

		Ref	Expression
	Assertion	measres	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to {M ↾}_{T} \in measures (T)$

Proof

Step	Hyp	Ref	Expression
1		simp2	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to T \in ⋃ ran sigAlgebra$
2		measfrge0	$⊢ M \in measures (S) \to M : S ⟶ [0, +∞]$
3	2	3ad2ant1	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to M : S ⟶ [0, +∞]$
4		simp3	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to T \subseteq S$
5	3 4	fssresd	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to ({M ↾}_{T}) : T ⟶ [0, +∞]$
6		0elsiga	$⊢ T \in ⋃ ran sigAlgebra \to \emptyset \in T$
7		fvres	$⊢ \emptyset \in T \to ({M ↾}_{T}) (\emptyset) = M (\emptyset)$
8	1 6 7	3syl	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to ({M ↾}_{T}) (\emptyset) = M (\emptyset)$
9		measvnul	$⊢ M \in measures (S) \to M (\emptyset) = 0$
10	9	3ad2ant1	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to M (\emptyset) = 0$
11	8 10	eqtrd	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to ({M ↾}_{T}) (\emptyset) = 0$
12		simp11	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to M \in measures (S)$
13		simp13	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to T \subseteq S$
14		simp2	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x \in 𝒫 T$
15		sspw	$⊢ T \subseteq S \to 𝒫 T \subseteq 𝒫 S$
16	15	sselda	$⊢ (T \subseteq S \land x \in 𝒫 T) \to x \in 𝒫 S$
17	13 14 16	syl2anc	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x \in 𝒫 S$
18		simp3	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to (x ≼ ω \land \underset{y \in x}{Disj} y)$
19		measvun	$⊢ (M \in measures (S) \land x \in 𝒫 S \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y)$
20	12 17 18 19	syl3anc	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to M (⋃ x) = \underset{y \in x}{\sum^{*}} M (y)$
21	1	3ad2ant1	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to T \in ⋃ ran sigAlgebra$
22		simp3l	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to x ≼ ω$
23		sigaclcu	$⊢ (T \in ⋃ ran sigAlgebra \land x \in 𝒫 T \land x ≼ ω) \to ⋃ x \in T$
24	21 14 22 23	syl3anc	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ⋃ x \in T$
25	24	fvresd	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ({M ↾}_{T}) (⋃ x) = M (⋃ x)$
26		elpwi	$⊢ x \in 𝒫 T \to x \subseteq T$
27	26	sselda	$⊢ (x \in 𝒫 T \land y \in x) \to y \in T$
28	27	adantll	$⊢ (((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T) \land y \in x) \to y \in T$
29	28	fvresd	$⊢ (((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T) \land y \in x) \to ({M ↾}_{T}) (y) = M (y)$
30	29	esumeq2dv	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T) \to \underset{y \in x}{\sum^{}} ({M ↾}_{T}) (y) = \underset{y \in x}{\sum^{}} M (y)$
31	30	3adant3	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to \underset{y \in x}{\sum^{}} ({M ↾}_{T}) (y) = \underset{y \in x}{\sum^{}} M (y)$
32	20 25 31	3eqtr4d	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y)$
33	32	3expia	$⊢ ((M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \land x \in 𝒫 T) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y))$
34	33	ralrimiva	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to \forall x \in 𝒫 T ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y))$
35	5 11 34	3jca	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to (({M ↾}_{T}) : T ⟶ [0, +∞] \land ({M ↾}_{T}) (\emptyset) = 0 \land \forall x \in 𝒫 T ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y)))$
36		ismeas	$⊢ T \in ⋃ ran sigAlgebra \to ({M ↾}_{T} \in measures (T) \leftrightarrow (({M ↾}_{T}) : T ⟶ [0, +∞] \land ({M ↾}_{T}) (\emptyset) = 0 \land \forall x \in 𝒫 T ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y))))$
37	36	biimprd	$⊢ T \in ⋃ ran sigAlgebra \to ((({M ↾}_{T}) : T ⟶ [0, +∞] \land ({M ↾}_{T}) (\emptyset) = 0 \land \forall x \in 𝒫 T ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({M ↾}_{T}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({M ↾}_{T}) (y))) \to {M ↾}_{T} \in measures (T))$
38	1 35 37	sylc	$⊢ (M \in measures (S) \land T \in ⋃ ran sigAlgebra \land T \subseteq S) \to {M ↾}_{T} \in measures (T)$

Metamath Proof Explorer

Theorem measres

Proof