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 
|- ( ph -> X e. V )
psmeasure.h 
|- ( ph -> H : X --> ( 0 [,] +oo ) )
psmeasure.m 
|- M = ( x e. ~P X |-> ( sum^ ` ( H |` x ) ) )
Assertion psmeasure 
|- ( ph -> M e. Meas )

Proof

Step Hyp Ref Expression
1 psmeasure.x 
 |-  ( ph -> X e. V )
2 psmeasure.h 
 |-  ( ph -> H : X --> ( 0 [,] +oo ) )
3 psmeasure.m 
 |-  M = ( x e. ~P X |-> ( sum^ ` ( H |` x ) ) )
4 simpr 
 |-  ( ( ph /\ x e. ~P X ) -> x e. ~P X )
5 2 adantr 
 |-  ( ( ph /\ x e. ~P X ) -> H : X --> ( 0 [,] +oo ) )
6 4 elpwid 
 |-  ( ( ph /\ x e. ~P X ) -> x C_ X )
7 fssres 
 |-  ( ( H : X --> ( 0 [,] +oo ) /\ x C_ X ) -> ( H |` x ) : x --> ( 0 [,] +oo ) )
8 5 6 7 syl2anc 
 |-  ( ( ph /\ x e. ~P X ) -> ( H |` x ) : x --> ( 0 [,] +oo ) )
9 4 8 sge0cl 
 |-  ( ( ph /\ x e. ~P X ) -> ( sum^ ` ( H |` x ) ) e. ( 0 [,] +oo ) )
10 9 3 fmptd 
 |-  ( ph -> M : ~P X --> ( 0 [,] +oo ) )
11 3 9 dmmptd 
 |-  ( ph -> dom M = ~P X )
12 11 feq2d 
 |-  ( ph -> ( M : dom M --> ( 0 [,] +oo ) <-> M : ~P X --> ( 0 [,] +oo ) ) )
13 10 12 mpbird 
 |-  ( ph -> M : dom M --> ( 0 [,] +oo ) )
14 pwsal 
 |-  ( X e. V -> ~P X e. SAlg )
15 1 14 syl 
 |-  ( ph -> ~P X e. SAlg )
16 11 15 eqeltrd 
 |-  ( ph -> dom M e. SAlg )
17 13 16 jca 
 |-  ( ph -> ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) )
18 reseq2 
 |-  ( x = (/) -> ( H |` x ) = ( H |` (/) ) )
19 18 fveq2d 
 |-  ( x = (/) -> ( sum^ ` ( H |` x ) ) = ( sum^ ` ( H |` (/) ) ) )
20 0elpw 
 |-  (/) e. ~P X
21 20 a1i 
 |-  ( ph -> (/) e. ~P X )
22 fvexd 
 |-  ( ph -> ( sum^ ` ( H |` (/) ) ) e. _V )
23 3 19 21 22 fvmptd3 
 |-  ( ph -> ( M ` (/) ) = ( sum^ ` ( H |` (/) ) ) )
24 res0 
 |-  ( H |` (/) ) = (/)
25 24 fveq2i 
 |-  ( sum^ ` ( H |` (/) ) ) = ( sum^ ` (/) )
26 sge00 
 |-  ( sum^ ` (/) ) = 0
27 25 26 eqtri 
 |-  ( sum^ ` ( H |` (/) ) ) = 0
28 27 a1i 
 |-  ( ph -> ( sum^ ` ( H |` (/) ) ) = 0 )
29 23 28 eqtrd 
 |-  ( ph -> ( M ` (/) ) = 0 )
30 simpl 
 |-  ( ( ph /\ y e. ~P dom M ) -> ph )
31 simpr 
 |-  ( ( ph /\ y e. ~P dom M ) -> y e. ~P dom M )
32 11 pweqd 
 |-  ( ph -> ~P dom M = ~P ~P X )
33 32 adantr 
 |-  ( ( ph /\ y e. ~P dom M ) -> ~P dom M = ~P ~P X )
34 31 33 eleqtrd 
 |-  ( ( ph /\ y e. ~P dom M ) -> y e. ~P ~P X )
35 elpwi 
 |-  ( y e. ~P ~P X -> y C_ ~P X )
36 34 35 syl 
 |-  ( ( ph /\ y e. ~P dom M ) -> y C_ ~P X )
37 1 ad2antrr 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> X e. V )
38 2 ad2antrr 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> H : X --> ( 0 [,] +oo ) )
39 10 ad2antrr 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> M : ~P X --> ( 0 [,] +oo ) )
40 simplr 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> y C_ ~P X )
41 id 
 |-  ( w = z -> w = z )
42 41 cbvdisjv 
 |-  ( Disj_ w e. y w <-> Disj_ z e. y z )
43 42 biimpi 
 |-  ( Disj_ w e. y w -> Disj_ z e. y z )
44 43 adantl 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> Disj_ z e. y z )
45 37 38 3 39 40 44 psmeasurelem 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) )
46 45 adantrl 
 |-  ( ( ( ph /\ y C_ ~P X ) /\ ( y ~<_ _om /\ Disj_ w e. y w ) ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) )
47 46 ex 
 |-  ( ( ph /\ y C_ ~P X ) -> ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) )
48 30 36 47 syl2anc 
 |-  ( ( ph /\ y e. ~P dom M ) -> ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) )
49 48 ralrimiva 
 |-  ( ph -> A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) )
50 17 29 49 jca31 
 |-  ( ph -> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) ) )
51 ismea 
 |-  ( M e. Meas <-> ( ( ( M : dom M --> ( 0 [,] +oo ) /\ dom M e. SAlg ) /\ ( M ` (/) ) = 0 ) /\ A. y e. ~P dom M ( ( y ~<_ _om /\ Disj_ w e. y w ) -> ( M ` U. y ) = ( sum^ ` ( M |` y ) ) ) ) )
52 50 51 sylibr 
 |-  ( ph -> M e. Meas )