phtpcer

Description: Path homotopy is an equivalence relation. Proposition 1.2 of Hatcher p. 26. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 6-Jul-2015) (Proof shortened by AV, 1-May-2021)

		Ref	Expression
	Assertion	phtpcer	$⊢ ≃_{ph} (J) Er (II Cn J)$

Proof

Step	Hyp	Ref	Expression
1		phtpcrel	$⊢ Rel ≃_{ph} (J)$
2		isphtpc	$⊢ x ≃_{ph} (J) y \leftrightarrow (x \in (II Cn J) \land y \in (II Cn J) \land x PHtpy (J) y \neq \emptyset)$
3	2	simp2bi	$⊢ x ≃_{ph} (J) y \to y \in (II Cn J)$
4	2	simp1bi	$⊢ x ≃_{ph} (J) y \to x \in (II Cn J)$
5	2	simp3bi	$⊢ x ≃_{ph} (J) y \to x PHtpy (J) y \neq \emptyset$
6		n0	$⊢ x PHtpy (J) y \neq \emptyset \leftrightarrow \exists f f \in (x PHtpy (J) y)$
7	5 6	sylib	$⊢ x ≃_{ph} (J) y \to \exists f f \in (x PHtpy (J) y)$
8	4	adantr	$⊢ (x ≃_{ph} (J) y \land f \in (x PHtpy (J) y)) \to x \in (II Cn J)$
9	3	adantr	$⊢ (x ≃_{ph} (J) y \land f \in (x PHtpy (J) y)) \to y \in (II Cn J)$
10		eqid	$⊢ (u \in [0, 1], v \in [0, 1] ⟼ u f (1 - v)) = (u \in [0, 1], v \in [0, 1] ⟼ u f (1 - v))$
11		simpr	$⊢ (x ≃_{ph} (J) y \land f \in (x PHtpy (J) y)) \to f \in (x PHtpy (J) y)$
12	8 9 10 11	phtpycom	$⊢ (x ≃_{ph} (J) y \land f \in (x PHtpy (J) y)) \to (u \in [0, 1], v \in [0, 1] ⟼ u f (1 - v)) \in (y PHtpy (J) x)$
13	12	ne0d	$⊢ (x ≃_{ph} (J) y \land f \in (x PHtpy (J) y)) \to y PHtpy (J) x \neq \emptyset$
14	7 13	exlimddv	$⊢ x ≃_{ph} (J) y \to y PHtpy (J) x \neq \emptyset$
15		isphtpc	$⊢ y ≃_{ph} (J) x \leftrightarrow (y \in (II Cn J) \land x \in (II Cn J) \land y PHtpy (J) x \neq \emptyset)$
16	3 4 14 15	syl3anbrc	$⊢ x ≃_{ph} (J) y \to y ≃_{ph} (J) x$
17	4	adantr	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to x \in (II Cn J)$
18		simpr	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to y ≃_{ph} (J) z$
19		isphtpc	$⊢ y ≃_{ph} (J) z \leftrightarrow (y \in (II Cn J) \land z \in (II Cn J) \land y PHtpy (J) z \neq \emptyset)$
20	18 19	sylib	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to (y \in (II Cn J) \land z \in (II Cn J) \land y PHtpy (J) z \neq \emptyset)$
21	20	simp2d	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to z \in (II Cn J)$
22	5	adantr	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to x PHtpy (J) y \neq \emptyset$
23	22 6	sylib	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to \exists f f \in (x PHtpy (J) y)$
24	20	simp3d	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to y PHtpy (J) z \neq \emptyset$
25		n0	$⊢ y PHtpy (J) z \neq \emptyset \leftrightarrow \exists g g \in (y PHtpy (J) z)$
26	24 25	sylib	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to \exists g g \in (y PHtpy (J) z)$
27		exdistrv	$⊢ \exists f \exists g (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z)) \leftrightarrow (\exists f f \in (x PHtpy (J) y) \land \exists g g \in (y PHtpy (J) z))$
28	23 26 27	sylanbrc	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to \exists f \exists g (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))$
29		eqid	$⊢ (u \in [0, 1], v \in [0, 1] ⟼ if (v \leq \frac{1}{2}, u f 2 v, u g (2 v - 1))) = (u \in [0, 1], v \in [0, 1] ⟼ if (v \leq \frac{1}{2}, u f 2 v, u g (2 v - 1)))$
30	17	adantr	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to x \in (II Cn J)$
31	20	simp1d	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to y \in (II Cn J)$
32	31	adantr	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to y \in (II Cn J)$
33	21	adantr	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to z \in (II Cn J)$
34		simprl	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to f \in (x PHtpy (J) y)$
35		simprr	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to g \in (y PHtpy (J) z)$
36	29 30 32 33 34 35	phtpycc	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to (u \in [0, 1], v \in [0, 1] ⟼ if (v \leq \frac{1}{2}, u f 2 v, u g (2 v - 1))) \in (x PHtpy (J) z)$
37	36	ne0d	$⊢ ((x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \land (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z))) \to x PHtpy (J) z \neq \emptyset$
38	37	ex	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to ((f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z)) \to x PHtpy (J) z \neq \emptyset)$
39	38	exlimdvv	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to (\exists f \exists g (f \in (x PHtpy (J) y) \land g \in (y PHtpy (J) z)) \to x PHtpy (J) z \neq \emptyset)$
40	28 39	mpd	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to x PHtpy (J) z \neq \emptyset$
41		isphtpc	$⊢ x ≃_{ph} (J) z \leftrightarrow (x \in (II Cn J) \land z \in (II Cn J) \land x PHtpy (J) z \neq \emptyset)$
42	17 21 40 41	syl3anbrc	$⊢ (x ≃_{ph} (J) y \land y ≃_{ph} (J) z) \to x ≃_{ph} (J) z$
43		eqid	$⊢ (y \in [0, 1], z \in [0, 1] ⟼ x (y)) = (y \in [0, 1], z \in [0, 1] ⟼ x (y))$
44		id	$⊢ x \in (II Cn J) \to x \in (II Cn J)$
45	43 44	phtpyid	$⊢ x \in (II Cn J) \to (y \in [0, 1], z \in [0, 1] ⟼ x (y)) \in (x PHtpy (J) x)$
46	45	ne0d	$⊢ x \in (II Cn J) \to x PHtpy (J) x \neq \emptyset$
47	46	ancli	$⊢ x \in (II Cn J) \to (x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset)$
48	47	pm4.71ri	$⊢ x \in (II Cn J) \leftrightarrow ((x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset) \land x \in (II Cn J))$
49		df-3an	$⊢ (x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset \land x \in (II Cn J)) \leftrightarrow ((x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset) \land x \in (II Cn J))$
50		3ancomb	$⊢ (x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset \land x \in (II Cn J)) \leftrightarrow (x \in (II Cn J) \land x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset)$
51	48 49 50	3bitr2i	$⊢ x \in (II Cn J) \leftrightarrow (x \in (II Cn J) \land x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset)$
52		isphtpc	$⊢ x ≃_{ph} (J) x \leftrightarrow (x \in (II Cn J) \land x \in (II Cn J) \land x PHtpy (J) x \neq \emptyset)$
53	51 52	bitr4i	$⊢ x \in (II Cn J) \leftrightarrow x ≃_{ph} (J) x$
54	1 16 42 53	iseri	$⊢ ≃_{ph} (J) Er (II Cn J)$

Metamath Proof Explorer

Theorem phtpcer

Proof