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 
|- ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )

Proof

Step Hyp Ref Expression
1 df-ov 
 |-  ( A ( cprob ` P ) B ) = ( ( cprob ` P ) ` <. A , B >. )
2 df-cndprob 
 |-  cprob = ( p e. Prob |-> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) )
3 dmeq 
 |-  ( p = P -> dom p = dom P )
4 fveq1 
 |-  ( p = P -> ( p ` ( a i^i b ) ) = ( P ` ( a i^i b ) ) )
5 fveq1 
 |-  ( p = P -> ( p ` b ) = ( P ` b ) )
6 4 5 oveq12d 
 |-  ( p = P -> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) = ( ( P ` ( a i^i b ) ) / ( P ` b ) ) )
7 3 3 6 mpoeq123dv 
 |-  ( p = P -> ( a e. dom p , b e. dom p |-> ( ( p ` ( a i^i b ) ) / ( p ` b ) ) ) = ( a e. dom P , b e. dom P |-> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) ) )
8 id 
 |-  ( P e. Prob -> P e. Prob )
9 dmexg 
 |-  ( P e. Prob -> dom P e. _V )
10 mpoexga 
 |-  ( ( dom P e. _V /\ dom P e. _V ) -> ( a e. dom P , b e. dom P |-> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) ) e. _V )
11 9 9 10 syl2anc 
 |-  ( P e. Prob -> ( a e. dom P , b e. dom P |-> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) ) e. _V )
12 2 7 8 11 fvmptd3 
 |-  ( P e. Prob -> ( cprob ` P ) = ( a e. dom P , b e. dom P |-> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) ) )
13 12 3ad2ant1 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( cprob ` P ) = ( a e. dom P , b e. dom P |-> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) ) )
14 simprl 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> a = A )
15 simprr 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> b = B )
16 14 15 ineq12d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> ( a i^i b ) = ( A i^i B ) )
17 16 fveq2d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> ( P ` ( a i^i b ) ) = ( P ` ( A i^i B ) ) )
18 15 fveq2d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> ( P ` b ) = ( P ` B ) )
19 17 18 oveq12d 
 |-  ( ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) /\ ( a = A /\ b = B ) ) -> ( ( P ` ( a i^i b ) ) / ( P ` b ) ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
20 simp2 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> A e. dom P )
21 simp3 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> B e. dom P )
22 ovexd 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( P ` ( A i^i B ) ) / ( P ` B ) ) e. _V )
23 13 19 20 21 22 ovmpod 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( A ( cprob ` P ) B ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )
24 1 23 eqtr3id 
 |-  ( ( P e. Prob /\ A e. dom P /\ B e. dom P ) -> ( ( cprob ` P ) ` <. A , B >. ) = ( ( P ` ( A i^i B ) ) / ( P ` B ) ) )