Metamath Proof Explorer

Theorem cndprobtot

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

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( P e. Prob /\ A e. dom P ) -> P e. Prob )
2 1 unveldomd 
 |-  ( ( P e. Prob /\ A e. dom P ) -> U. dom P e. dom P )
3 simpr 
 |-  ( ( P e. Prob /\ A e. dom P ) -> A e. dom P )
4 cndprobval 
 |-  ( ( P e. Prob /\ U. dom P e. dom P /\ A e. dom P ) -> ( ( cprob ` P ) ` <. U. dom P , A >. ) = ( ( P ` ( U. dom P i^i A ) ) / ( P ` A ) ) )
5 1 2 3 4 syl3anc 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( ( cprob ` P ) ` <. U. dom P , A >. ) = ( ( P ` ( U. dom P i^i A ) ) / ( P ` A ) ) )
6 5 3adant3 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( cprob ` P ) ` <. U. dom P , A >. ) = ( ( P ` ( U. dom P i^i A ) ) / ( P ` A ) ) )
7 elssuni 
 |-  ( A e. dom P -> A C_ U. dom P )
8 7 3ad2ant2 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> A C_ U. dom P )
9 sseqin2 
 |-  ( A C_ U. dom P <-> ( U. dom P i^i A ) = A )
10 8 9 sylib 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( U. dom P i^i A ) = A )
11 10 fveq2d 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` ( U. dom P i^i A ) ) = ( P ` A ) )
12 11 oveq1d 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( P ` ( U. dom P i^i A ) ) / ( P ` A ) ) = ( ( P ` A ) / ( P ` A ) ) )
13 prob01 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )
14 13 3adant3 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) e. ( 0 [,] 1 ) )
15 elunitcn 
 |-  ( ( P ` A ) e. ( 0 [,] 1 ) -> ( P ` A ) e. CC )
16 14 15 syl 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) e. CC )
17 simp3 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( P ` A ) =/= 0 )
18 16 17 dividd 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( P ` A ) / ( P ` A ) ) = 1 )
19 6 12 18 3eqtrd 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( P ` A ) =/= 0 ) -> ( ( cprob ` P ) ` <. U. dom P , A >. ) = 1 )