Metamath Proof Explorer

Theorem probun

Description: The probability of the union two incompatible events is the sum of their probabilities. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Assertion probun 
|- ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( A i^i B ) = (/) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) ) )

Proof

Step Hyp Ref Expression
1 simpll1 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A = B ) /\ ( A i^i B ) = (/) ) -> P e. Prob )
2 simplr 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A = B ) /\ ( A i^i B ) = (/) ) -> A = B )
3 simpr 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A = B ) /\ ( A i^i B ) = (/) ) -> ( A i^i B ) = (/) )
4 disj3 
 |-  ( ( A i^i B ) = (/) <-> A = ( A \ B ) )
5 4 biimpi 
 |-  ( ( A i^i B ) = (/) -> A = ( A \ B ) )
6 difeq1 
 |-  ( A = B -> ( A \ B ) = ( B \ B ) )
7 difid 
 |-  ( B \ B ) = (/)
8 6 7 eqtrdi 
 |-  ( A = B -> ( A \ B ) = (/) )
9 5 8 sylan9eqr 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> A = (/) )
10 eqtr2 
 |-  ( ( A = B /\ A = (/) ) -> B = (/) )
11 9 10 syldan 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> B = (/) )
12 9 11 uneq12d 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> ( A u. B ) = ( (/) u. (/) ) )
13 unidm 
 |-  ( (/) u. (/) ) = (/)
14 12 13 eqtrdi 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> ( A u. B ) = (/) )
15 14 fveq2d 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> ( P ` ( A u. B ) ) = ( P ` (/) ) )
16 probnul 
 |-  ( P e. Prob -> ( P ` (/) ) = 0 )
17 15 16 sylan9eqr 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( P ` ( A u. B ) ) = 0 )
18 9 fveq2d 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> ( P ` A ) = ( P ` (/) ) )
19 18 16 sylan9eqr 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( P ` A ) = 0 )
20 11 fveq2d 
 |-  ( ( A = B /\ ( A i^i B ) = (/) ) -> ( P ` B ) = ( P ` (/) ) )
21 20 16 sylan9eqr 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( P ` B ) = 0 )
22 19 21 oveq12d 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( ( P ` A ) + ( P ` B ) ) = ( 0 + 0 ) )
23 00id 
 |-  ( 0 + 0 ) = 0
24 22 23 eqtrdi 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( ( P ` A ) + ( P ` B ) ) = 0 )
25 17 24 eqtr4d 
 |-  ( ( P e. Prob /\ ( A = B /\ ( A i^i B ) = (/) ) ) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) )
26 1 2 3 25 syl12anc 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A = B ) /\ ( A i^i B ) = (/) ) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) )
27 26 ex 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A = B ) -> ( ( A i^i B ) = (/) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) ) )
28 3anass 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) <-> ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) ) )
29 28 anbi1i 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) <-> ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) ) /\ A =/= B ) )
30 df-3an 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) <-> ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) ) /\ A =/= B ) )
31 29 30 bitr4i 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) <-> ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) )
32 simpl1 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> P e. Prob )
33 prssi 
 |-  ( ( A e. dom P /\ B e. dom P ) -> { A , B } C_ dom P )
34 33 3ad2ant2 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> { A , B } C_ dom P )
35 34 adantr 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> { A , B } C_ dom P )
36 prex 
 |-  { A , B } e. _V
37 36 elpw 
 |-  ( { A , B } e. ~P dom P <-> { A , B } C_ dom P )
38 35 37 sylibr 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> { A , B } e. ~P dom P )
39 prct 
 |-  ( ( A e. dom P /\ B e. dom P ) -> { A , B } ~<_ _om )
40 39 3ad2ant2 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> { A , B } ~<_ _om )
41 40 adantr 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> { A , B } ~<_ _om )
42 simp2l 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> A e. dom P )
43 simp2r 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> B e. dom P )
44 simp3 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> A =/= B )
45 id 
 |-  ( x = A -> x = A )
46 id 
 |-  ( x = B -> x = B )
47 45 46 disjprg 
 |-  ( ( A e. dom P /\ B e. dom P /\ A =/= B ) -> ( Disj_ x e. { A , B } x <-> ( A i^i B ) = (/) ) )
