cndprobprob

Description: The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

		Ref	Expression
	Assertion	cndprobprob	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to (a \in dom P ⟼ cProb (P) (⟨a, B⟩)) \in Prob$

Proof

Step	Hyp	Ref	Expression
1		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
2	1	3ad2ant1	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to P \in measures (dom P)$
3		simp2	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to B \in dom P$
4		prob01	$⊢ (P \in Prob \land B \in dom P) \to P (B) \in [0, 1]$
5	4	3adant3	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to P (B) \in [0, 1]$
6		elunitrn	$⊢ P (B) \in [0, 1] \to P (B) \in ℝ$
7	5 6	syl	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to P (B) \in ℝ$
8		elunitge0	$⊢ P (B) \in [0, 1] \to 0 \leq P (B)$
9	5 8	syl	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to 0 \leq P (B)$
10		simp3	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to P (B) \neq 0$
11	7 9 10	ne0gt0d	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to 0 < P (B)$
12	7 11	elrpd	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to P (B) \in ℝ^{+}$
13		probmeasb	$⊢ (P \in measures (dom P) \land B \in dom P \land P (B) \in ℝ^{+}) \to (a \in dom P ⟼ \frac{P (a \cap B)}{P (B)}) \in Prob$
14	2 3 12 13	syl3anc	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to (a \in dom P ⟼ \frac{P (a \cap B)}{P (B)}) \in Prob$
15		3anan32	$⊢ (P \in Prob \land a \in dom P \land B \in dom P) \leftrightarrow ((P \in Prob \land B \in dom P) \land a \in dom P)$
16		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)}$
17	15 16	sylbir	$⊢ ((P \in Prob \land B \in dom P) \land a \in dom P) \to cProb (P) (⟨a, B⟩) = \frac{P (a \cap B)}{P (B)}$
18	17	mpteq2dva	$⊢ (P \in Prob \land B \in dom P) \to (a \in dom P ⟼ cProb (P) (⟨a, B⟩)) = (a \in dom P ⟼ \frac{P (a \cap B)}{P (B)})$
19	18	eleq1d	$⊢ (P \in Prob \land B \in dom P) \to ((a \in dom P ⟼ cProb (P) (⟨a, B⟩)) \in Prob \leftrightarrow (a \in dom P ⟼ \frac{P (a \cap B)}{P (B)}) \in Prob)$
20	19	3adant3	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to ((a \in dom P ⟼ cProb (P) (⟨a, B⟩)) \in Prob \leftrightarrow (a \in dom P ⟼ \frac{P (a \cap B)}{P (B)}) \in Prob)$
21	14 20	mpbird	$⊢ (P \in Prob \land B \in dom P \land P (B) \neq 0) \to (a \in dom P ⟼ cProb (P) (⟨a, B⟩)) \in Prob$

Metamath Proof Explorer

Theorem cndprobprob

Proof