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 e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A \ B ) ) = ( ( P ` A ) - ( P ` ( A i^i B ) ) ) )

Proof

Step Hyp Ref Expression
1 inundif 
 |-  ( ( A i^i B ) u. ( A \ B ) ) = A
2 1 fveq2i 
 |-  ( P ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( P ` A )
3 simp1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> P e. Prob )
4 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
5 inelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ A e. dom P /\ B e. dom P ) -> ( A i^i B ) e. dom P )
6 4 5 syl3an1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( A i^i B ) e. dom P )
7 difelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ A e. dom P /\ B e. dom P ) -> ( A \ B ) e. dom P )
8 4 7 syl3an1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( A \ B ) e. dom P )
9 inindif 
 |-  ( ( A i^i B ) i^i ( A \ B ) ) = (/)
10 probun 
 |-  ( ( P e. Prob /\ ( A i^i B ) e. dom P /\ ( A \ B ) e. dom P ) -> ( ( ( A i^i B ) i^i ( A \ B ) ) = (/) -> ( P ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) ) )
11 9 10 mpi 
 |-  ( ( P e. Prob /\ ( A i^i B ) e. dom P /\ ( A \ B ) e. dom P ) -> ( P ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) )
12 3 6 8 11 syl3anc 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( ( A i^i B ) u. ( A \ B ) ) ) = ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) )
13 2 12 eqtr3id 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` A ) = ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) )
14 13 oveq1d 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( P ` A ) - ( P ` ( A i^i B ) ) ) = ( ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) - ( P ` ( A i^i B ) ) ) )
15 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
16 prob01 
 |-  ( ( P e. Prob /\ ( A i^i B ) e. dom P ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
17 3 6 16 syl2anc 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A i^i B ) ) e. ( 0 [,] 1 ) )
18 15 17 sselid 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A i^i B ) ) e. CC )
19 prob01 
 |-  ( ( P e. Prob /\ ( A \ B ) e. dom P ) -> ( P ` ( A \ B ) ) e. ( 0 [,] 1 ) )
20 3 8 19 syl2anc 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A \ B ) ) e. ( 0 [,] 1 ) )
21 15 20 sselid 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A \ B ) ) e. CC )
22 18 21 pncan2d 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( ( P ` ( A i^i B ) ) + ( P ` ( A \ B ) ) ) - ( P ` ( A i^i B ) ) ) = ( P ` ( A \ B ) ) )
23 14 22 eqtr2d 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( P ` ( A \ B ) ) = ( ( P ` A ) - ( P ` ( A i^i B ) ) ) )