Metamath Proof Explorer

Theorem coinfliplem

Description: Division in the extended real numbers can be used for the coin-flip example. (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 coinfliplem 
|- P = ( ( # |` ~P { H , T } ) oFC /e 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 simpr 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> x e. ~P { H , T } )
7 fvres 
 |-  ( x e. ~P { H , T } -> ( ( # |` ~P { H , T } ) ` x ) = ( # ` x ) )
8 6 7 syl 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> ( ( # |` ~P { H , T } ) ` x ) = ( # ` x ) )
9 prfi 
 |-  { H , T } e. Fin
10 6 elpwid 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> x C_ { H , T } )
11 ssfi 
 |-  ( ( { H , T } e. Fin /\ x C_ { H , T } ) -> x e. Fin )
12 9 10 11 sylancr 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> x e. Fin )
13 hashcl 
 |-  ( x e. Fin -> ( # ` x ) e. NN0 )
14 12 13 syl 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> ( # ` x ) e. NN0 )
15 14 nn0red 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> ( # ` x ) e. RR )
16 8 15 eqeltrd 
 |-  ( ( H e. _V /\ x e. ~P { H , T } ) -> ( ( # |` ~P { H , T } ) ` x ) e. RR )
17 simpr 
 |-  ( ( H e. _V /\ y e. RR ) -> y e. RR )
18 2re 
 |-  2 e. RR
19 18 a1i 
 |-  ( ( H e. _V /\ y e. RR ) -> 2 e. RR )
20 2ne0 
 |-  2 =/= 0
21 20 a1i 
 |-  ( ( H e. _V /\ y e. RR ) -> 2 =/= 0 )
22 rexdiv 
 |-  ( ( y e. RR /\ 2 e. RR /\ 2 =/= 0 ) -> ( y /e 2 ) = ( y / 2 ) )
23 17 19 21 22 syl3anc 
 |-  ( ( H e. _V /\ y e. RR ) -> ( y /e 2 ) = ( y / 2 ) )
24 hashresfn 
 |-  ( # |` ~P { H , T } ) Fn ~P { H , T }
25 24 a1i 
 |-  ( H e. _V -> ( # |` ~P { H , T } ) Fn ~P { H , T } )
26 pwfi 
 |-  ( { H , T } e. Fin <-> ~P { H , T } e. Fin )
27 9 26 mpbi 
 |-  ~P { H , T } e. Fin
28 27 a1i 
 |-  ( H e. _V -> ~P { H , T } e. Fin )
29 18 a1i 
 |-  ( H e. _V -> 2 e. RR )
30 16 23 25 28 29 ofcfeqd2 
 |-  ( H e. _V -> ( ( # |` ~P { H , T } ) oFC /e 2 ) = ( ( # |` ~P { H , T } ) oFC / 2 ) )
31 1 30 ax-mp 
 |-  ( ( # |` ~P { H , T } ) oFC /e 2 ) = ( ( # |` ~P { H , T } ) oFC / 2 )
32 4 31 eqtr4i 
 |-  P = ( ( # |` ~P { H , T } ) oFC /e 2 )