Metamath Proof Explorer

Theorem ismeas

Description: The property of being a measure. (Contributed by Thierry Arnoux, 10-Sep-2016) (Revised by Thierry Arnoux, 19-Oct-2016)

Ref Expression
Assertion ismeas 
|- ( S e. U. ran sigAlgebra -> ( M e. ( measures ` S ) <-> ( 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 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elex 
 |-  ( M e. ( measures ` S ) -> M e. _V )
2 1 a1i 
 |-  ( S e. U. ran sigAlgebra -> ( M e. ( measures ` S ) -> M e. _V ) )
3 simp1 
 |-  ( ( 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 ) ) ) -> M : S --> ( 0 [,] +oo ) )
4 ovex 
 |-  ( 0 [,] +oo ) e. _V
5 fex2 
 |-  ( ( M : S --> ( 0 [,] +oo ) /\ S e. U. ran sigAlgebra /\ ( 0 [,] +oo ) e. _V ) -> M e. _V )
6 5 3expb 
 |-  ( ( M : S --> ( 0 [,] +oo ) /\ ( S e. U. ran sigAlgebra /\ ( 0 [,] +oo ) e. _V ) ) -> M e. _V )
7 6 expcom 
 |-  ( ( S e. U. ran sigAlgebra /\ ( 0 [,] +oo ) e. _V ) -> ( M : S --> ( 0 [,] +oo ) -> M e. _V ) )
8 4 7 mpan2 
 |-  ( S e. U. ran sigAlgebra -> ( M : S --> ( 0 [,] +oo ) -> M e. _V ) )
9 3 8 syl5 
 |-  ( S e. U. ran sigAlgebra -> ( ( 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 ) ) ) -> M e. _V ) )
10 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 ) ) ) } )
11 vex 
 |-  s e. _V
12 mapex 
 |-  ( ( s e. _V /\ ( 0 [,] +oo ) e. _V ) -> { m | m : s --> ( 0 [,] +oo ) } e. _V )
13 11 4 12 mp2an 
 |-  { m | m : s --> ( 0 [,] +oo ) } e. _V
14 simp1 
 |-  ( ( 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 ) ) ) -> m : s --> ( 0 [,] +oo ) )
15 14 ss2abi 
 |-  { 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 ) ) ) } C_ { m | m : s --> ( 0 [,] +oo ) }
16 13 15 ssexi 
 |-  { 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 ) ) ) } e. _V
17 simpr 
 |-  ( ( s = S /\ m = M ) -> m = M )
18 simpl 
 |-  ( ( s = S /\ m = M ) -> s = S )
19 17 18 feq12d 
 |-  ( ( s = S /\ m = M ) -> ( m : s --> ( 0 [,] +oo ) <-> M : S --> ( 0 [,] +oo ) ) )
20 fveq1 
 |-  ( m = M -> ( m ` (/) ) = ( M ` (/) ) )
21 20 eqeq1d 
 |-  ( m = M -> ( ( m ` (/) ) = 0 <-> ( M ` (/) ) = 0 ) )
22 21 adantl 
 |-  ( ( s = S /\ m = M ) -> ( ( m ` (/) ) = 0 <-> ( M ` (/) ) = 0 ) )
23 18 pweqd 
 |-  ( ( s = S /\ m = M ) -> ~P s = ~P S )
24 fveq1 
 |-  ( m = M -> ( m ` U. x ) = ( M ` U. x ) )
25 fveq1 
 |-  ( m = M -> ( m ` y ) = ( M ` y ) )
26 25 esumeq2sdv 
 |-  ( m = M -> sum* y e. x ( m ` y ) = sum* y e. x ( M ` y ) )
27 24 26 eqeq12d 
 |-  ( m = M -> ( ( m ` U. x ) = sum* y e. x ( m ` y ) <-> ( M ` U. x ) = sum* y e. x ( M ` y ) ) )
28 27 imbi2d 
 |-  ( m = M -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
29 28 adantl 
 |-  ( ( s = S /\ m = M ) -> ( ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
30 23 29 raleqbidv 
 |-  ( ( s = S /\ m = M ) -> ( A. x e. ~P s ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( m ` U. x ) = sum* y e. x ( m ` y ) ) <-> A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( M ` U. x ) = sum* y e. x ( M ` y ) ) ) )
31 19 22 30 3anbi123d 
 |-  ( ( s = S /\ m = 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 ) ) ) <-> ( 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 ) ) ) ) )
32 10 16 31 abfmpel 
 |-  ( ( S e. U. ran sigAlgebra /\ M e. _V ) -> ( M e. ( measures ` S ) <-> ( 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 ) ) ) ) )
33 32 ex 
 |-  ( S e. U. ran sigAlgebra -> ( M e. _V -> ( M e. ( measures ` S ) <-> ( 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 2 9 33 pm5.21ndd 
 |-  ( S e. U. ran sigAlgebra -> ( M e. ( measures ` S ) <-> ( 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 ) ) ) ) )