Metamath Proof Explorer

Theorem probfinmeasb

Description: Build a probability measure from a finite measure. (Contributed by Thierry Arnoux, 31-Jan-2017)

Ref Expression
Assertion probfinmeasb 
|- ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) e. Prob )

Proof

Step Hyp Ref Expression
1 measdivcst 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) e. ( measures ` S ) )
2 measfn 
 |-  ( M e. ( measures ` S ) -> M Fn S )
3 2 adantr 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> M Fn S )
4 measbase 
 |-  ( M e. ( measures ` S ) -> S e. U. ran sigAlgebra )
5 4 adantr 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> S e. U. ran sigAlgebra )
6 simpr 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M ` U. S ) e. RR+ )
7 3 5 6 ofcfn 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) Fn S )
8 7 fndmd 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> dom ( M oFC /e ( M ` U. S ) ) = S )
9 8 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( measures ` dom ( M oFC /e ( M ` U. S ) ) ) = ( measures ` S ) )
10 1 9 eleqtrrd 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) e. ( measures ` dom ( M oFC /e ( M ` U. S ) ) ) )
11 measbasedom 
 |-  ( ( M oFC /e ( M ` U. S ) ) e. U. ran measures <-> ( M oFC /e ( M ` U. S ) ) e. ( measures ` dom ( M oFC /e ( M ` U. S ) ) ) )
12 10 11 sylibr 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) e. U. ran measures )
13 8 unieqd 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> U. dom ( M oFC /e ( M ` U. S ) ) = U. S )
14 13 fveq2d 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( M oFC /e ( M ` U. S ) ) ` U. dom ( M oFC /e ( M ` U. S ) ) ) = ( ( M oFC /e ( M ` U. S ) ) ` U. S ) )
15 unielsiga 
 |-  ( S e. U. ran sigAlgebra -> U. S e. S )
16 5 15 syl 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> U. S e. S )
17 eqidd 
 |-  ( ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) /\ U. S e. S ) -> ( M ` U. S ) = ( M ` U. S ) )
18 3 5 6 17 ofcval 
 |-  ( ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) /\ U. S e. S ) -> ( ( M oFC /e ( M ` U. S ) ) ` U. S ) = ( ( M ` U. S ) /e ( M ` U. S ) ) )
19 16 18 mpdan 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( M oFC /e ( M ` U. S ) ) ` U. S ) = ( ( M ` U. S ) /e ( M ` U. S ) ) )
20 rpre 
 |-  ( ( M ` U. S ) e. RR+ -> ( M ` U. S ) e. RR )
21 rpne0 
 |-  ( ( M ` U. S ) e. RR+ -> ( M ` U. S ) =/= 0 )
22 xdivid 
 |-  ( ( ( M ` U. S ) e. RR /\ ( M ` U. S ) =/= 0 ) -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
23 20 21 22 syl2anc 
 |-  ( ( M ` U. S ) e. RR+ -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
24 23 adantl 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( M ` U. S ) /e ( M ` U. S ) ) = 1 )
25 14 19 24 3eqtrd 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( ( M oFC /e ( M ` U. S ) ) ` U. dom ( M oFC /e ( M ` U. S ) ) ) = 1 )
26 elprob 
 |-  ( ( M oFC /e ( M ` U. S ) ) e. Prob <-> ( ( M oFC /e ( M ` U. S ) ) e. U. ran measures /\ ( ( M oFC /e ( M ` U. S ) ) ` U. dom ( M oFC /e ( M ` U. S ) ) ) = 1 ) )
27 12 25 26 sylanbrc 
 |-  ( ( M e. ( measures ` S ) /\ ( M ` U. S ) e. RR+ ) -> ( M oFC /e ( M ` U. S ) ) e. Prob )