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 = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmeas 
 |-  measures
1 vs 
 |-  s
2 csiga 
 |-  sigAlgebra
3 2 crn 
 |-  ran sigAlgebra
4 3 cuni 
 |-  U. ran sigAlgebra
5 vm 
 |-  m
6 5 cv 
 |-  m
7 1 cv 
 |-  s
8 cc0 
 |-  0
9 cicc 
 |-  [,]
10 cpnf 
 |-  +oo
11 8 10 9 co 
 |-  ( 0 [,] +oo )
12 7 11 6 wf 
 |-  m : s --> ( 0 [,] +oo )
13 c0 
 |-  (/)
14 13 6 cfv 
 |-  ( m ` (/) )
15 14 8 wceq 
 |-  ( m ` (/) ) = 0
16 vx 
 |-  x
17 7 cpw 
 |-  ~P s
18 16 cv 
 |-  x
19 cdom 
 |-  ~<_
20 com 
 |-  _om
21 18 20 19 wbr 
 |-  x ~<_ _om
22 vy 
 |-  y
23 22 cv 
 |-  y
24 22 18 23 wdisj 
 |-  Disj_ y e. x y
25 21 24 wa 
 |-  ( x ~<_ _om /\ Disj_ y e. x y )
26 18 cuni 
 |-  U. x
27 26 6 cfv 
 |-  ( m ` U. x )
28 23 6 cfv 
 |-  ( m ` y )
29 18 28 22 cesum 
 |-  sum* y e. x ( m ` y )
30 27 29 wceq 
 |-  ( m ` U. x ) = sum* y e. x ( m ` y )
31 25 30 wi 
 |-  ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) )
32 31 16 17 wral 
 |-  A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) )
33 12 15 32 w3a 
 |-  ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) )
34 33 5 cab 
 |-  { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) }
35 1 4 34 cmpt 
 |-  ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )
36 0 35 wceq 
 |-  measures = ( s e. U. ran sigAlgebra |-> { m | ( m : s --> ( 0 [,] +oo ) /\ ( m ` (/) ) = 0 /\ A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) ) } )