psmeasure

Description: Point supported measure, Remark 112B (d) of Fremlin1 p. 15. (Contributed by Glauco Siliprandi, 17-Aug-2020)

	Ref	Expression
Hypotheses	psmeasure.x	$⊢ φ \to X \in V$
	psmeasure.h	$⊢ φ \to H : X ⟶ [0, +∞]$
	psmeasure.m	$⊢ M = (x \in 𝒫 X ⟼ sum^({H ↾}_{x}))$
Assertion	psmeasure	$⊢ φ \to M \in Meas$

Proof

Step	Hyp	Ref	Expression
1		psmeasure.x	$⊢ φ \to X \in V$
2		psmeasure.h	$⊢ φ \to H : X ⟶ [0, +∞]$
3		psmeasure.m	$⊢ M = (x \in 𝒫 X ⟼ sum^({H ↾}_{x}))$
4		simpr	$⊢ (φ \land x \in 𝒫 X) \to x \in 𝒫 X$
5	2	adantr	$⊢ (φ \land x \in 𝒫 X) \to H : X ⟶ [0, +∞]$
6	4	elpwid	$⊢ (φ \land x \in 𝒫 X) \to x \subseteq X$
7		fssres	$⊢ (H : X ⟶ [0, +∞] \land x \subseteq X) \to ({H ↾}_{x}) : x ⟶ [0, +∞]$
8	5 6 7	syl2anc	$⊢ (φ \land x \in 𝒫 X) \to ({H ↾}_{x}) : x ⟶ [0, +∞]$
9	4 8	sge0cl	$⊢ (φ \land x \in 𝒫 X) \to sum^({H ↾}_{x}) \in [0, +∞]$
10	9 3	fmptd	$⊢ φ \to M : 𝒫 X ⟶ [0, +∞]$
11	3 9	dmmptd	$⊢ φ \to dom M = 𝒫 X$
12	11	feq2d	$⊢ φ \to (M : dom M ⟶ [0, +∞] \leftrightarrow M : 𝒫 X ⟶ [0, +∞])$
13	10 12	mpbird	$⊢ φ \to M : dom M ⟶ [0, +∞]$
14		pwsal	$⊢ X \in V \to 𝒫 X \in SAlg$
15	1 14	syl	$⊢ φ \to 𝒫 X \in SAlg$
16	11 15	eqeltrd	$⊢ φ \to dom M \in SAlg$
17	13 16	jca	$⊢ φ \to (M : dom M ⟶ [0, +∞] \land dom M \in SAlg)$
18		reseq2	$⊢ x = \emptyset \to {H ↾}_{x} = {H ↾}_{\emptyset}$
19	18	fveq2d	$⊢ x = \emptyset \to sum^({H ↾}_{x}) = sum^({H ↾}_{\emptyset})$
20		0elpw	$⊢ \emptyset \in 𝒫 X$
21	20	a1i	$⊢ φ \to \emptyset \in 𝒫 X$
22		fvexd	$⊢ φ \to sum^({H ↾}_{\emptyset}) \in V$
23	3 19 21 22	fvmptd3	$⊢ φ \to M (\emptyset) = sum^({H ↾}_{\emptyset})$
24		res0	$⊢ {H ↾}_{\emptyset} = \emptyset$
25	24	fveq2i	$⊢ sum^({H ↾}_{\emptyset}) = sum^(\emptyset)$
26		sge00	$⊢ sum^(\emptyset) = 0$
27	25 26	eqtri	$⊢ sum^({H ↾}_{\emptyset}) = 0$
28	27	a1i	$⊢ φ \to sum^({H ↾}_{\emptyset}) = 0$
29	23 28	eqtrd	$⊢ φ \to M (\emptyset) = 0$
30		simpl	$⊢ (φ \land y \in 𝒫 dom M) \to φ$
31		simpr	$⊢ (φ \land y \in 𝒫 dom M) \to y \in 𝒫 dom M$
32	11	pweqd	$⊢ φ \to 𝒫 dom M = 𝒫 𝒫 X$
33	32	adantr	$⊢ (φ \land y \in 𝒫 dom M) \to 𝒫 dom M = 𝒫 𝒫 X$
34	31 33	eleqtrd	$⊢ (φ \land y \in 𝒫 dom M) \to y \in 𝒫 𝒫 X$
35		elpwi	$⊢ y \in 𝒫 𝒫 X \to y \subseteq 𝒫 X$
36	34 35	syl	$⊢ (φ \land y \in 𝒫 dom M) \to y \subseteq 𝒫 X$
37	1	ad2antrr	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to X \in V$
38	2	ad2antrr	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to H : X ⟶ [0, +∞]$
39	10	ad2antrr	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to M : 𝒫 X ⟶ [0, +∞]$
40		simplr	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to y \subseteq 𝒫 X$
41		id	$⊢ w = z \to w = z$
42	41	cbvdisjv	$⊢ \underset{w \in y}{Disj} w \leftrightarrow \underset{z \in y}{Disj} z$
43	42	bilani	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to \underset{z \in y}{Disj} z$
44	37 38 3 39 40 43	psmeasurelem	$⊢ ((φ \land y \subseteq 𝒫 X) \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y})$
45	44	adantrl	$⊢ ((φ \land y \subseteq 𝒫 X) \land (y ≼ ω \land \underset{w \in y}{Disj} w)) \to M (⋃ y) = sum^({M ↾}_{y})$
46	45	ex	$⊢ (φ \land y \subseteq 𝒫 X) \to ((y ≼ ω \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y}))$
47	30 36 46	syl2anc	$⊢ (φ \land y \in 𝒫 dom M) \to ((y ≼ ω \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y}))$
48	47	ralrimiva	$⊢ φ \to \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y}))$
49	17 29 48	jca31	$⊢ φ \to (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y})))$
50		ismea	$⊢ M \in Meas \leftrightarrow (((M : dom M ⟶ [0, +∞] \land dom M \in SAlg) \land M (\emptyset) = 0) \land \forall y \in 𝒫 dom M ((y ≼ ω \land \underset{w \in y}{Disj} w) \to M (⋃ y) = sum^({M ↾}_{y})))$
51	49 50	sylibr	$⊢ φ \to M \in Meas$

Metamath Proof Explorer

Theorem psmeasure

Proof