Theorem psmeasure

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

	Ref	Expression
Hypotheses	psmeasure.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
	psmeasure.h	⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
	psmeasure.m	⊢ 𝑀 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) )
Assertion	psmeasure	⊢ ( 𝜑 → 𝑀 ∈ Meas )

Proof

Step	Hyp	Ref	Expression
1		psmeasure.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
2		psmeasure.h	⊢ ( 𝜑 → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
3		psmeasure.m	⊢ 𝑀 = ( 𝑥 ∈ 𝒫 𝑋 ↦ ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) )
4		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ∈ 𝒫 𝑋 )
5	2	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
6	4	elpwid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑋 ) → 𝑥 ⊆ 𝑋 )
7		fssres	⊢ ( ( 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) ∧ 𝑥 ⊆ 𝑋 ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
8	5 6 7	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( 𝐻 ↾ 𝑥 ) : 𝑥 ⟶ ( 0 [,] +∞ ) )
9	4 8	sge0cl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝒫 𝑋 ) → ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) ∈ ( 0 [,] +∞ ) )
10	9 3	fmptd	⊢ ( 𝜑 → 𝑀 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
11	3 9	dmmptd	⊢ ( 𝜑 → dom 𝑀 = 𝒫 𝑋 )
12	11	feq2d	⊢ ( 𝜑 → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ↔ 𝑀 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) ) )
13	10 12	mpbird	⊢ ( 𝜑 → 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) )
14		pwsal	⊢ ( 𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ SAlg )
15	1 14	syl	⊢ ( 𝜑 → 𝒫 𝑋 ∈ SAlg )
16	11 15	eqeltrd	⊢ ( 𝜑 → dom 𝑀 ∈ SAlg )
17	13 16	jca	⊢ ( 𝜑 → ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) )
18		reseq2	⊢ ( 𝑥 = ∅ → ( 𝐻 ↾ 𝑥 ) = ( 𝐻 ↾ ∅ ) )
19	18	fveq2d	⊢ ( 𝑥 = ∅ → ( Σ^ ‘ ( 𝐻 ↾ 𝑥 ) ) = ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) )
20		0elpw	⊢ ∅ ∈ 𝒫 𝑋
21	20	a1i	⊢ ( 𝜑 → ∅ ∈ 𝒫 𝑋 )
22		fvexd	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) ∈ V )
23	3 19 21 22	fvmptd3	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) )
24		res0	⊢ ( 𝐻 ↾ ∅ ) = ∅
25	24	fveq2i	⊢ ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) = ( Σ^ ‘ ∅ )
26		sge00	⊢ ( Σ^ ‘ ∅ ) = 0
27	25 26	eqtri	⊢ ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) = 0
28	27	a1i	⊢ ( 𝜑 → ( Σ^ ‘ ( 𝐻 ↾ ∅ ) ) = 0 )
29	23 28	eqtrd	⊢ ( 𝜑 → ( 𝑀 ‘ ∅ ) = 0 )
30		simpl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → 𝜑 )
31		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → 𝑦 ∈ 𝒫 dom 𝑀 )
32	11	pweqd	⊢ ( 𝜑 → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋 )
33	32	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → 𝒫 dom 𝑀 = 𝒫 𝒫 𝑋 )
34	31 33	eleqtrd	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → 𝑦 ∈ 𝒫 𝒫 𝑋 )
35		elpwi	⊢ ( 𝑦 ∈ 𝒫 𝒫 𝑋 → 𝑦 ⊆ 𝒫 𝑋 )
36	34 35	syl	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → 𝑦 ⊆ 𝒫 𝑋 )
37	1	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → 𝑋 ∈ 𝑉 )
38	2	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → 𝐻 : 𝑋 ⟶ ( 0 [,] +∞ ) )
39	10	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → 𝑀 : 𝒫 𝑋 ⟶ ( 0 [,] +∞ ) )
40		simplr	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → 𝑦 ⊆ 𝒫 𝑋 )
41		id	⊢ ( 𝑤 = 𝑧 → 𝑤 = 𝑧 )
42	41	cbvdisjv	⊢ ( Disj 𝑤 ∈ 𝑦 𝑤 ↔ Disj 𝑧 ∈ 𝑦 𝑧 )
43	42	bilani	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → Disj 𝑧 ∈ 𝑦 𝑧 )
44	37 38 3 39 40 43	psmeasurelem	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) )
45	44	adantrl	⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) )
46	45	ex	⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
47	30 36 46	syl2anc	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
48	47	ralrimiva	⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
49	17 29 48	jca31	⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
50		ismea	⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
51	49 50	sylibr	⊢ ( 𝜑 → 𝑀 ∈ Meas )