Metamath Proof Explorer

Theorem cndprobval

Description: The value of the conditional probability , i.e. the probability for the event A , given B , under the probability law P . (Contributed by Thierry Arnoux, 21-Jan-2017)

Ref Expression
Assertion cndprobval ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )

Proof

Step Hyp Ref Expression
1 df-ov ⊢ ( 𝐴 ( cprob ‘ 𝑃 ) 𝐵 ) = ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ )
2 df-cndprob ⊢ cprob = ( 𝑝 ∈ Prob ↦ ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) ) )
3 dmeq ⊢ ( 𝑝 = 𝑃 → dom 𝑝 = dom 𝑃 )
4 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) )
5 fveq1 ⊢ ( 𝑝 = 𝑃 → ( 𝑝 ‘ 𝑏 ) = ( 𝑃 ‘ 𝑏 ) )
6 4 5 oveq12d ⊢ ( 𝑝 = 𝑃 → ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) = ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) )
7 3 3 6 mpoeq123dv ⊢ ( 𝑝 = 𝑃 → ( 𝑎 ∈ dom 𝑝 , 𝑏 ∈ dom 𝑝 ↦ ( ( 𝑝 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑝 ‘ 𝑏 ) ) ) = ( 𝑎 ∈ dom 𝑃 , 𝑏 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) ) )
8 id ⊢ ( 𝑃 ∈ Prob → 𝑃 ∈ Prob )
9 dmexg ⊢ ( 𝑃 ∈ Prob → dom 𝑃 ∈ V )
10 mpoexga ⊢ ( ( dom 𝑃 ∈ V ∧ dom 𝑃 ∈ V ) → ( 𝑎 ∈ dom 𝑃 , 𝑏 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) ) ∈ V )
11 9 9 10 syl2anc ⊢ ( 𝑃 ∈ Prob → ( 𝑎 ∈ dom 𝑃 , 𝑏 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) ) ∈ V )
12 2 7 8 11 fvmptd3 ⊢ ( 𝑃 ∈ Prob → ( cprob ‘ 𝑃 ) = ( 𝑎 ∈ dom 𝑃 , 𝑏 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) ) )
13 12 3ad2ant1 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( cprob ‘ 𝑃 ) = ( 𝑎 ∈ dom 𝑃 , 𝑏 ∈ dom 𝑃 ↦ ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) ) )
14 simprl ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → 𝑎 = 𝐴 )
15 simprr ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → 𝑏 = 𝐵 )
16 14 15 ineq12d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑎 ∩ 𝑏 ) = ( 𝐴 ∩ 𝐵 ) )
17 16 fveq2d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) = ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) )
18 15 fveq2d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( 𝑃 ‘ 𝑏 ) = ( 𝑃 ‘ 𝐵 ) )
19 17 18 oveq12d ⊢ ( ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) ∧ ( 𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ) ) → ( ( 𝑃 ‘ ( 𝑎 ∩ 𝑏 ) ) / ( 𝑃 ‘ 𝑏 ) ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
20 simp2 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → 𝐴 ∈ dom 𝑃 )
21 simp3 ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → 𝐵 ∈ dom 𝑃 )
22 ovexd ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) ∈ V )
23 13 19 20 21 22 ovmpod ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( 𝐴 ( cprob ‘ 𝑃 ) 𝐵 ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )
24 1 23 eqtr3id ⊢ ( ( 𝑃 ∈ Prob ∧ 𝐴 ∈ dom 𝑃 ∧ 𝐵 ∈ dom 𝑃 ) → ( ( cprob ‘ 𝑃 ) ‘ ⟨ 𝐴 , 𝐵 ⟩ ) = ( ( 𝑃 ‘ ( 𝐴 ∩ 𝐵 ) ) / ( 𝑃 ‘ 𝐵 ) ) )