Metamath Proof Explorer

Theorem cndprobprob

Description: The conditional probability defines a probability law. (Contributed by Thierry Arnoux, 23-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprobprob ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑎 ∈ dom 𝑃 ↦ ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) ) ∈ Prob )

Proof

Step Hyp Ref Expression
1 domprobmeas ⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
2 1 3ad2ant1 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
3 simp2 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝐵 ∈ dom 𝑃 )
4 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
5 4 3adant3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
6 elunitrn ⊢ ( ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℝ )
7 5 6 syl ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℝ )
8 elunitge0 ⊢ ( ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) → 0 ≤ ( 𝑃 ‘ 𝐵 ) )
9 5 8 syl ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 0 ≤ ( 𝑃 ‘ 𝐵 ) )
10 simp3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ≠ 0 )
11 7 9 10 ne0gt0d ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 0 < ( 𝑃 ‘ 𝐵 ) )
12 7 11 elrpd ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ℝ+ )
13 probmeasb ⊢ ( ( 𝑃 ∈ ( measures ‘ dom 𝑃 ) ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ∈ ℝ+ ) → ( 𝑎 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ) ∈ Prob )
14 2 3 12 13 syl3anc ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑎 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ) ∈ Prob )
15 3anan32 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ↔ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝑎 ∈ dom 𝑃 ) )
16 cndprobval ⊢ ( ( 𝑃 ∈ Prob ∧ 𝑎 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
17 15 16 sylbir ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) ∧ 𝑎 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
18 17 mpteq2dva ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑎 ∈ dom 𝑃 ↦ ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) ) = ( 𝑎 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ) )
19 18 eleq1d ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( ( 𝑎 ∈ dom 𝑃 ↦ ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) ) ∈ Prob ↔ ( 𝑎 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ) ∈ Prob ) )
20 19 3adant3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( 𝑎 ∈ dom 𝑃 ↦ ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) ) ∈ Prob ↔ ( 𝑎 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ) ∈ Prob ) )
21 14 20 mpbird ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑎 ∈ dom 𝑃 ↦ ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝑎 , 𝐵 ⟩ ) ) ∈ Prob )