Metamath Proof Explorer

Theorem cndprobnul

Description: The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> P e. Prob )
2 nuleldmp 
 |-  ( P e. Prob -> (/) e. dom P )
3 1 2 syl 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> (/) e. dom P )
4 simp2 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> A e. dom P )
5 cndprobval 
 |-  ( ( P e. Prob /\ (/) e. dom P /\ A e. dom P ) -> ( ( cprob ` P ) ` <. (/) , A >. ) = ( ( P ` ( (/) i^i A ) ) / ( P ` A ) ) )
6 1 3 4 5 syl3anc 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( cprob ` P ) ` <. (/) , A >. ) = ( ( P ` ( (/) i^i A ) ) / ( P ` A ) ) )
7 0in 
 |-  ( (/) i^i A ) = (/)
8 7 fveq2i 
 |-  ( P ` ( (/) i^i A ) ) = ( P ` (/) )
9 8 oveq1i 
 |-  ( ( P ` ( (/) i^i A ) ) / ( P ` A ) ) = ( ( P ` (/) ) / ( P ` A ) )
10 9 a1i 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( P ` ( (/) i^i A ) ) / ( P ` A ) ) = ( ( P ` (/) ) / ( P ` A ) ) )
11 probnul 
 |-  ( P e. Prob -> ( P ` (/) ) = 0 )
12 1 11 syl 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` (/) ) = 0 )
13 12 oveq1d 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( P ` (/) ) / ( P ` A ) ) = ( 0 / ( P ` A ) ) )
14 prob01 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )
15 14 3adant3 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) e. ( 0 [,] 1 ) )
16 elunitcn 
 |-  ( ( P ` A ) e. ( 0 [,] 1 ) -> ( P ` A ) e. CC )
17 15 16 syl 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) e. CC )
18 simp3 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) =/= 0 )
19 17 18 div0d 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( 0 / ( P ` A ) ) = 0 )
20 10 13 19 3eqtrd 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( P ` ( (/) i^i A ) ) / ( P ` A ) ) = 0 )
21 6 20 eqtrd 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( cprob ` P ) ` <. (/) , A >. ) = 0 )