Metamath Proof Explorer

Theorem bayesth

Description: Bayes Theorem. (Contributed by Thierry Arnoux, 20-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

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

Proof

Step Hyp Ref Expression
1 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
2 cndprob01 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) e. ( 0 [,] 1 ) )
3 2 3adant2 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) e. ( 0 [,] 1 ) )
4 1 3 sseldi 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) e. CC )
5 simp11 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> P e. Prob )
6 simp13 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> B e. dom P )
7 prob01 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
8 5 6 7 syl2anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. ( 0 [,] 1 ) )
9 1 8 sseldi 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( P ` B ) e. CC )
10 simp3 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( P ` B ) =/= 0 )
11 4 9 10 divcan4d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) / ( P ` B ) ) = ( ( cprob ` P ) ` <. A , B >. ) )
12 incom 
 |-  ( A i^i B ) = ( B i^i A )
13 12 fveq2i 
 |-  ( P ` ( A i^i B ) ) = ( P ` ( B i^i A ) )
14 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 ) ) )
15 14 3adant2 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( P ` ( A i^i B ) ) )
16 simp12 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> A e. dom P )
17 simp2 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( P ` A ) =/= 0 )
18 cndprobin 
 |-  ( ( ( P e. Prob /\ B e. dom P /\ A e. dom P ) /\ ( P ` A ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) = ( P ` ( B i^i A ) ) )
19 5 6 16 17 18 syl31anc 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) = ( P ` ( B i^i A ) ) )
20 13 15 19 3eqtr4a 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) = ( ( ( cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) )
21 20 oveq1d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( ( ( cprob ` P ) ` <. A , B >. ) x. ( P ` B ) ) / ( P ` B ) ) = ( ( ( ( cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) / ( P ` B ) ) )
22 11 21 eqtr3d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( P ` A ) =/= 0 /\ ( P ` B ) =/= 0 ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( ( ( cprob ` P ) ` <. B , A >. ) x. ( P ` A ) ) / ( P ` B ) ) )