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\in \mathrm{V}$$
	coinflip.t	$$⊢T\in \mathrm{V}$$
	coinflip.th	$$⊢H\ne T$$
	coinflip.2	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2$$
	coinflip.3	$$⊢X=\left\{⟨H,1⟩,⟨T,0⟩\right\}$$
Assertion	coinflipprob	$$⊢P\in \mathrm{Prob}$$

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	$$⊢H\in \mathrm{V}$$
2		coinflip.t	$$⊢T\in \mathrm{V}$$
3		coinflip.th	$$⊢H\ne T$$
4		coinflip.2	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}÷2$$
5		coinflip.3	$$⊢X=\left\{⟨H,1⟩,⟨T,0⟩\right\}$$
6	1 2 3 4 5	coinfliplem	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}2$$
7		unipw	$$⊢\bigcup 𝒫\left\{H,T\right\}=\left\{H,T\right\}$$
8		prex	$$⊢\left\{H,T\right\}\in \mathrm{V}$$
9	8	pwid	$$⊢\left\{H,T\right\}\in 𝒫\left\{H,T\right\}$$
10	7 9	eqeltri	$$⊢\bigcup 𝒫\left\{H,T\right\}\in 𝒫\left\{H,T\right\}$$
11		fvres	$$⊢\bigcup 𝒫\left\{H,T\right\}\in 𝒫\left\{H,T\right\}\to \left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)=\left|\bigcup 𝒫\left\{H,T\right\}\right|$$
12	10 11	ax-mp	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)=\left|\bigcup 𝒫\left\{H,T\right\}\right|$$
13	7	fveq2i	$$⊢\left|\bigcup 𝒫\left\{H,T\right\}\right|=\left|\left\{H,T\right\}\right|$$
14		hashprg	$$⊢\left(H\in \mathrm{V}\wedge T\in \mathrm{V}\right)\to \left(H\ne T\leftrightarrow \left|\left\{H,T\right\}\right|=2\right)$$
15	1 2 14	mp2an	$$⊢H\ne T\leftrightarrow \left|\left\{H,T\right\}\right|=2$$
16	3 15	mpbi	$$⊢\left|\left\{H,T\right\}\right|=2$$
17	12 13 16	3eqtri	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)=2$$
18	17	oveq2i	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}2$$
19	6 18	eqtr4i	$$⊢P=\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)$$
20		pwcntmeas	$$⊢\left\{H,T\right\}\in \mathrm{V}\to {\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\in \mathrm{measures}\left(𝒫\left\{H,T\right\}\right)$$
21	8 20	ax-mp	$$⊢{\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\in \mathrm{measures}\left(𝒫\left\{H,T\right\}\right)$$
22		2rp	$$⊢2\in {ℝ}^{+}$$
23	17 22	eqeltri	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)\in {ℝ}^{+}$$
24		probfinmeasb	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\in \mathrm{measures}\left(𝒫\left\{H,T\right\}\right)\wedge \left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)\in {ℝ}^{+}\right)\to \left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)\in \mathrm{Prob}$$
25	21 23 24	mp2an	$$⊢\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right){\circ }_{\mathrm{fc}}{÷}_{𝑒}\left({\left|.\right|\upharpoonright }_{𝒫\left\{H,T\right\}}\right)\left(\bigcup 𝒫\left\{H,T\right\}\right)\in \mathrm{Prob}$$
26	19 25	eqeltri	$$⊢P\in \mathrm{Prob}$$