cntmeas

Description: The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

		Ref	Expression
	Assertion	cntmeas	$⊢ S \in ⋃ ran sigAlgebra \to {\|.\| ↾}_{S} \in measures (S)$

Proof

Step	Hyp	Ref	Expression
1		hashf2	$⊢ \|.\| : V ⟶ [0, +∞]$
2		ssv	$⊢ S \subseteq V$
3		fssres	$⊢ (\|.\| : V ⟶ [0, +∞] \land S \subseteq V) \to ({\|.\| ↾}_{S}) : S ⟶ [0, +∞]$
4	1 2 3	mp2an	$⊢ ({\|.\| ↾}_{S}) : S ⟶ [0, +∞]$
5	4	a1i	$⊢ S \in ⋃ ran sigAlgebra \to ({\|.\| ↾}_{S}) : S ⟶ [0, +∞]$
6		0elsiga	$⊢ S \in ⋃ ran sigAlgebra \to \emptyset \in S$
7		fvres	$⊢ \emptyset \in S \to ({\|.\| ↾}_{S}) (\emptyset) = \|\emptyset\|$
8	6 7	syl	$⊢ S \in ⋃ ran sigAlgebra \to ({\|.\| ↾}_{S}) (\emptyset) = \|\emptyset\|$
9		hash0	$⊢ \|\emptyset\| = 0$
10	8 9	eqtrdi	$⊢ S \in ⋃ ran sigAlgebra \to ({\|.\| ↾}_{S}) (\emptyset) = 0$
11		vex	$⊢ x \in V$
12		hasheuni	$⊢ (x \in V \land \underset{y \in x}{Disj} y) \to \|⋃ x\| = \underset{y \in x}{\sum^{*}} \|y\|$
13	11 12	mpan	$⊢ \underset{y \in x}{Disj} y \to \|⋃ x\| = \underset{y \in x}{\sum^{*}} \|y\|$
14	13	ad2antll	$⊢ ((S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to \|⋃ x\| = \underset{y \in x}{\sum^{*}} \|y\|$
15		isrnsigau	$⊢ S \in ⋃ ran sigAlgebra \to (S \subseteq 𝒫 ⋃ S \land (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)))$
16	15	simprd	$⊢ S \in ⋃ ran sigAlgebra \to (⋃ S \in S \land \forall x \in S ⋃ S ∖ x \in S \land \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S))$
17	16	simp3d	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S)$
18		fvres	$⊢ ⋃ x \in S \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|$
19	18	imim2i	$⊢ (x ≼ ω \to ⋃ x \in S) \to (x ≼ ω \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|)$
20	19	ralimi	$⊢ \forall x \in 𝒫 S (x ≼ ω \to ⋃ x \in S) \to \forall x \in 𝒫 S (x ≼ ω \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|)$
21	17 20	syl	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S (x ≼ ω \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|)$
22	21	r19.21bi	$⊢ (S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \to (x ≼ ω \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|)$
23	22	imp	$⊢ ((S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \land x ≼ ω) \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|$
24	23	adantrr	$⊢ ((S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ({\|.\| ↾}_{S}) (⋃ x) = \|⋃ x\|$
25		elpwi	$⊢ x \in 𝒫 S \to x \subseteq S$
26	25	sseld	$⊢ x \in 𝒫 S \to (y \in x \to y \in S)$
27		fvres	$⊢ y \in S \to ({\|.\| ↾}_{S}) (y) = \|y\|$
28	26 27	syl6	$⊢ x \in 𝒫 S \to (y \in x \to ({\|.\| ↾}_{S}) (y) = \|y\|)$
29	28	imp	$⊢ (x \in 𝒫 S \land y \in x) \to ({\|.\| ↾}_{S}) (y) = \|y\|$
30	29	esumeq2dv	$⊢ x \in 𝒫 S \to \underset{y \in x}{\sum^{}} ({\|.\| ↾}_{S}) (y) = \underset{y \in x}{\sum^{}} \|y\|$
31	30	ad2antlr	$⊢ ((S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to \underset{y \in x}{\sum^{}} ({\|.\| ↾}_{S}) (y) = \underset{y \in x}{\sum^{}} \|y\|$
32	14 24 31	3eqtr4d	$⊢ ((S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \land (x ≼ ω \land \underset{y \in x}{Disj} y)) \to ({\|.\| ↾}_{S}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({\|.\| ↾}_{S}) (y)$
33	32	ex	$⊢ (S \in ⋃ ran sigAlgebra \land x \in 𝒫 S) \to ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({\|.\| ↾}_{S}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({\|.\| ↾}_{S}) (y))$
34	33	ralrimiva	$⊢ S \in ⋃ ran sigAlgebra \to \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({\|.\| ↾}_{S}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({\|.\| ↾}_{S}) (y))$
35		ismeas	$⊢ S \in ⋃ ran sigAlgebra \to ({\|.\| ↾}_{S} \in measures (S) \leftrightarrow (({\|.\| ↾}_{S}) : S ⟶ [0, +∞] \land ({\|.\| ↾}_{S}) (\emptyset) = 0 \land \forall x \in 𝒫 S ((x ≼ ω \land \underset{y \in x}{Disj} y) \to ({\|.\| ↾}_{S}) (⋃ x) = \underset{y \in x}{\sum^{*}} ({\|.\| ↾}_{S}) (y))))$
36	5 10 34 35	mpbir3and	$⊢ S \in ⋃ ran sigAlgebra \to {\|.\| ↾}_{S} \in measures (S)$

Metamath Proof Explorer

Theorem cntmeas

Proof