Metamath Proof Explorer

Theorem coinfliprv

Description: The X we defined for coin-flip is a random variable. (Contributed by Thierry Arnoux, 12-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 coinfliprv 
|- X e. ( rRndVar ` P )

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 1ex 
 |-  1 e. _V
7 c0ex 
 |-  0 e. _V
8 1 2 6 7 fpr 
 |-  ( H =/= T -> { <. H , 1 >. , <. T , 0 >. } : { H , T } --> { 1 , 0 } )
9 3 8 ax-mp 
 |-  { <. H , 1 >. , <. T , 0 >. } : { H , T } --> { 1 , 0 }
10 5 feq1i 
 |-  ( X : { H , T } --> { 1 , 0 } <-> { <. H , 1 >. , <. T , 0 >. } : { H , T } --> { 1 , 0 } )
11 9 10 mpbir 
 |-  X : { H , T } --> { 1 , 0 }
12 1 2 3 4 5 coinflipuniv 
 |-  U. dom P = { H , T }
13 12 feq2i 
 |-  ( X : U. dom P --> { 1 , 0 } <-> X : { H , T } --> { 1 , 0 } )
14 11 13 mpbir 
 |-  X : U. dom P --> { 1 , 0 }
15 1re 
 |-  1 e. RR
16 0re 
 |-  0 e. RR
17 15 16 pm3.2i 
 |-  ( 1 e. RR /\ 0 e. RR )
18 6 7 prss 
 |-  ( ( 1 e. RR /\ 0 e. RR ) <-> { 1 , 0 } C_ RR )
19 17 18 mpbi 
 |-  { 1 , 0 } C_ RR
20 fss 
 |-  ( ( X : U. dom P --> { 1 , 0 } /\ { 1 , 0 } C_ RR ) -> X : U. dom P --> RR )
21 14 19 20 mp2an 
 |-  X : U. dom P --> RR
22 imassrn 
 |-  ( `' X " y ) C_ ran `' X
23 dfdm4 
 |-  dom X = ran `' X
24 11 fdmi 
 |-  dom X = { H , T }
25 23 24 eqtr3i 
 |-  ran `' X = { H , T }
26 22 25 sseqtri 
 |-  ( `' X " y ) C_ { H , T }
27 1 2 3 4 5 coinflipspace 
 |-  dom P = ~P { H , T }
28 27 eleq2i 
 |-  ( ( `' X " y ) e. dom P <-> ( `' X " y ) e. ~P { H , T } )
29 prex 
 |-  { <. H , 1 >. , <. T , 0 >. } e. _V
30 5 29 eqeltri 
 |-  X e. _V
31 cnvexg 
 |-  ( X e. _V -> `' X e. _V )
32 imaexg 
 |-  ( `' X e. _V -> ( `' X " y ) e. _V )
33 30 31 32 mp2b 
 |-  ( `' X " y ) e. _V
34 33 elpw 
 |-  ( ( `' X " y ) e. ~P { H , T } <-> ( `' X " y ) C_ { H , T } )
35 28 34 bitr2i 
 |-  ( ( `' X " y ) C_ { H , T } <-> ( `' X " y ) e. dom P )
36 35 biimpi 
 |-  ( ( `' X " y ) C_ { H , T } -> ( `' X " y ) e. dom P )
37 26 36 mp1i 
 |-  ( y e. BrSiga -> ( `' X " y ) e. dom P )
38 37 rgen 
 |-  A. y e. BrSiga ( `' X " y ) e. dom P
39 1 2 3 4 5 coinflipprob 
 |-  P e. Prob
40 39 a1i 
 |-  ( H e. _V -> P e. Prob )
41 40 isrrvv 
 |-  ( H e. _V -> ( X e. ( rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) ) )
42 1 41 ax-mp 
 |-  ( X e. ( rRndVar ` P ) <-> ( X : U. dom P --> RR /\ A. y e. BrSiga ( `' X " y ) e. dom P ) )
43 21 38 42 mpbir2an 
 |-  X e. ( rRndVar ` P )