Metamath Proof Explorer

Theorem totprob

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

		Ref	Expression
	Assertion	totprob	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → ( 𝑃 ‘ 𝐴 ) = Σ^* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		simp1	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → 𝑃 ∈ Prob )
2		simp2	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → 𝐴 ∈ dom 𝑃 )
3		simp32	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → 𝐵 ∈ 𝒫 dom 𝑃 )
4		simp31	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → ∪ 𝐵 = ∪ dom 𝑃 )
5		simp33l	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → 𝐵 ≼ ω )
6		simp33r	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → Disj 𝑏 ∈ 𝐵 𝑏 )
7		id	⊢ ( 𝑏 = 𝑐 → 𝑏 = 𝑐 )
8	7	cbvdisjv	⊢ ( Disj 𝑏 ∈ 𝐵 𝑏 ↔ Disj 𝑐 ∈ 𝐵 𝑐 )
9	6 8	sylib	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → Disj 𝑐 ∈ 𝐵 𝑐 )
10	1 2 3 4 5 9	totprobd	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → ( 𝑃 ‘ 𝐴 ) = Σ^* 𝑐 ∈ 𝐵 ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) )
11		ineq1	⊢ ( 𝑏 = 𝑐 → ( 𝑏 ∩ 𝐴 ) = ( 𝑐 ∩ 𝐴 ) )
12	11	fveq2d	⊢ ( 𝑏 = 𝑐 → ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) = ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) ) )
13	12	cbvesumv	⊢ Σ^* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) = Σ^* 𝑐 ∈ 𝐵 ( 𝑃 ‘ ( 𝑐 ∩ 𝐴 ) )
14	10 13	eqtr4di	⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( ∪ 𝐵 = ∪ dom 𝑃 ∧ 𝐵 ∈ 𝒫 dom 𝑃 ∧ ( 𝐵 ≼ ω ∧ Disj 𝑏 ∈ 𝐵 𝑏 ) ) ) → ( 𝑃 ‘ 𝐴 ) = Σ^* 𝑏 ∈ 𝐵 ( 𝑃 ‘ ( 𝑏 ∩ 𝐴 ) ) )