Metamath Proof Explorer


Definition df-meas

Description: Define a measure as a nonnegative countably additive function over a sigma-algebra onto ( 0 , +oo ) . (Contributed by Thierry Arnoux, 10-Sep-2016)

Ref Expression
Assertion df-meas measures = ( 𝑠 ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmeas measures
1 vs 𝑠
2 csiga sigAlgebra
3 2 crn ran sigAlgebra
4 3 cuni ran sigAlgebra
5 vm 𝑚
6 5 cv 𝑚
7 1 cv 𝑠
8 cc0 0
9 cicc [,]
10 cpnf +∞
11 8 10 9 co ( 0 [,] +∞ )
12 7 11 6 wf 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ )
13 c0
14 13 6 cfv ( 𝑚 ‘ ∅ )
15 14 8 wceq ( 𝑚 ‘ ∅ ) = 0
16 vx 𝑥
17 7 cpw 𝒫 𝑠
18 16 cv 𝑥
19 cdom
20 com ω
21 18 20 19 wbr 𝑥 ≼ ω
22 vy 𝑦
23 22 cv 𝑦
24 22 18 23 wdisj Disj 𝑦𝑥 𝑦
25 21 24 wa ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 )
26 18 cuni 𝑥
27 26 6 cfv ( 𝑚 𝑥 )
28 23 6 cfv ( 𝑚𝑦 )
29 18 28 22 cesum Σ* 𝑦𝑥 ( 𝑚𝑦 )
30 27 29 wceq ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 )
31 25 30 wi ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) )
32 31 16 17 wral 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) )
33 12 15 32 w3a ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) )
34 33 5 cab { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) }
35 1 4 34 cmpt ( 𝑠 ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } )
36 0 35 wceq measures = ( 𝑠 ran sigAlgebra ↦ { 𝑚 ∣ ( 𝑚 : 𝑠 ⟶ ( 0 [,] +∞ ) ∧ ( 𝑚 ‘ ∅ ) = 0 ∧ ∀ 𝑥 ∈ 𝒫 𝑠 ( ( 𝑥 ≼ ω ∧ Disj 𝑦𝑥 𝑦 ) → ( 𝑚 𝑥 ) = Σ* 𝑦𝑥 ( 𝑚𝑦 ) ) ) } )