Metamath Proof Explorer

Theorem cndprobtot

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

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

Proof

Step	Hyp	Ref	Expression
1		simpl	$⊢ (P \in Prob \land A \in dom P) \to P \in Prob$
2	1	unveldomd	$⊢ (P \in Prob \land A \in dom P) \to ⋃ dom P \in dom P$
3		simpr	$⊢ (P \in Prob \land A \in dom P) \to A \in dom P$
4		cndprobval	$⊢ (P \in Prob \land ⋃ dom P \in dom P \land A \in dom P) \to cProb (P) (⟨⋃ dom P, A⟩) = \frac{P (⋃ dom P \cap A)}{P (A)}$
5	1 2 3 4	syl3anc	$⊢ (P \in Prob \land A \in dom P) \to cProb (P) (⟨⋃ dom P, A⟩) = \frac{P (⋃ dom P \cap A)}{P (A)}$
6	5	3adant3	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to cProb (P) (⟨⋃ dom P, A⟩) = \frac{P (⋃ dom P \cap A)}{P (A)}$
7		elssuni	$⊢ A \in dom P \to A \subseteq ⋃ dom P$
8	7	3ad2ant2	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to A \subseteq ⋃ dom P$
9		sseqin2	$⊢ A \subseteq ⋃ dom P \leftrightarrow ⋃ dom P \cap A = A$
10	8 9	sylib	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to ⋃ dom P \cap A = A$
11	10	fveq2d	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (⋃ dom P \cap A) = P (A)$
12	11	oveq1d	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{P (⋃ dom P \cap A)}{P (A)} = \frac{P (A)}{P (A)}$
13		prob01	$⊢ (P \in Prob \land A \in dom P) \to P (A) \in [0, 1]$
14	13	3adant3	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \in [0, 1]$
15		elunitcn	$⊢ P (A) \in [0, 1] \to P (A) \in ℂ$
16	14 15	syl	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \in ℂ$
17		simp3	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to P (A) \neq 0$
18	16 17	dividd	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to \frac{P (A)}{P (A)} = 1$
19	6 12 18	3eqtrd	$⊢ (P \in Prob \land A \in dom P \land P (A) \neq 0) \to cProb (P) (⟨⋃ dom P, A⟩) = 1$