Description: Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016)
Ref | Expression | ||
---|---|---|---|
Hypotheses | totprobd.1 | |
|
totprobd.2 | |
||
totprobd.3 | |
||
totprobd.4 | |
||
totprobd.5 | |
||
totprobd.6 | |
||
Assertion | totprobd | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | totprobd.1 | |
|
2 | totprobd.2 | |
|
3 | totprobd.3 | |
|
4 | totprobd.4 | |
|
5 | totprobd.5 | |
|
6 | totprobd.6 | |
|
7 | elssuni | |
|
8 | 2 7 | syl | |
9 | 8 4 | sseqtrrd | |
10 | sseqin2 | |
|
11 | 9 10 | sylib | |
12 | 11 | fveq2d | |
13 | domprobmeas | |
|
14 | 1 13 | syl | |
15 | measinb | |
|
16 | 14 2 15 | syl2anc | |
17 | measvun | |
|
18 | 16 3 5 6 17 | syl112anc | |
19 | eqidd | |
|
20 | simpr | |
|
21 | 20 | ineq1d | |
22 | 21 | fveq2d | |
23 | domprobsiga | |
|
24 | 1 23 | syl | |
25 | sigaclcu | |
|
26 | 24 3 5 25 | syl3anc | |
27 | inelsiga | |
|
28 | 24 26 2 27 | syl3anc | |
29 | prob01 | |
|
30 | 1 28 29 | syl2anc | |
31 | 19 22 26 30 | fvmptd | |
32 | eqidd | |
|
33 | simpr | |
|
34 | 33 | ineq1d | |
35 | 34 | fveq2d | |
36 | simpr | |
|
37 | 3 | adantr | |
38 | elelpwi | |
|
39 | 36 37 38 | syl2anc | |
40 | 1 | adantr | |
41 | 24 | adantr | |
42 | 2 | adantr | |
43 | inelsiga | |
|
44 | 41 39 42 43 | syl3anc | |
45 | prob01 | |
|
46 | 40 44 45 | syl2anc | |
47 | 32 35 39 46 | fvmptd | |
48 | 47 | esumeq2dv | |
49 | 18 31 48 | 3eqtr3d | |
50 | 12 49 | eqtr3d | |