48 42 43 44 47 syl3anc 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( Disj_ x e. { A , B } x <-> ( A i^i B ) = (/) ) )
49 48 biimpar 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> Disj_ x e. { A , B } x )
50 probcun 
 |-  ( ( P e. Prob /\ { A , B } e. ~P dom P /\ ( { A , B } ~<_ _om /\ Disj_ x e. { A , B } x ) ) -> ( P ` U. { A , B } ) = sum* x e. { A , B } ( P ` x ) )
51 32 38 41 49 50 syl112anc 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` U. { A , B } ) = sum* x e. { A , B } ( P ` x ) )
52 uniprg 
 |-  ( ( A e. dom P /\ B e. dom P ) -> U. { A , B } = ( A u. B ) )
53 52 fveq2d 
 |-  ( ( A e. dom P /\ B e. dom P ) -> ( P ` U. { A , B } ) = ( P ` ( A u. B ) ) )
54 53 3ad2ant2 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( P ` U. { A , B } ) = ( P ` ( A u. B ) ) )
55 fveq2 
 |-  ( x = A -> ( P ` x ) = ( P ` A ) )
56 55 adantl 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ x = A ) -> ( P ` x ) = ( P ` A ) )
57 fveq2 
 |-  ( x = B -> ( P ` x ) = ( P ` B ) )
58 57 adantl 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ x = B ) -> ( P ` x ) = ( P ` B ) )
59 unitssxrge0 
 |-  ( 0 [,] 1 ) C_ ( 0 [,] +oo )
60 simp1 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> P e. Prob )
61 prob01 
 |-  ( ( P e. Prob /\ A e. dom P ) -> ( P ` A ) e. ( 0 [,] 1 ) )
62 60 42 61 syl2anc 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( P ` A ) e. ( 0 [,] 1 ) )
63 59 62 sselid 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( P ` A ) e. ( 0 [,] +oo ) )
64 prob01 
 |-  ( ( P e. Prob /\ B e. dom P ) -> ( P ` B ) e. ( 0 [,] 1 ) )
65 60 43 64 syl2anc 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( P ` B ) e. ( 0 [,] 1 ) )
66 59 65 sselid 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( P ` B ) e. ( 0 [,] +oo ) )
67 56 58 42 43 63 66 44 esumpr 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> sum* x e. { A , B } ( P ` x ) = ( ( P ` A ) +e ( P ` B ) ) )
68 54 67 eqeq12d 
 |-  ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( ( P ` U. { A , B } ) = sum* x e. { A , B } ( P ` x ) <-> ( P ` ( A u. B ) ) = ( ( P ` A ) +e ( P ` B ) ) ) )
69 68 adantr 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( ( P ` U. { A , B } ) = sum* x e. { A , B } ( P ` x ) <-> ( P ` ( A u. B ) ) = ( ( P ` A ) +e ( P ` B ) ) ) )
70 51 69 mpbid 
 |-  ( ( ( P e. Prob /\ ( A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` ( A u. B ) ) = ( ( P ` A ) +e ( P ` B ) ) )
71 31 70 sylanb 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` ( A u. B ) ) = ( ( P ` A ) +e ( P ` B ) ) )
72 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
73 simpll1 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> P e. Prob )
74 simpll2 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> A e. dom P )
75 73 74 61 syl2anc 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` A ) e. ( 0 [,] 1 ) )
76 72 75 sselid 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` A ) e. RR )
77 simpll3 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> B e. dom P )
78 73 77 64 syl2anc 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` B ) e. ( 0 [,] 1 ) )
79 72 78 sselid 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` B ) e. RR )
80 rexadd 
 |-  ( ( ( P ` A ) e. RR /\ ( P ` B ) e. RR ) -> ( ( P ` A ) +e ( P ` B ) ) = ( ( P ` A ) + ( P ` B ) ) )
81 76 79 80 syl2anc 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( ( P ` A ) +e ( P ` B ) ) = ( ( P ` A ) + ( P ` B ) ) )
82 71 81 eqtrd 
 |-  ( ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) /\ ( A i^i B ) = (/) ) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) )
83 82 ex 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ A =/= B ) -> ( ( A i^i B ) = (/) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) ) )
84 27 83 pm2.61dane 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( A i^i B ) = (/) -> ( P ` ( A u. B ) ) = ( ( P ` A ) + ( P ` B ) ) ) )