Theorem coinflipspace

Description: The space of our coin-flip probability. (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	coinflipspace	|- dom P = ~P { H , T }

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	dmeqi	|- dom P = dom ( ( # |` ~P { H , T } ) oFC / 2 )
7		hashresfn	|- ( # |` ~P { H , T } ) Fn ~P { H , T }
8	7	a1i	|- ( H e. _V -> ( # |` ~P { H , T } ) Fn ~P { H , T } )
9		prex	|- { H , T } e. _V
10		pwexg	|- ( { H , T } e. _V -> ~P { H , T } e. _V )
11	9 10	mp1i	|- ( H e. _V -> ~P { H , T } e. _V )
12		2re	|- 2 e. RR
13	12	a1i	|- ( H e. _V -> 2 e. RR )
14	8 11 13	ofcfn	|- ( H e. _V -> ( ( # |` ~P { H , T } ) oFC / 2 ) Fn ~P { H , T } )
15		fndm	|- ( ( ( # |` ~P { H , T } ) oFC / 2 ) Fn ~P { H , T } -> dom ( ( # |` ~P { H , T } ) oFC / 2 ) = ~P { H , T } )
16	1 14 15	mp2b	|- dom ( ( # |` ~P { H , T } ) oFC / 2 ) = ~P { H , T }
17	6 16	eqtri	|- dom P = ~P { H , T }