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 |