Metamath Proof Explorer


Theorem totprobd

Description: Law of total probability, deduction form. (Contributed by Thierry Arnoux, 25-Dec-2016)

Ref Expression
Hypotheses totprobd.1 φPProb
totprobd.2 φAdomP
totprobd.3 φB𝒫domP
totprobd.4 φB=domP
totprobd.5 φBω
totprobd.6 φDisjbBb
Assertion totprobd φPA=*bBPbA

Proof

Step Hyp Ref Expression
1 totprobd.1 φPProb
2 totprobd.2 φAdomP
3 totprobd.3 φB𝒫domP
4 totprobd.4 φB=domP
5 totprobd.5 φBω
6 totprobd.6 φDisjbBb
7 elssuni AdomPAdomP
8 2 7 syl φAdomP
9 8 4 sseqtrrd φAB
10 sseqin2 ABBA=A
11 9 10 sylib φBA=A
12 11 fveq2d φPBA=PA
13 domprobmeas PProbPmeasuresdomP
14 1 13 syl φPmeasuresdomP
15 measinb PmeasuresdomPAdomPcdomPPcAmeasuresdomP
16 14 2 15 syl2anc φcdomPPcAmeasuresdomP
17 measvun cdomPPcAmeasuresdomPB𝒫domPBωDisjbBbcdomPPcAB=*bBcdomPPcAb
18 16 3 5 6 17 syl112anc φcdomPPcAB=*bBcdomPPcAb
19 eqidd φcdomPPcA=cdomPPcA
20 simpr φc=Bc=B
21 20 ineq1d φc=BcA=BA
22 21 fveq2d φc=BPcA=PBA
23 domprobsiga PProbdomPransigAlgebra
24 1 23 syl φdomPransigAlgebra
25 sigaclcu domPransigAlgebraB𝒫domPBωBdomP
26 24 3 5 25 syl3anc φBdomP
27 inelsiga domPransigAlgebraBdomPAdomPBAdomP
28 24 26 2 27 syl3anc φBAdomP
29 prob01 PProbBAdomPPBA01
30 1 28 29 syl2anc φPBA01
31 19 22 26 30 fvmptd φcdomPPcAB=PBA
32 eqidd φbBcdomPPcA=cdomPPcA
33 simpr φbBc=bc=b
34 33 ineq1d φbBc=bcA=bA
35 34 fveq2d φbBc=bPcA=PbA
36 simpr φbBbB
37 3 adantr φbBB𝒫domP
38 elelpwi bBB𝒫domPbdomP
39 36 37 38 syl2anc φbBbdomP
40 1 adantr φbBPProb
41 24 adantr φbBdomPransigAlgebra
42 2 adantr φbBAdomP
43 inelsiga domPransigAlgebrabdomPAdomPbAdomP
44 41 39 42 43 syl3anc φbBbAdomP
45 prob01 PProbbAdomPPbA01
46 40 44 45 syl2anc φbBPbA01
47 32 35 39 46 fvmptd φbBcdomPPcAb=PbA
48 47 esumeq2dv φ*bBcdomPPcAb=*bBPbA
49 18 31 48 3eqtr3d φPBA=*bBPbA
50 12 49 eqtr3d φPA=*bBPbA