cndprobval

Description: The value of the conditional probability , i.e. the probability for the event A , given B , under the probability law P . (Contributed by Thierry Arnoux, 21-Jan-2017)

		Ref	Expression
	Assertion	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)}$

Proof

Step	Hyp	Ref	Expression
1		df-ov	$⊢ A cProb (P) B = cProb (P) (⟨A, B⟩)$
2		df-cndprob	$⊢ cProb = (p \in Prob ⟼ (a \in dom p, b \in dom p ⟼ \frac{p (a \cap b)}{p (b)}))$
3		dmeq	$⊢ p = P \to dom p = dom P$
4		fveq1	$⊢ p = P \to p (a \cap b) = P (a \cap b)$
5		fveq1	$⊢ p = P \to p (b) = P (b)$
6	4 5	oveq12d	$⊢ p = P \to \frac{p (a \cap b)}{p (b)} = \frac{P (a \cap b)}{P (b)}$
7	3 3 6	mpoeq123dv	$⊢ p = P \to (a \in dom p, b \in dom p ⟼ \frac{p (a \cap b)}{p (b)}) = (a \in dom P, b \in dom P ⟼ \frac{P (a \cap b)}{P (b)})$
8		id	$⊢ P \in Prob \to P \in Prob$
9		dmexg	$⊢ P \in Prob \to dom P \in V$
10		mpoexga	$⊢ (dom P \in V \land dom P \in V) \to (a \in dom P, b \in dom P ⟼ \frac{P (a \cap b)}{P (b)}) \in V$
11	9 9 10	syl2anc	$⊢ P \in Prob \to (a \in dom P, b \in dom P ⟼ \frac{P (a \cap b)}{P (b)}) \in V$
12	2 7 8 11	fvmptd3	$⊢ P \in Prob \to cProb (P) = (a \in dom P, b \in dom P ⟼ \frac{P (a \cap b)}{P (b)})$
13	12	3ad2ant1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to cProb (P) = (a \in dom P, b \in dom P ⟼ \frac{P (a \cap b)}{P (b)})$
14		simprl	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to a = A$
15		simprr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to b = B$
16	14 15	ineq12d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to a \cap b = A \cap B$
17	16	fveq2d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to P (a \cap b) = P (A \cap B)$
18	15	fveq2d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to P (b) = P (B)$
19	17 18	oveq12d	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land (a = A \land b = B)) \to \frac{P (a \cap b)}{P (b)} = \frac{P (A \cap B)}{P (B)}$
20		simp2	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to A \in dom P$
21		simp3	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to B \in dom P$
22		ovexd	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to \frac{P (A \cap B)}{P (B)} \in V$
23	13 19 20 21 22	ovmpod	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to A cProb (P) B = \frac{P (A \cap B)}{P (B)}$
24	1 23	eqtr3id	$⊢ (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)}$

Metamath Proof Explorer

Theorem cndprobval

Proof