Metamath Proof Explorer

Theorem cndprobnul

Description: The conditional probability given empty event is zero. (Contributed by Thierry Arnoux, 20-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprobnul ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → cProb ⁡ P ⁡ ∅ A = 0

Proof

Step Hyp Ref Expression
1 simp1 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ∈ Prob
2 nuleldmp ⊢ P ∈ Prob → ∅ ∈ dom ⁡ P
3 1 2 syl ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → ∅ ∈ dom ⁡ P
4 simp2 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → A ∈ dom ⁡ P
5 cndprobval ⊢ P ∈ Prob ∧ ∅ ∈ dom ⁡ P ∧ A ∈ dom ⁡ P → cProb ⁡ P ⁡ ∅ A = P ⁡ ∅ ∩ A P ⁡ A
6 1 3 4 5 syl3anc ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → cProb ⁡ P ⁡ ∅ A = P ⁡ ∅ ∩ A P ⁡ A
7 0in ⊢ ∅ ∩ A = ∅
8 7 fveq2i ⊢ P ⁡ ∅ ∩ A = P ⁡ ∅
9 8 oveq1i ⊢ P ⁡ ∅ ∩ A P ⁡ A = P ⁡ ∅ P ⁡ A
10 9 a1i ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ ∅ ∩ A P ⁡ A = P ⁡ ∅ P ⁡ A
11 probnul ⊢ P ∈ Prob → P ⁡ ∅ = 0
12 1 11 syl ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ ∅ = 0
13 12 oveq1d ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ ∅ P ⁡ A = 0 P ⁡ A
14 prob01 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P → P ⁡ A ∈ 0 1
15 14 3adant3 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ A ∈ 0 1
16 elunitcn ⊢ P ⁡ A ∈ 0 1 → P ⁡ A ∈ ℂ
17 15 16 syl ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ A ∈ ℂ
18 simp3 ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ A ≠ 0
19 17 18 div0d ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → 0 P ⁡ A = 0
20 10 13 19 3eqtrd ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → P ⁡ ∅ ∩ A P ⁡ A = 0
21 6 20 eqtrd ⊢ P ∈ Prob ∧ A ∈ dom ⁡ P ∧ P ⁡ A ≠ 0 → cProb ⁡ P ⁡ ∅ A = 0