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 ≼ ω ∧ Disj b ∈ B b → P ⁡ A = ∑ * b ∈ B P ⁡ b ∩ A

Proof

Step Hyp Ref Expression
1 simp1 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → P ∈ Prob
2 simp2 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → A ∈ dom ⁡ P
3 simp32 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → B ∈ 𝒫 dom ⁡ P
4 simp31 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → ⋃ B = ⋃ dom ⁡ P
5 simp33l ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → B ≼ ω
6 simp33r ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → Disj b ∈ B b
7 id ⊢ b = c → b = c
8 7 cbvdisjv ⊢ Disj b ∈ B b ↔ Disj c ∈ B c
9 6 8 sylib ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → Disj c ∈ B c
10 1 2 3 4 5 9 totprobd ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → P ⁡ A = ∑ * c ∈ B P ⁡ 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 ∈ B P ⁡ b ∩ A = ∑ * c ∈ B P ⁡ c ∩ A
14 10 13 eqtr4di ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ ⋃ B = ⋃ dom ⁡ P ∧ B ∈ 𝒫 dom ⁡ P ∧ B ≼ ω ∧ Disj b ∈ B b → P ⁡ A = ∑ * b ∈ B P ⁡ b ∩ A