Metamath Proof Explorer

Theorem cndprobprob

Description: The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprobprob 
|- ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( a e. dom P |-> ( ( cprob ` P ) ` <. a , B >. ) ) e. Prob )

Proof

Step Hyp Ref Expression
1 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
2 1 3ad2ant1 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> P e. ( measures ` dom P ) )
3 simp2 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> B e. dom P )
4 prob01 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
5 4 3adant3 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. ( 0 [,] 1 ) )
6 elunitrn 
 |-  ( ( P ` B ) e. ( 0 [,] 1 ) -> ( P ` B ) e. RR )
7 5 6 syl 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. RR )
8 elunitge0 
 |-  ( ( P ` B ) e. ( 0 [,] 1 ) -> 0 <_ ( P ` B ) )
9 5 8 syl 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> 0 <_ ( P ` B ) )
10 simp3 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( P ` B ) =/= 0 )
11 7 9 10 ne0gt0d 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> 0 < ( P ` B ) )
12 7 11 elrpd 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. RR+ )
13 probmeasb 
 |-  ( ( P e. ( measures ` dom P ) /\ B e. dom P /\ ( P ` B ) e. RR+ ) -> ( a e. dom P |-> ( ( P ` ( a i^i B ) ) / ( P ` B ) ) ) e. Prob )
14 2 3 12 13 syl3anc 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( a e. dom P |-> ( ( P ` ( a i^i B ) ) / ( P ` B ) ) ) e. Prob )
15 3anan32 
 |-  ( ( P e. Prob /\ a e. dom P /\ B e. dom P ) <-> ( ( P e. Prob /\ B e. dom P ) /\ a e. dom P ) )
16 cndprobval 
 |-  ( ( P e. Prob /\ a e. dom P /\ B e. dom P ) -> ( ( cprob ` P ) ` <. a , B >. ) = ( ( P ` ( a i^i B ) ) / ( P ` B ) ) )
17 15 16 sylbir 
 |-  ( ( ( P e. Prob /\ B e. dom P ) /\ a e. dom P ) -> ( ( cprob ` P ) ` <. a , B >. ) = ( ( P ` ( a i^i B ) ) / ( P ` B ) ) )
18 17 mpteq2dva 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( a e. dom P |-> ( ( cprob ` P ) ` <. a , B >. ) ) = ( a e. dom P |-> ( ( P ` ( a i^i B ) ) / ( P ` B ) ) ) )
19 18 eleq1d 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( ( a e. dom P |-> ( ( cprob ` P ) ` <. a , B >. ) ) e. Prob <-> ( a e. dom P |-> ( ( P ` ( a i^i B ) ) / ( P ` B ) ) ) e. Prob ) )
20 19 3adant3 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( ( a e. dom P |-> ( ( cprob ` P ) ` <. a , B >. ) ) e. Prob <-> ( a e. dom P |-> ( ( P ` ( a i^i B ) ) / ( P ` B ) ) ) e. Prob ) )
21 14 20 mpbird 
 |-  ( ( P e. Prob /\ B e. dom P /\ ( P ` B ) =/= 0 ) -> ( a e. dom P |-> ( ( cprob ` P ) ` <. a , B >. ) ) e. Prob )