Metamath Proof Explorer

Theorem probdif

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

Ref Expression
Assertion probdif ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∖ B = P ⁡ A − P ⁡ A ∩ B

Proof

Step Hyp Ref Expression
1 inundif ⊢ A ∩ B ∪ A ∖ B = A
2 1 fveq2i ⊢ P ⁡ A ∩ B ∪ A ∖ B = P ⁡ A
3 simp1 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ∈ Prob
4 domprobsiga ⊢ P ∈ Prob → dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra
5 inelsiga ⊢ dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → A ∩ B ∈ dom ⁡ P
6 4 5 syl3an1 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → A ∩ B ∈ dom ⁡ P
7 difelsiga ⊢ dom ⁡ P ∈ ⋃ ran ⁡ sigAlgebra ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → A ∖ B ∈ dom ⁡ P
8 4 7 syl3an1 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → A ∖ B ∈ dom ⁡ P
9 inindif ⊢ A ∩ B ∩ A ∖ B = ∅
10 probun ⊢ P ∈ Prob ∧ A ∩ B ∈ dom ⁡ P ∧ A ∖ B ∈ dom ⁡ P → A ∩ B ∩ A ∖ B = ∅ → P ⁡ A ∩ B ∪ A ∖ B = P ⁡ A ∩ B + P ⁡ A ∖ B
11 9 10 mpi ⊢ P ∈ Prob ∧ A ∩ B ∈ dom ⁡ P ∧ A ∖ B ∈ dom ⁡ P → P ⁡ A ∩ B ∪ A ∖ B = P ⁡ A ∩ B + P ⁡ A ∖ B
12 3 6 8 11 syl3anc ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∩ B ∪ A ∖ B = P ⁡ A ∩ B + P ⁡ A ∖ B
13 2 12 eqtr3id ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A = P ⁡ A ∩ B + P ⁡ A ∖ B
14 13 oveq1d ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A − P ⁡ A ∩ B = P ⁡ A ∩ B + P ⁡ A ∖ B - P ⁡ A ∩ B
15 unitsscn ⊢ 0 1 ⊆ ℂ
16 prob01 ⊢ P ∈ Prob ∧ A ∩ B ∈ dom ⁡ P → P ⁡ A ∩ B ∈ 0 1
17 3 6 16 syl2anc ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∩ B ∈ 0 1
18 15 17 sselid ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∩ B ∈ ℂ
19 prob01 ⊢ P ∈ Prob ∧ A ∖ B ∈ dom ⁡ P → P ⁡ A ∖ B ∈ 0 1
20 3 8 19 syl2anc ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∖ B ∈ 0 1
21 15 20 sselid ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∖ B ∈ ℂ
22 18 21 pncan2d ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∩ B + P ⁡ A ∖ B - P ⁡ A ∩ B = P ⁡ A ∖ B
23 14 22 eqtr2d ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ B ∈ dom ⁡ P → P ⁡ A ∖ B = P ⁡ A − P ⁡ A ∩ B