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 ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∅ , 𝐴 ⟩ ) = 0 )

Proof

Step Hyp Ref Expression
1 simp1 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → 𝑃 ∈ Prob )
2 nuleldmp ⊢ ( 𝑃 ∈ Prob → ∅ ∈ dom 𝑃 )
3 1 2 syl ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ∅ ∈ dom 𝑃 )
4 simp2 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → 𝐴 ∈ dom 𝑃 )
5 cndprobval ⊢ ( ( 𝑃 ∈ Prob ∧ ∅ ∈ dom 𝑃 ∧ 𝐴 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∅ , 𝐴 ⟩ ) = ( ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) )
6 1 3 4 5 syl3anc ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∅ , 𝐴 ⟩ ) = ( ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) )
7 0in ⊢ ( ∅ ∩ 𝐴 ) = ∅
8 7 fveq2i ⊢ ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) = ( 𝑃 ‘ ∅ )
9 8 oveq1i ⊢ ( ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) = ( ( 𝑃 ‘ ∅ ) / ( 𝑃 ‘ 𝐴 ) )
10 9 a1i ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) = ( ( 𝑃 ‘ ∅ ) / ( 𝑃 ‘ 𝐴 ) ) )
11 probnul ⊢ ( 𝑃 ∈ Prob → ( 𝑃 ‘ ∅ ) = 0 )
12 1 11 syl ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ ∅ ) = 0 )
13 12 oveq1d ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑃 ‘ ∅ ) / ( 𝑃 ‘ 𝐴 ) ) = ( 0 / ( 𝑃 ‘ 𝐴 ) ) )
14 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
15 14 3adant3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) )
16 elunitcn ⊢ ( ( 𝑃 ‘ 𝐴 ) ∈ ( 0 [,] 1 ) → ( 𝑃 ‘ 𝐴 ) ∈ ℂ )
17 15 16 syl ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ∈ ℂ )
18 simp3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 𝑃 ‘ 𝐴 ) ≠ 0 )
19 17 18 div0d ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( 0 / ( 𝑃 ‘ 𝐴 ) ) = 0 )
20 10 13 19 3eqtrd ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( 𝑃 ‘ ( ∅ ∩ 𝐴 ) ) / ( 𝑃 ‘ 𝐴 ) ) = 0 )
21 6 20 eqtrd ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐴 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ ∅ , 𝐴 ⟩ ) = 0 )