Metamath Proof Explorer

Theorem coinflipprob

Description: The P we defined for coin-flip is a probability law. (Contributed by Thierry Arnoux, 15-Jan-2017)

Ref Expression
Hypotheses coinflip.h 
|- H e. _V
coinflip.t 
|- T e. _V
coinflip.th 
|- H =/= T
coinflip.2 
|- P = ( ( # |` ~P { H , T } ) oFC / 2 )
coinflip.3 
|- X = { <. H , 1 >. , <. T , 0 >. }
Assertion coinflipprob 
|- P e. Prob

Proof

Step Hyp Ref Expression
1 coinflip.h 
 |-  H e. _V
2 coinflip.t 
 |-  T e. _V
3 coinflip.th 
 |-  H =/= T
4 coinflip.2 
 |-  P = ( ( # |` ~P { H , T } ) oFC / 2 )
5 coinflip.3 
 |-  X = { <. H , 1 >. , <. T , 0 >. }
6 1 2 3 4 5 coinfliplem 
 |-  P = ( ( # |` ~P { H , T } ) oFC /e 2 )
7 unipw 
 |-  U. ~P { H , T } = { H , T }
8 prex 
 |-  { H , T } e. _V
9 8 pwid 
 |-  { H , T } e. ~P { H , T }
10 7 9 eqeltri 
 |-  U. ~P { H , T } e. ~P { H , T }
11 fvres 
 |-  ( U. ~P { H , T } e. ~P { H , T } -> ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) = ( # ` U. ~P { H , T } ) )
12 10 11 ax-mp 
 |-  ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) = ( # ` U. ~P { H , T } )
13 7 fveq2i 
 |-  ( # ` U. ~P { H , T } ) = ( # ` { H , T } )
14 hashprg 
 |-  ( ( H e. _V /\ T e. _V ) -> ( H =/= T <-> ( # ` { H , T } ) = 2 ) )
15 1 2 14 mp2an 
 |-  ( H =/= T <-> ( # ` { H , T } ) = 2 )
16 3 15 mpbi 
 |-  ( # ` { H , T } ) = 2
17 12 13 16 3eqtri 
 |-  ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) = 2
18 17 oveq2i 
 |-  ( ( # |` ~P { H , T } ) oFC /e ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) ) = ( ( # |` ~P { H , T } ) oFC /e 2 )
19 6 18 eqtr4i 
 |-  P = ( ( # |` ~P { H , T } ) oFC /e ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) )
20 pwcntmeas 
 |-  ( { H , T } e. _V -> ( # |` ~P { H , T } ) e. ( measures ` ~P { H , T } ) )
21 8 20 ax-mp 
 |-  ( # |` ~P { H , T } ) e. ( measures ` ~P { H , T } )
22 2rp 
 |-  2 e. RR+
23 17 22 eqeltri 
 |-  ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) e. RR+
24 probfinmeasb 
 |-  ( ( ( # |` ~P { H , T } ) e. ( measures ` ~P { H , T } ) /\ ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) e. RR+ ) -> ( ( # |` ~P { H , T } ) oFC /e ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) ) e. Prob )
25 21 23 24 mp2an 
 |-  ( ( # |` ~P { H , T } ) oFC /e ( ( # |` ~P { H , T } ) ` U. ~P { H , T } ) ) e. Prob
26 19 25 eqeltri 
 |-  P e. Prob