coinfliplem

Description: Division in the extended real numbers can be used for the coin-flip example. (Contributed by Thierry Arnoux, 15-Jan-2017)

	Ref	Expression
Hypotheses	coinflip.h	$⊢ H \in V$
	coinflip.t	$⊢ T \in V$
	coinflip.th	$⊢ H \neq T$
	coinflip.2	$⊢ P = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div 2$
	coinflip.3	$⊢ X = \{⟨H, 1⟩, ⟨T, 0⟩\}$
Assertion	coinfliplem	$⊢ P = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div_{𝑒} 2$

Proof

Step	Hyp	Ref	Expression
1		coinflip.h	$⊢ H \in V$
2		coinflip.t	$⊢ T \in V$
3		coinflip.th	$⊢ H \neq T$
4		coinflip.2	$⊢ P = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div 2$
5		coinflip.3	$⊢ X = \{⟨H, 1⟩, ⟨T, 0⟩\}$
6		simpr	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to x \in 𝒫 \{H, T\}$
7		fvres	$⊢ x \in 𝒫 \{H, T\} \to ({\|.\| ↾}_{𝒫 \{H, T\}}) (x) = \|x\|$
8	6 7	syl	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to ({\|.\| ↾}_{𝒫 \{H, T\}}) (x) = \|x\|$
9		prfi	$⊢ \{H, T\} \in Fin$
10	6	elpwid	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to x \subseteq \{H, T\}$
11		ssfi	$⊢ (\{H, T\} \in Fin \land x \subseteq \{H, T\}) \to x \in Fin$
12	9 10 11	sylancr	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to x \in Fin$
13		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
14	12 13	syl	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to \|x\| \in ℕ_{0}$
15	14	nn0red	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to \|x\| \in ℝ$
16	8 15	eqeltrd	$⊢ (H \in V \land x \in 𝒫 \{H, T\}) \to ({\|.\| ↾}_{𝒫 \{H, T\}}) (x) \in ℝ$
17		simpr	$⊢ (H \in V \land y \in ℝ) \to y \in ℝ$
18		2re	$⊢ 2 \in ℝ$
19	18	a1i	$⊢ (H \in V \land y \in ℝ) \to 2 \in ℝ$
20		2ne0	$⊢ 2 \neq 0$
21	20	a1i	$⊢ (H \in V \land y \in ℝ) \to 2 \neq 0$
22		rexdiv	$⊢ (y \in ℝ \land 2 \in ℝ \land 2 \neq 0) \to y \div_{𝑒} 2 = \frac{y}{2}$
23	17 19 21 22	syl3anc	$⊢ (H \in V \land y \in ℝ) \to y \div_{𝑒} 2 = \frac{y}{2}$
24		hashresfn	$⊢ ({\|.\| ↾}_{𝒫 \{H, T\}}) Fn 𝒫 \{H, T\}$
25	24	a1i	$⊢ H \in V \to ({\|.\| ↾}_{𝒫 \{H, T\}}) Fn 𝒫 \{H, T\}$
26		pwfi	$⊢ \{H, T\} \in Fin \leftrightarrow 𝒫 \{H, T\} \in Fin$
27	9 26	mpbi	$⊢ 𝒫 \{H, T\} \in Fin$
28	27	a1i	$⊢ H \in V \to 𝒫 \{H, T\} \in Fin$
29	18	a1i	$⊢ H \in V \to 2 \in ℝ$
30	16 23 25 28 29	ofcfeqd2	$⊢ H \in V \to ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div_{𝑒} 2 = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div 2$
31	1 30	ax-mp	$⊢ ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div_{𝑒} 2 = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div 2$
32	4 31	eqtr4i	$⊢ P = ({\|.\| ↾}_{𝒫 \{H, T\}}) \circ_{fc} \div_{𝑒} 2$

Metamath Proof Explorer

Theorem coinfliplem

Proof