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

### 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|↾}_{𝒫\left\{{H},{T}\right\}}\right){\circ }_{\mathrm{fc}}÷2$
5 coinflip.3 ${⊢}{X}=\left\{⟨{H},1⟩,⟨{T},0⟩\right\}$
6 1ex ${⊢}1\in \mathrm{V}$
7 c0ex ${⊢}0\in \mathrm{V}$
8 1 2 6 7 fpr ${⊢}{H}\ne {T}\to \left\{⟨{H},1⟩,⟨{T},0⟩\right\}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}$
9 3 8 ax-mp ${⊢}\left\{⟨{H},1⟩,⟨{T},0⟩\right\}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}$
10 5 feq1i ${⊢}{X}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}↔\left\{⟨{H},1⟩,⟨{T},0⟩\right\}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}$
11 9 10 mpbir ${⊢}{X}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}$
12 1 2 3 4 5 coinflipuniv ${⊢}\bigcup \mathrm{dom}{P}=\left\{{H},{T}\right\}$
13 12 feq2i ${⊢}{X}:\bigcup \mathrm{dom}{P}⟶\left\{1,0\right\}↔{X}:\left\{{H},{T}\right\}⟶\left\{1,0\right\}$
14 11 13 mpbir ${⊢}{X}:\bigcup \mathrm{dom}{P}⟶\left\{1,0\right\}$
15 1re ${⊢}1\in ℝ$
16 0re ${⊢}0\in ℝ$
17 15 16 pm3.2i ${⊢}\left(1\in ℝ\wedge 0\in ℝ\right)$
18 6 7 prss ${⊢}\left(1\in ℝ\wedge 0\in ℝ\right)↔\left\{1,0\right\}\subseteq ℝ$
19 17 18 mpbi ${⊢}\left\{1,0\right\}\subseteq ℝ$
20 fss ${⊢}\left({X}:\bigcup \mathrm{dom}{P}⟶\left\{1,0\right\}\wedge \left\{1,0\right\}\subseteq ℝ\right)\to {X}:\bigcup \mathrm{dom}{P}⟶ℝ$
21 14 19 20 mp2an ${⊢}{X}:\bigcup \mathrm{dom}{P}⟶ℝ$
22 imassrn ${⊢}{{X}}^{-1}\left[{y}\right]\subseteq \mathrm{ran}{{X}}^{-1}$
23 dfdm4 ${⊢}\mathrm{dom}{X}=\mathrm{ran}{{X}}^{-1}$
24 11 fdmi ${⊢}\mathrm{dom}{X}=\left\{{H},{T}\right\}$
25 23 24 eqtr3i ${⊢}\mathrm{ran}{{X}}^{-1}=\left\{{H},{T}\right\}$
26 22 25 sseqtri ${⊢}{{X}}^{-1}\left[{y}\right]\subseteq \left\{{H},{T}\right\}$
27 1 2 3 4 5 coinflipspace ${⊢}\mathrm{dom}{P}=𝒫\left\{{H},{T}\right\}$
28 27 eleq2i ${⊢}{{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}↔{{X}}^{-1}\left[{y}\right]\in 𝒫\left\{{H},{T}\right\}$
29 prex ${⊢}\left\{⟨{H},1⟩,⟨{T},0⟩\right\}\in \mathrm{V}$
30 5 29 eqeltri ${⊢}{X}\in \mathrm{V}$
31 cnvexg ${⊢}{X}\in \mathrm{V}\to {{X}}^{-1}\in \mathrm{V}$
32 imaexg ${⊢}{{X}}^{-1}\in \mathrm{V}\to {{X}}^{-1}\left[{y}\right]\in \mathrm{V}$
33 30 31 32 mp2b ${⊢}{{X}}^{-1}\left[{y}\right]\in \mathrm{V}$
34 33 elpw ${⊢}{{X}}^{-1}\left[{y}\right]\in 𝒫\left\{{H},{T}\right\}↔{{X}}^{-1}\left[{y}\right]\subseteq \left\{{H},{T}\right\}$
35 28 34 bitr2i ${⊢}{{X}}^{-1}\left[{y}\right]\subseteq \left\{{H},{T}\right\}↔{{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}$
36 35 biimpi ${⊢}{{X}}^{-1}\left[{y}\right]\subseteq \left\{{H},{T}\right\}\to {{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}$
37 26 36 mp1i ${⊢}{y}\in {𝔅}_{ℝ}\to {{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}$
38 37 rgen ${⊢}\forall {y}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}$
39 1 2 3 4 5 coinflipprob ${⊢}{P}\in \mathrm{Prob}$
40 39 a1i ${⊢}{H}\in \mathrm{V}\to {P}\in \mathrm{Prob}$
41 40 isrrvv ${⊢}{H}\in \mathrm{V}\to \left({X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)↔\left({X}:\bigcup \mathrm{dom}{P}⟶ℝ\wedge \forall {y}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}\right)\right)$
42 1 41 ax-mp ${⊢}{X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)↔\left({X}:\bigcup \mathrm{dom}{P}⟶ℝ\wedge \forall {y}\in {𝔅}_{ℝ}\phantom{\rule{.4em}{0ex}}{{X}}^{-1}\left[{y}\right]\in \mathrm{dom}{P}\right)$
43 21 38 42 mpbir2an ${⊢}{X}\in {\mathrm{RndVar}}_{ℝ}\left({P}\right)$