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 ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝐴 ∖ 𝐵 ) ) = ( ( 𝑃 ‘ 𝐴 ) − ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ) )

Proof

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