cndprobnul

Description: The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

		Ref	Expression
	Assertion	cndprobnul	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to cProb (P) (⟨\emptyset, A⟩) = 0$

Proof

Step	Hyp	Ref	Expression
1		simp1	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P \in Prob$
2		nuleldmp	$⊢ P \in Prob \to \emptyset \in dom P$
3	1 2	syl	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \emptyset \in dom P$
4		simp2	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to A \in dom P$
5		cndprobval	$⊢ (P \in Prob \land \emptyset \in dom P \land A \in dom P) \to cProb (P) (⟨\emptyset, A⟩) = \frac{P (\emptyset \cap A)}{P (A)}$
6	1 3 4 5	syl3anc	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to cProb (P) (⟨\emptyset, A⟩) = \frac{P (\emptyset \cap A)}{P (A)}$
7		0in	$⊢ \emptyset \cap A = \emptyset$
8	7	fveq2i	$⊢ P (\emptyset \cap A) = P (\emptyset)$
9	8	oveq1i	$⊢ \frac{P (\emptyset \cap A)}{P (A)} = \frac{P (\emptyset)}{P (A)}$
10	9	a1i	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{P (\emptyset \cap A)}{P (A)} = \frac{P (\emptyset)}{P (A)}$
11		probnul	$⊢ P \in Prob \to P (\emptyset) = 0$
12	1 11	syl	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (\emptyset) = 0$
13	12	oveq1d	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{P (\emptyset)}{P (A)} = \frac{0}{P (A)}$
14		prob01	$⊢ (P \in Prob \land A \in dom P) \to P (A) \in [0, 1]$
15	14	3adant3	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \in [0, 1]$
16		elunitcn	$⊢ P (A) \in [0, 1] \to P (A) \in ℂ$
17	15 16	syl	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \in ℂ$
18		simp3	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \neq 0$
19	17 18	div0d	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{0}{P (A)} = 0$
20	10 13 19	3eqtrd	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{P (\emptyset \cap A)}{P (A)} = 0$
21	6 20	eqtrd	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to cProb (P) (⟨\emptyset, A⟩) = 0$

Metamath Proof Explorer

Theorem cndprobnul

Proof