bayesth

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

		Ref	Expression
	Assertion	bayesth	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) = \frac{cProb (P) (⟨B, A⟩) P (A)}{P (B)}$

Proof

Step	Hyp	Ref	Expression
1		unitsscn	$⊢ [0, 1] \subseteq ℂ$
2		cndprob01	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) \in [0, 1]$
3	2	3adant2	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) \in [0, 1]$
4	1 3	sselid	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) \in ℂ$
5		simp11	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to P \in Prob$
6		simp13	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to B \in dom P$
7		prob01	$⊢ (P \in Prob \land B \in dom P) \to P (B) \in [0, 1]$
8	5 6 7	syl2anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to P (B) \in [0, 1]$
9	1 8	sselid	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to P (B) \in ℂ$
10		simp3	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to P (B) \neq 0$
11	4 9 10	divcan4d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to \frac{cProb (P) (⟨A, B⟩) P (B)}{P (B)} = cProb (P) (⟨A, B⟩)$
12		incom	$⊢ A \cap B = B \cap A$
13	12	fveq2i	$⊢ P (A \cap B) = P (B \cap A)$
14		cndprobin	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) P (B) = P (A \cap B)$
15	14	3adant2	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) P (B) = P (A \cap B)$
16		simp12	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to A \in dom P$
17		simp2	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to P (A) \neq 0$
18		cndprobin	$⊢ ((P \in Prob \land B \in dom P \land A \in dom P) \land P (A) \neq 0) \to cProb (P) (⟨B, A⟩) P (A) = P (B \cap A)$
19	5 6 16 17 18	syl31anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨B, A⟩) P (A) = P (B \cap A)$
20	13 15 19	3eqtr4a	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) P (B) = cProb (P) (⟨B, A⟩) P (A)$
21	20	oveq1d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to \frac{cProb (P) (⟨A, B⟩) P (B)}{P (B)} = \frac{cProb (P) (⟨B, A⟩) P (A)}{P (B)}$
22	11 21	eqtr3d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (A) \neq 0 \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) = \frac{cProb (P) (⟨B, A⟩) P (A)}{P (B)}$

Metamath Proof Explorer

Theorem bayesth

Proof