Metamath Proof Explorer

Theorem cndprob01

Description: The conditional probability has values in [ 0 , 1 ] . (Contributed by Thierry Arnoux, 13-Dec-2016) (Revised by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprob01 ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 0 [,] 1 ) )

Proof

Step Hyp Ref Expression
1 cndprobval ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
2 1 adantr ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
3 simpl1 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝑃 ∈ Prob )
4 domprobmeas ⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
5 3 4 syl ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝑃 ∈ ( measures ‘ dom 𝑃 ) )
6 domprobsiga ⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ ∪ ran sigAlgebra )
7 3 6 syl ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → dom 𝑃 ∈ ∪ ran sigAlgebra )
8 simpl2 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝐴 ∈ dom 𝑃 )
9 simpl3 ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → 𝐵 ∈ dom 𝑃 )
10 inelsiga ⊢ ( ( dom 𝑃 ∈ ∪ ran sigAlgebra ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 )
11 7 8 9 10 syl3anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 )
12 inss2 ⊢ ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵
13 12 a1i ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝐴 ∩ 𝐵 ) ⊆ 𝐵 )
14 5 11 9 13 measssd ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑃 ‘ 𝐵 ) )
15 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ ( 𝐴 ∩ 𝐵 ) ∈ dom 𝑃 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] 1 ) )
16 3 11 15 syl2anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] 1 ) )
17 prob01 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
18 3 9 17 syl2anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) )
19 simpr ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( 𝑃 ‘ 𝐵 ) ≠ 0 )
20 unitdivcld ⊢ ( ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ∈ ( 0 [,] 1 ) ∧ ( 𝑃 ‘ 𝐵 ) ∈ ( 0 [,] 1 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑃 ‘ 𝐵 ) ↔ ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ∈ ( 0 [,] 1 ) ) )
21 16 18 19 20 syl3anc ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) ≤ ( 𝑃 ‘ 𝐵 ) ↔ ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ∈ ( 0 [,] 1 ) ) )
22 14 21 mpbid ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ∈ ( 0 [,] 1 ) )
23 2 22 eqeltrd ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑃 ‘ 𝐵 ) ≠ 0 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) ∈ ( 0 [,] 1 ) )