pcohtpy

Description: Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

	Ref	Expression
Hypotheses	pcohtpy.4	$⊢ φ \to F (1) = G (0)$
	pcohtpy.5	$⊢ φ \to F ≃_{ph} (J) H$
	pcohtpy.6	$⊢ φ \to G ≃_{ph} (J) K$
Assertion	pcohtpy	$⊢ φ \to (F _{𝑝} (J) G) ≃_{ph} (J) (H _{𝑝} (J) K)$

Proof

Step	Hyp	Ref	Expression
1		pcohtpy.4	$⊢ φ \to F (1) = G (0)$
2		pcohtpy.5	$⊢ φ \to F ≃_{ph} (J) H$
3		pcohtpy.6	$⊢ φ \to G ≃_{ph} (J) K$
4		isphtpc	$⊢ F ≃_{ph} (J) H \leftrightarrow (F \in (II Cn J) \land H \in (II Cn J) \land F PHtpy (J) H \neq \emptyset)$
5	2 4	sylib	$⊢ φ \to (F \in (II Cn J) \land H \in (II Cn J) \land F PHtpy (J) H \neq \emptyset)$
6	5	simp1d	$⊢ φ \to F \in (II Cn J)$
7		isphtpc	$⊢ G ≃_{ph} (J) K \leftrightarrow (G \in (II Cn J) \land K \in (II Cn J) \land G PHtpy (J) K \neq \emptyset)$
8	3 7	sylib	$⊢ φ \to (G \in (II Cn J) \land K \in (II Cn J) \land G PHtpy (J) K \neq \emptyset)$
9	8	simp1d	$⊢ φ \to G \in (II Cn J)$
10	6 9 1	pcocn	$⊢ φ \to F *_{𝑝} (J) G \in (II Cn J)$
11	5	simp2d	$⊢ φ \to H \in (II Cn J)$
12	8	simp2d	$⊢ φ \to K \in (II Cn J)$
13		phtpc01	$⊢ F ≃_{ph} (J) H \to (F (0) = H (0) \land F (1) = H (1))$
14	2 13	syl	$⊢ φ \to (F (0) = H (0) \land F (1) = H (1))$
15	14	simprd	$⊢ φ \to F (1) = H (1)$
16		phtpc01	$⊢ G ≃_{ph} (J) K \to (G (0) = K (0) \land G (1) = K (1))$
17	3 16	syl	$⊢ φ \to (G (0) = K (0) \land G (1) = K (1))$
18	17	simpld	$⊢ φ \to G (0) = K (0)$
19	1 15 18	3eqtr3d	$⊢ φ \to H (1) = K (0)$
20	11 12 19	pcocn	$⊢ φ \to H *_{𝑝} (J) K \in (II Cn J)$
21	5	simp3d	$⊢ φ \to F PHtpy (J) H \neq \emptyset$
22		n0	$⊢ F PHtpy (J) H \neq \emptyset \leftrightarrow \exists m m \in (F PHtpy (J) H)$
23	21 22	sylib	$⊢ φ \to \exists m m \in (F PHtpy (J) H)$
24	8	simp3d	$⊢ φ \to G PHtpy (J) K \neq \emptyset$
25		n0	$⊢ G PHtpy (J) K \neq \emptyset \leftrightarrow \exists n n \in (G PHtpy (J) K)$
26	24 25	sylib	$⊢ φ \to \exists n n \in (G PHtpy (J) K)$
27		exdistrv	$⊢ \exists m \exists n (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K)) \leftrightarrow (\exists m m \in (F PHtpy (J) H) \land \exists n n \in (G PHtpy (J) K))$
28	23 26 27	sylanbrc	$⊢ φ \to \exists m \exists n (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))$
29	1	adantr	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to F (1) = G (0)$
30	2	adantr	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to F ≃_{ph} (J) H$
31	3	adantr	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to G ≃_{ph} (J) K$
32		eqid	$⊢ (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x m y, (2 x - 1) n y)) = (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x m y, (2 x - 1) n y))$
33		simprl	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to m \in (F PHtpy (J) H)$
34		simprr	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to n \in (G PHtpy (J) K)$
35	29 30 31 32 33 34	pcohtpylem	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to (x \in [0, 1], y \in [0, 1] ⟼ if (x \leq \frac{1}{2}, 2 x m y, (2 x - 1) n y)) \in ((F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K))$
36	35	ne0d	$⊢ (φ \land (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K))) \to (F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K) \neq \emptyset$
37	36	ex	$⊢ φ \to ((m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K)) \to (F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K) \neq \emptyset)$
38	37	exlimdvv	$⊢ φ \to (\exists m \exists n (m \in (F PHtpy (J) H) \land n \in (G PHtpy (J) K)) \to (F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K) \neq \emptyset)$
39	28 38	mpd	$⊢ φ \to (F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K) \neq \emptyset$
40		isphtpc	$⊢ (F _{𝑝} (J) G) ≃_{ph} (J) (H _{𝑝} (J) K) \leftrightarrow (F _{𝑝} (J) G \in (II Cn J) \land H _{𝑝} (J) K \in (II Cn J) \land (F _{𝑝} (J) G) PHtpy (J) (H _{𝑝} (J) K) \neq \emptyset)$
41	10 20 39 40	syl3anbrc	$⊢ φ \to (F _{𝑝} (J) G) ≃_{ph} (J) (H _{𝑝} (J) K)$

Metamath Proof Explorer

Theorem pcohtpy

Proof