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