Metamath Proof Explorer

Theorem totprob

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

Ref Expression
Assertion totprob ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→P⁡A=∑*b∈BP⁡b∩A

Proof

Step Hyp Ref Expression
1 simp1 ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→P∈Prob
2 simp2 ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→A∈dom⁡P
3 simp32 ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→B∈𝒫dom⁡P
4 simp31 ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→⋃B=⋃dom⁡P
5 simp33l ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→B≼ω
6 simp33r ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→Disjb∈Bb
7 id ⊢b=c→b=c
8 7 cbvdisjv ⊢Disjb∈Bb↔Disjc∈Bc
9 6 8 sylib ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→Disjc∈Bc
10 1 2 3 4 5 9 totprobd ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→P⁡A=∑*c∈BP⁡c∩A
11 ineq1 ⊢b=c→b∩A=c∩A
12 11 fveq2d ⊢b=c→P⁡b∩A=P⁡c∩A
13 12 cbvesumv ⊢∑*b∈BP⁡b∩A=∑*c∈BP⁡c∩A
14 10 13 eqtr4di ⊢P∈Prob∧A∈dom⁡P∧⋃B=⋃dom⁡P∧B∈𝒫dom⁡P∧B≼ω∧Disjb∈Bb→P⁡A=∑*b∈BP⁡b∩A