Metamath Proof Explorer

Theorem cntmeas

Description: The Counting measure is a measure on any sigma-algebra. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion cntmeas 
|- ( S e. U. ran sigAlgebra -> ( # |` S ) e. ( measures ` S ) )

Proof

Step Hyp Ref Expression
1 hashf2 
 |-  # : _V --> ( 0 [,] +oo )
2 ssv 
 |-  S C_ _V
3 fssres 
 |-  ( ( # : _V --> ( 0 [,] +oo ) /\ S C_ _V ) -> ( # |` S ) : S --> ( 0 [,] +oo ) )
4 1 2 3 mp2an 
 |-  ( # |` S ) : S --> ( 0 [,] +oo )
5 4 a1i 
 |-  ( S e. U. ran sigAlgebra -> ( # |` S ) : S --> ( 0 [,] +oo ) )
6 0elsiga 
 |-  ( S e. U. ran sigAlgebra -> (/) e. S )
7 fvres 
 |-  ( (/) e. S -> ( ( # |` S ) ` (/) ) = ( # ` (/) ) )
8 6 7 syl 
 |-  ( S e. U. ran sigAlgebra -> ( ( # |` S ) ` (/) ) = ( # ` (/) ) )
9 hash0 
 |-  ( # ` (/) ) = 0
10 8 9 eqtrdi 
 |-  ( S e. U. ran sigAlgebra -> ( ( # |` S ) ` (/) ) = 0 )
11 vex 
 |-  x e. _V
12 hasheuni 
 |-  ( ( x e. _V /\ Disj_ y e. x y ) -> ( # ` U. x ) = sum* y e. x ( # ` y ) )
13 11 12 mpan 
 |-  ( Disj_ y e. x y -> ( # ` U. x ) = sum* y e. x ( # ` y ) )
14 13 ad2antll 
 |-  ( ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( # ` U. x ) = sum* y e. x ( # ` y ) )
15 isrnsigau 
 |-  ( S e. U. ran sigAlgebra -> ( S C_ ~P U. S /\ ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) ) )
16 15 simprd 
 |-  ( S e. U. ran sigAlgebra -> ( U. S e. S /\ A. x e. S ( U. S \ x ) e. S /\ A. x e. ~P S ( x ~<_ _om -> U. x e. S ) ) )
17 16 simp3d 
 |-  ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> U. x e. S ) )
18 fvres 
 |-  ( U. x e. S -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) )
19 18 imim2i 
 |-  ( ( x ~<_ _om -> U. x e. S ) -> ( x ~<_ _om -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) ) )
20 19 ralimi 
 |-  ( A. x e. ~P S ( x ~<_ _om -> U. x e. S ) -> A. x e. ~P S ( x ~<_ _om -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) ) )
21 17 20 syl 
 |-  ( S e. U. ran sigAlgebra -> A. x e. ~P S ( x ~<_ _om -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) ) )
22 21 r19.21bi 
 |-  ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) -> ( x ~<_ _om -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) ) )
23 22 imp 
 |-  ( ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) /\ x ~<_ _om ) -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) )
24 23 adantrr 
 |-  ( ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( ( # |` S ) ` U. x ) = ( # ` U. x ) )
25 elpwi 
 |-  ( x e. ~P S -> x C_ S )
26 25 sseld 
 |-  ( x e. ~P S -> ( y e. x -> y e. S ) )
27 fvres 
 |-  ( y e. S -> ( ( # |` S ) ` y ) = ( # ` y ) )
28 26 27 syl6 
 |-  ( x e. ~P S -> ( y e. x -> ( ( # |` S ) ` y ) = ( # ` y ) ) )
29 28 imp 
 |-  ( ( x e. ~P S /\ y e. x ) -> ( ( # |` S ) ` y ) = ( # ` y ) )
30 29 esumeq2dv 
 |-  ( x e. ~P S -> sum* y e. x ( ( # |` S ) ` y ) = sum* y e. x ( # ` y ) )
31 30 ad2antlr 
 |-  ( ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> sum* y e. x ( ( # |` S ) ` y ) = sum* y e. x ( # ` y ) )
32 14 24 31 3eqtr4d 
 |-  ( ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) /\ ( x ~<_ _om /\ Disj_ y e. x y ) ) -> ( ( # |` S ) ` U. x ) = sum* y e. x ( ( # |` S ) ` y ) )
33 32 ex 
 |-  ( ( S e. U. ran sigAlgebra /\ x e. ~P S ) -> ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( # |` S ) ` U. x ) = sum* y e. x ( ( # |` S ) ` y ) ) )
34 33 ralrimiva 
 |-  ( S e. U. ran sigAlgebra -> A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( # |` S ) ` U. x ) = sum* y e. x ( ( # |` S ) ` y ) ) )
35 ismeas 
 |-  ( S e. U. ran sigAlgebra -> ( ( # |` S ) e. ( measures ` S ) <-> ( ( # |` S ) : S --> ( 0 [,] +oo ) /\ ( ( # |` S ) ` (/) ) = 0 /\ A. x e. ~P S ( ( x ~<_ _om /\ Disj_ y e. x y ) -> ( ( # |` S ) ` U. x ) = sum* y e. x ( ( # |` S ) ` y ) ) ) ) )
36 5 10 34 35 mpbir3and 
 |-  ( S e. U. ran sigAlgebra -> ( # |` S ) e. ( measures ` S ) )