cndprob01

Description: The conditional probability has values in [ 0 , 1 ] . (Contributed by Thierry Arnoux, 13-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

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

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	adantr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to cProb (P) (⟨A, B⟩) = \frac{P (A \cap B)}{P (B)}$
3		simpl1	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P \in Prob$
4		domprobmeas	$⊢ P \in Prob \to P \in measures (dom P)$
5	3 4	syl	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P \in measures (dom P)$
6		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
7	3 6	syl	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to dom P \in ⋃ ran sigAlgebra$
8		simpl2	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to A \in dom P$
9		simpl3	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to B \in dom P$
10		inelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land A \in dom P \land B \in dom P) \to A \cap B \in dom P$
11	7 8 9 10	syl3anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to A \cap B \in dom P$
12		inss2	$⊢ A \cap B \subseteq B$
13	12	a1i	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to A \cap B \subseteq B$
14	5 11 9 13	measssd	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (A \cap B) \leq P (B)$
15		prob01	$⊢ (P \in Prob \land A \cap B \in dom P) \to P (A \cap B) \in [0, 1]$
16	3 11 15	syl2anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (A \cap B) \in [0, 1]$
17		prob01	$⊢ (P \in Prob \land B \in dom P) \to P (B) \in [0, 1]$
18	3 9 17	syl2anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (B) \in [0, 1]$
19		simpr	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to P (B) \neq 0$
20		unitdivcld	$⊢ (P (A \cap B) \in [0, 1] \land P (B) \in [0, 1] \land P (B) \neq 0) \to (P (A \cap B) \leq P (B) \leftrightarrow \frac{P (A \cap B)}{P (B)} \in [0, 1])$
21	16 18 19 20	syl3anc	$⊢ ((P \in Prob \land A \in dom P \land B \in dom P) \land P (B) \neq 0) \to (P (A \cap B) \leq P (B) \leftrightarrow \frac{P (A \cap B)}{P (B)} \in [0, 1])$
22	14 21	mpbid	$⊢ ((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)} \in [0, 1]$
23	2 22	eqeltrd	$⊢ ((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]$

Metamath Proof Explorer

Theorem cndprob01

Proof