Metamath Proof Explorer

Theorem totprobd

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

Ref Expression
Hypotheses totprobd.1 
|- ( ph -> P e. Prob )
totprobd.2 
|- ( ph -> A e. dom P )
totprobd.3 
|- ( ph -> B e. ~P dom P )
totprobd.4 
|- ( ph -> U. B = U. dom P )
totprobd.5 
|- ( ph -> B ~<_ _om )
totprobd.6 
|- ( ph -> Disj_ b e. B b )
Assertion totprobd 
|- ( ph -> ( P ` A ) = sum* b e. B ( P ` ( b i^i A ) ) )

Proof

Step Hyp Ref Expression
1 totprobd.1 
 |-  ( ph -> P e. Prob )
2 totprobd.2 
 |-  ( ph -> A e. dom P )
3 totprobd.3 
 |-  ( ph -> B e. ~P dom P )
4 totprobd.4 
 |-  ( ph -> U. B = U. dom P )
5 totprobd.5 
 |-  ( ph -> B ~<_ _om )
6 totprobd.6 
 |-  ( ph -> Disj_ b e. B b )
7 elssuni 
 |-  ( A e. dom P -> A C_ U. dom P )
8 2 7 syl 
 |-  ( ph -> A C_ U. dom P )
9 8 4 sseqtrrd 
 |-  ( ph -> A C_ U. B )
10 sseqin2 
 |-  ( A C_ U. B <-> ( U. B i^i A ) = A )
11 9 10 sylib 
 |-  ( ph -> ( U. B i^i A ) = A )
12 11 fveq2d 
 |-  ( ph -> ( P ` ( U. B i^i A ) ) = ( P ` A ) )
13 domprobmeas 
 |-  ( P e. Prob -> P e. ( measures ` dom P ) )
14 1 13 syl 
 |-  ( ph -> P e. ( measures ` dom P ) )
15 measinb 
 |-  ( ( P e. ( measures ` dom P ) /\ A e. dom P ) -> ( c e. dom P |-> ( P ` ( c i^i A ) ) ) e. ( measures ` dom P ) )
16 14 2 15 syl2anc 
 |-  ( ph -> ( c e. dom P |-> ( P ` ( c i^i A ) ) ) e. ( measures ` dom P ) )
17 measvun 
 |-  ( ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) e. ( measures ` dom P ) /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) -> ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` U. B ) = sum* b e. B ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` b ) )
18 16 3 5 6 17 syl112anc 
 |-  ( ph -> ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` U. B ) = sum* b e. B ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` b ) )
19 eqidd 
 |-  ( ph -> ( c e. dom P |-> ( P ` ( c i^i A ) ) ) = ( c e. dom P |-> ( P ` ( c i^i A ) ) ) )
20 simpr 
 |-  ( ( ph /\ c = U. B ) -> c = U. B )
21 20 ineq1d 
 |-  ( ( ph /\ c = U. B ) -> ( c i^i A ) = ( U. B i^i A ) )
22 21 fveq2d 
 |-  ( ( ph /\ c = U. B ) -> ( P ` ( c i^i A ) ) = ( P ` ( U. B i^i A ) ) )
23 domprobsiga 
 |-  ( P e. Prob -> dom P e. U. ran sigAlgebra )
24 1 23 syl 
 |-  ( ph -> dom P e. U. ran sigAlgebra )
25 sigaclcu 
 |-  ( ( dom P e. U. ran sigAlgebra /\ B e. ~P dom P /\ B ~<_ _om ) -> U. B e. dom P )
26 24 3 5 25 syl3anc 
 |-  ( ph -> U. B e. dom P )
27 inelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ U. B e. dom P /\ A e. dom P ) -> ( U. B i^i A ) e. dom P )
28 24 26 2 27 syl3anc 
 |-  ( ph -> ( U. B i^i A ) e. dom P )
29 prob01 
 |-  ( ( P e. Prob /\ ( U. B i^i A ) e. dom P ) -> ( P ` ( U. B i^i A ) ) e. ( 0 [,] 1 ) )
30 1 28 29 syl2anc 
 |-  ( ph -> ( P ` ( U. B i^i A ) ) e. ( 0 [,] 1 ) )
31 19 22 26 30 fvmptd 
 |-  ( ph -> ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` U. B ) = ( P ` ( U. B i^i A ) ) )
32 eqidd 
 |-  ( ( ph /\ b e. B ) -> ( c e. dom P |-> ( P ` ( c i^i A ) ) ) = ( c e. dom P |-> ( P ` ( c i^i A ) ) ) )
33 simpr 
 |-  ( ( ( ph /\ b e. B ) /\ c = b ) -> c = b )
34 33 ineq1d 
 |-  ( ( ( ph /\ b e. B ) /\ c = b ) -> ( c i^i A ) = ( b i^i A ) )
35 34 fveq2d 
 |-  ( ( ( ph /\ b e. B ) /\ c = b ) -> ( P ` ( c i^i A ) ) = ( P ` ( b i^i A ) ) )
36 simpr 
 |-  ( ( ph /\ b e. B ) -> b e. B )
37 3 adantr 
 |-  ( ( ph /\ b e. B ) -> B e. ~P dom P )
38 elelpwi 
 |-  ( ( b e. B /\ B e. ~P dom P ) -> b e. dom P )
39 36 37 38 syl2anc 
 |-  ( ( ph /\ b e. B ) -> b e. dom P )
40 1 adantr 
 |-  ( ( ph /\ b e. B ) -> P e. Prob )
41 24 adantr 
 |-  ( ( ph /\ b e. B ) -> dom P e. U. ran sigAlgebra )
42 2 adantr 
 |-  ( ( ph /\ b e. B ) -> A e. dom P )
43 inelsiga 
 |-  ( ( dom P e. U. ran sigAlgebra /\ b e. dom P /\ A e. dom P ) -> ( b i^i A ) e. dom P )
44 41 39 42 43 syl3anc 
 |-  ( ( ph /\ b e. B ) -> ( b i^i A ) e. dom P )
45 prob01 
 |-  ( ( P e. Prob /\ ( b i^i A ) e. dom P ) -> ( P ` ( b i^i A ) ) e. ( 0 [,] 1 ) )
46 40 44 45 syl2anc 
 |-  ( ( ph /\ b e. B ) -> ( P ` ( b i^i A ) ) e. ( 0 [,] 1 ) )
47 32 35 39 46 fvmptd 
 |-  ( ( ph /\ b e. B ) -> ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` b ) = ( P ` ( b i^i A ) ) )
48 47 esumeq2dv 
 |-  ( ph -> sum* b e. B ( ( c e. dom P |-> ( P ` ( c i^i A ) ) ) ` b ) = sum* b e. B ( P ` ( b i^i A ) ) )
49 18 31 48 3eqtr3d 
 |-  ( ph -> ( P ` ( U. B i^i A ) ) = sum* b e. B ( P ` ( b i^i A ) ) )
50 12 49 eqtr3d 
 |-  ( ph -> ( P ` A ) = sum* b e. B ( P ` ( b i^i A ) ) )