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 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) / ( 𝑃 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
2 cndprob01 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 0 [,] 1 ) )
3 2 3adant2 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 0 [,] 1 ) )
4 1 3 sseldi ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ℂ )
5 simp11 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝑃 ∈ Prob )
6 simp13 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝐵 ∈ dom 𝑃 )
7 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
8 5 6 7 syl2anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
9 1 8 sseldi ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℂ )
10 simp3 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ≠ 0 )
11 4 9 10 divcan4d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) = ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) )
12 incom ⊢ ( 𝐴 ∩ 𝐵 ) = ( 𝐵 ∩ 𝐴 )
13 12 fveq2i ⊢ ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐵 ∩ 𝐴 ) )
14 cndprobin ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )
15 14 3adant2 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )
16 simp12 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝐴 ∈ dom 𝑃 )
17 simp2 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ≠ 0 )
18 cndprobin ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) = ( 𝑃 ‘ ( 𝐵 ∩ 𝐴 ) ) )
19 5 6 16 17 18 syl31anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) = ( 𝑃 ‘ ( 𝐵 ∩ 𝐴 ) ) )
20 13 15 19 3eqtr4a ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) = ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) )
21 20 oveq1d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) · ( 𝑃 ‘ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) = ( ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
22 11 21 eqtr3d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐵 , 𝐴 ⟩ ) · ( 𝑃 ‘ 𝐴 ) ) / ( 𝑃 ‘ 𝐵 ) ) )