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 \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)$

Proof

Step	Hyp	Ref	Expression
1		cndprobval	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to cProb (P) (⟨A, B⟩) = \frac{P (A \cap B)}{P (B)}$
2	1	oveq1d	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to cProb (P) (⟨A, B⟩) P (B) = (\frac{P (A \cap B)}{P (B)}) P (B)$
3	2	adantr	$⊢ ((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) = (\frac{P (A \cap B)}{P (B)}) P (B)$
4		unitsscn	$⊢ [0, 1] \subseteq ℂ$
5		simp1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P \in Prob$
6		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
7		inelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land A \in dom P \land B \in dom P) \to A \cap B \in dom P$
8	6 7	syl3an1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to A \cap B \in dom P$
9		prob01	$⊢ (P \in Prob \land A \cap B \in dom P) \to P (A \cap B) \in [0, 1]$
10	5 8 9	syl2anc	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A \cap B) \in [0, 1]$
11	4 10	sseldi	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A \cap B) \in ℂ$
12	11	adantr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (A \cap B) \in ℂ$
13		prob01	$⊢ (P \in Prob \land B \in dom P) \to P (B) \in [0, 1]$
14	13	3adant2	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (B) \in [0, 1]$
15	4 14	sseldi	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (B) \in ℂ$
16	15	adantr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (B) \in ℂ$
17		simpr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (B) \neq 0$
18	12 16 17	divcan1d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to (\frac{P (A \cap B)}{P (B)}) P (B) = P (A \cap B)$
19	3 18	eqtrd	$⊢ ((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)$