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 𝑃 ) → ( 𝑃 ‘ ( 𝐴𝐵 ) ) = ( ( 𝑃𝐴 ) − ( 𝑃 ‘ ( 𝐴𝐵 ) ) ) )