Metamath Proof Explorer

Theorem totprob

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

Ref Expression
Assertion totprob 
|- ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> ( P ` A ) = sum* b e. B ( P ` ( b i^i A ) ) )

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> P e. Prob )
2 simp2 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> A e. dom P )
3 simp32 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> B e. ~P dom P )
4 simp31 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> U. B = U. dom P )
5 simp33l 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> B ~<_ _om )
6 simp33r 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> Disj_ b e. B b )
7 id 
 |-  ( b = c -> b = c )
8 7 cbvdisjv 
 |-  ( Disj_ b e. B b <-> Disj_ c e. B c )
9 6 8 sylib 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> Disj_ c e. B c )
10 1 2 3 4 5 9 totprobd 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> ( P ` A ) = sum* c e. B ( P ` ( c i^i A ) ) )
11 ineq1 
 |-  ( b = c -> ( b i^i A ) = ( c i^i A ) )
12 11 fveq2d 
 |-  ( b = c -> ( P ` ( b i^i A ) ) = ( P ` ( c i^i A ) ) )
13 12 cbvesumv 
 |-  sum* b e. B ( P ` ( b i^i A ) ) = sum* c e. B ( P ` ( c i^i A ) )
14 10 13 eqtr4di 
 |-  ( ( P e. Prob /\ A e. dom P /\ ( U. B = U. dom P /\ B e. ~P dom P /\ ( B ~<_ _om /\ Disj_ b e. B b ) ) ) -> ( P ` A ) = sum* b e. B ( P ` ( b i^i A ) ) )