probdif

Description: The probability of the difference of two event sets. (Contributed by Thierry Arnoux, 12-Dec-2016)

		Ref	Expression
	Assertion	probdif	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A ∖ B) = P (A) - P (A \cap B)$

Proof

Step	Hyp	Ref	Expression
1		inundif	$⊢ (A \cap B) \cup (A ∖ B) = A$
2	1	fveq2i	$⊢ P ((A \cap B) \cup (A ∖ B)) = P (A)$
3		simp1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P \in Prob$
4		domprobsiga	$⊢ P \in Prob \to dom P \in ⋃ ran sigAlgebra$
5		inelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land A \in dom P \land B \in dom P) \to A \cap B \in dom P$
6	4 5	syl3an1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to A \cap B \in dom P$
7		difelsiga	$⊢ (dom P \in ⋃ ran sigAlgebra \land A \in dom P \land B \in dom P) \to A ∖ B \in dom P$
8	4 7	syl3an1	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to A ∖ B \in dom P$
9		inindif	$⊢ (A \cap B) \cap (A ∖ B) = \emptyset$
10		probun	$⊢ (P \in Prob \land A \cap B \in dom P \land A ∖ B \in dom P) \to ((A \cap B) \cap (A ∖ B) = \emptyset \to P ((A \cap B) \cup (A ∖ B)) = P (A \cap B) + P (A ∖ B))$
11	9 10	mpi	$⊢ (P \in Prob \land A \cap B \in dom P \land A ∖ B \in dom P) \to P ((A \cap B) \cup (A ∖ B)) = P (A \cap B) + P (A ∖ B)$
12	3 6 8 11	syl3anc	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P ((A \cap B) \cup (A ∖ B)) = P (A \cap B) + P (A ∖ B)$
13	2 12	eqtr3id	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A) = P (A \cap B) + P (A ∖ B)$
14	13	oveq1d	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A) - P (A \cap B) = P (A \cap B) + P (A ∖ B) - P (A \cap B)$
15		unitsscn	$⊢ [0, 1] \subseteq ℂ$
16		prob01	$⊢ (P \in Prob \land A \cap B \in dom P) \to P (A \cap B) \in [0, 1]$
17	3 6 16	syl2anc	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A \cap B) \in [0, 1]$
18	15 17	sselid	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A \cap B) \in ℂ$
19		prob01	$⊢ (P \in Prob \land A ∖ B \in dom P) \to P (A ∖ B) \in [0, 1]$
20	3 8 19	syl2anc	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A ∖ B) \in [0, 1]$
21	15 20	sselid	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A ∖ B) \in ℂ$
22	18 21	pncan2d	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A \cap B) + P (A ∖ B) - P (A \cap B) = P (A ∖ B)$
23	14 22	eqtr2d	$⊢ (P \in Prob \land A \in dom P \land B \in dom P) \to P (A ∖ B) = P (A) - P (A \cap B)$

Metamath Proof Explorer

Theorem probdif

Proof