Metamath Proof Explorer

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 biimpi ⊢ ( Disj 𝑤 ∈ 𝑦 𝑤 → Disj 𝑧 ∈ 𝑦 𝑧 )
44 43 adantl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → Disj 𝑧 ∈ 𝑦 𝑧 )
45 37 38 3 39 40 44 psmeasurelem ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) )
46 45 adantrl ⊢ ( ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) ∧ ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) )
47 46 ex ⊢ ( ( 𝜑 ∧ 𝑦 ⊆ 𝒫 𝑋 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
48 30 36 47 syl2anc ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝒫 dom 𝑀 ) → ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
49 48 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) )
50 17 29 49 jca31 ⊢ ( 𝜑 → ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
51 ismea ⊢ ( 𝑀 ∈ Meas ↔ ( ( ( 𝑀 : dom 𝑀 ⟶ ( 0 [,] +∞ ) ∧ dom 𝑀 ∈ SAlg ) ∧ ( 𝑀 ‘ ∅ ) = 0 ) ∧ ∀ 𝑦 ∈ 𝒫 dom 𝑀 ( ( 𝑦 ≼ ω ∧ Disj 𝑤 ∈ 𝑦 𝑤 ) → ( 𝑀 ‘ ∪ 𝑦 ) = ( Σ^ ‘ ( 𝑀 ↾ 𝑦 ) ) ) ) )
52 50 51 sylibr ⊢ ( 𝜑 → 𝑀 ∈ Meas )