Metamath Proof Explorer

Theorem coinflippv

Description: The probability of heads is one-half. (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 coinflippv 
|- ( P ` { H } ) = ( 1 / 2 )

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 4 fveq1i 
 |-  ( P ` { H } ) = ( ( ( # |` ~P { H , T } ) oFC / 2 ) ` { H } )
7 snsspr1 
 |-  { H } C_ { H , T }
8 prex 
 |-  { H , T } e. _V
9 8 elpw2 
 |-  ( { H } e. ~P { H , T } <-> { H } C_ { H , T } )
10 9 biimpri 
 |-  ( { H } C_ { H , T } -> { H } e. ~P { H , T } )
11 fveq2 
 |-  ( x = { H } -> ( # ` x ) = ( # ` { H } ) )
12 hashsng 
 |-  ( H e. _V -> ( # ` { H } ) = 1 )
13 1 12 ax-mp 
 |-  ( # ` { H } ) = 1
14 11 13 eqtrdi 
 |-  ( x = { H } -> ( # ` x ) = 1 )
15 14 oveq1d 
 |-  ( x = { H } -> ( ( # ` x ) / 2 ) = ( 1 / 2 ) )
16 8 pwex 
 |-  ~P { H , T } e. _V
17 16 a1i 
 |-  ( H e. _V -> ~P { H , T } e. _V )
18 2nn0 
 |-  2 e. NN0
19 18 a1i 
 |-  ( H e. _V -> 2 e. NN0 )
20 prfi 
 |-  { H , T } e. Fin
21 elpwi 
 |-  ( x e. ~P { H , T } -> x C_ { H , T } )
22 ssfi 
 |-  ( ( { H , T } e. Fin /\ x C_ { H , T } ) -> x e. Fin )
23 20 21 22 sylancr 
 |-  ( x e. ~P { H , T } -> x e. Fin )
24 23 adantl 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> x e. Fin )
25 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
26 24 25 syl 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> ( # ` x ) e. NN0 )
27 hashf 
 |-  # : _V --> ( NN0 u. { +oo } )
28 27 a1i 
 |-  ( H e. _V -> # : _V --> ( NN0 u. { +oo } ) )
29 ssv 
 |-  ~P { H , T } C_ _V
30 29 a1i 
 |-  ( H e. _V -> ~P { H , T } C_ _V )
31 28 30 feqresmpt 
 |-  ( H e. _V -> ( # |` ~P { H , T } ) = ( x e. ~P { H , T } |-> ( # ` x ) ) )
32 17 19 26 31 ofcfval2 
 |-  ( H e. _V -> ( ( # |` ~P { H , T } ) oFC / 2 ) = ( x e. ~P { H , T } |-> ( ( # ` x ) / 2 ) ) )
33 1 32 ax-mp 
 |-  ( ( # |` ~P { H , T } ) oFC / 2 ) = ( x e. ~P { H , T } |-> ( ( # ` x ) / 2 ) )
34 ovex 
 |-  ( 1 / 2 ) e. _V
35 15 33 34 fvmpt 
 |-  ( { H } e. ~P { H , T } -> ( ( ( # |` ~P { H , T } ) oFC / 2 ) ` { H } ) = ( 1 / 2 ) )
36 7 10 35 mp2b 
 |-  ( ( ( # |` ~P { H , T } ) oFC / 2 ) ` { H } ) = ( 1 / 2 )
37 6 36 eqtri 
 |-  ( P ` { H } ) = ( 1 / 2 )