Metamath Proof Explorer

Theorem cndprobin

Description: An identity linking conditional probability and intersection. (Contributed by Thierry Arnoux, 13-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprobin 
|- ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( P ` ( A i^i B ) ) )

Proof

Step Hyp Ref Expression
1 cndprobval 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
2 1 oveq1d 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( ( ( P ` ( A i^i B ) ) / ( P ` B ) ) x. ( P ` B ) ) )
3 2 adantr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( ( ( P ` ( A i^i B ) ) / ( P ` B ) ) x. ( P ` B ) ) )
4 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
5 simp1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> P e. Prob )
6 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
7 inelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ A e. dom P /\ B e. dom P ) -> ( A i^i B ) e. dom P )
8 6 7 syl3an1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( A i^i B ) e. dom P )
9 prob01 
 |-  ( ( P e. Prob /\ ( A i^i B ) e. dom P ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
10 5 8 9 syl2anc 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
11 4 10 sselid 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A i^i B ) ) e. CC )
12 11 adantr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` ( A i^i B ) ) e. CC )
13 prob01 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
14 13 3adant2 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
15 4 14 sselid 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` B ) e. CC )
16 15 adantr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. CC )
17 simpr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( P ` B ) =/= 0 )
18 12 16 17 divcan1d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( ( P ` ( A i^i B ) ) / ( P ` B ) ) x. ( P ` B ) ) = ( P ` ( A i^i B ) ) )
19 3 18 eqtrd 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( P ` ( A i^i B ) ) )