phtpycc

Description: Concatenate two path homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 7-Jun-2014)

	Ref	Expression
Hypotheses	phtpycc.1	$⊢ M = (x \in [0, 1], y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, x K 2 y, x L (2 y - 1)))$
	phtpycc.3	$⊢ φ \to F \in (II Cn J)$
	phtpycc.4	$⊢ φ \to G \in (II Cn J)$
	phtpycc.5	$⊢ φ \to H \in (II Cn J)$
	phtpycc.6	$⊢ φ \to K \in (F PHtpy (J) G)$
	phtpycc.7	$⊢ φ \to L \in (G PHtpy (J) H)$
Assertion	phtpycc	$⊢ φ \to M \in (F PHtpy (J) H)$

Proof

Step	Hyp	Ref	Expression
1		phtpycc.1	$⊢ M = (x \in [0, 1], y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, x K 2 y, x L (2 y - 1)))$
2		phtpycc.3	$⊢ φ \to F \in (II Cn J)$
3		phtpycc.4	$⊢ φ \to G \in (II Cn J)$
4		phtpycc.5	$⊢ φ \to H \in (II Cn J)$
5		phtpycc.6	$⊢ φ \to K \in (F PHtpy (J) G)$
6		phtpycc.7	$⊢ φ \to L \in (G PHtpy (J) H)$
7		iitopon	$⊢ II \in TopOn ([0, 1])$
8	7	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
9	2 3	phtpyhtpy	$⊢ φ \to F PHtpy (J) G \subseteq F (II Htpy J) G$
10	9 5	sseldd	$⊢ φ \to K \in (F (II Htpy J) G)$
11	3 4	phtpyhtpy	$⊢ φ \to G PHtpy (J) H \subseteq G (II Htpy J) H$
12	11 6	sseldd	$⊢ φ \to L \in (G (II Htpy J) H)$
13	1 8 2 3 4 10 12	htpycc	$⊢ φ \to M \in (F (II Htpy J) H)$
14		0elunit	$⊢ 0 \in [0, 1]$
15		simpr	$⊢ (φ \land s \in [0, 1]) \to s \in [0, 1]$
16		simpr	$⊢ (x = 0 \land y = s) \to y = s$
17	16	breq1d	$⊢ (x = 0 \land y = s) \to (y \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
18		simpl	$⊢ (x = 0 \land y = s) \to x = 0$
19	16	oveq2d	$⊢ (x = 0 \land y = s) \to 2 y = 2 s$
20	18 19	oveq12d	$⊢ (x = 0 \land y = s) \to x K 2 y = 0 K 2 s$
21	19	oveq1d	$⊢ (x = 0 \land y = s) \to 2 y - 1 = 2 s - 1$
22	18 21	oveq12d	$⊢ (x = 0 \land y = s) \to x L (2 y - 1) = 0 L (2 s - 1)$
23	17 20 22	ifbieq12d	$⊢ (x = 0 \land y = s) \to if (y \leq \frac{1}{2}, x K 2 y, x L (2 y - 1)) = if (s \leq \frac{1}{2}, 0 K 2 s, 0 L (2 s - 1))$
24		ovex	$⊢ 0 K 2 s \in V$
25		ovex	$⊢ 0 L (2 s - 1) \in V$
26	24 25	ifex	$⊢ if (s \leq \frac{1}{2}, 0 K 2 s, 0 L (2 s - 1)) \in V$
27	23 1 26	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 M s = if (s \leq \frac{1}{2}, 0 K 2 s, 0 L (2 s - 1))$
28	14 15 27	sylancr	$⊢ (φ \land s \in [0, 1]) \to 0 M s = if (s \leq \frac{1}{2}, 0 K 2 s, 0 L (2 s - 1))$
29		simpll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to φ$
30		elii1	$⊢ s \in [0, \frac{1}{2}] \leftrightarrow (s \in [0, 1] \land s \leq \frac{1}{2})$
31		iihalf1	$⊢ s \in [0, \frac{1}{2}] \to 2 s \in [0, 1]$
32	30 31	sylbir	$⊢ (s \in [0, 1] \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
33	32	adantll	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 2 s \in [0, 1]$
34	2 3 5	phtpyi	$⊢ (φ \land 2 s \in [0, 1]) \to (0 K 2 s = F (0) \land 1 K 2 s = F (1))$
35	29 33 34	syl2anc	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to (0 K 2 s = F (0) \land 1 K 2 s = F (1))$
36	35	simpld	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 0 K 2 s = F (0)$
37		simpll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to φ$
38		elii2	$⊢ (s \in [0, 1] \land \neg s \leq \frac{1}{2}) \to s \in [\frac{1}{2}, 1]$
39		iihalf2	$⊢ s \in [\frac{1}{2}, 1] \to 2 s - 1 \in [0, 1]$
40	38 39	syl	$⊢ (s \in [0, 1] \land \neg s \leq \frac{1}{2}) \to 2 s - 1 \in [0, 1]$
41	40	adantll	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 2 s - 1 \in [0, 1]$
42	3 4 6	phtpyi	$⊢ (φ \land 2 s - 1 \in [0, 1]) \to (0 L (2 s - 1) = G (0) \land 1 L (2 s - 1) = G (1))$
43	37 41 42	syl2anc	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (0 L (2 s - 1) = G (0) \land 1 L (2 s - 1) = G (1))$
44	43	simpld	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 0 L (2 s - 1) = G (0)$
45	2 3 5	phtpy01	$⊢ φ \to (F (0) = G (0) \land F (1) = G (1))$
46	45	ad2antrr	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to (F (0) = G (0) \land F (1) = G (1))$
47	46	simpld	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to F (0) = G (0)$
48	44 47	eqtr4d	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 0 L (2 s - 1) = F (0)$
49	36 48	ifeqda	$⊢ (φ \land s \in [0, 1]) \to if (s \leq \frac{1}{2}, 0 K 2 s, 0 L (2 s - 1)) = F (0)$
50	28 49	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 0 M s = F (0)$
51		1elunit	$⊢ 1 \in [0, 1]$
52		simpr	$⊢ (x = 1 \land y = s) \to y = s$
53	52	breq1d	$⊢ (x = 1 \land y = s) \to (y \leq \frac{1}{2} \leftrightarrow s \leq \frac{1}{2})$
54		simpl	$⊢ (x = 1 \land y = s) \to x = 1$
55	52	oveq2d	$⊢ (x = 1 \land y = s) \to 2 y = 2 s$
56	54 55	oveq12d	$⊢ (x = 1 \land y = s) \to x K 2 y = 1 K 2 s$
57	55	oveq1d	$⊢ (x = 1 \land y = s) \to 2 y - 1 = 2 s - 1$
58	54 57	oveq12d	$⊢ (x = 1 \land y = s) \to x L (2 y - 1) = 1 L (2 s - 1)$
59	53 56 58	ifbieq12d	$⊢ (x = 1 \land y = s) \to if (y \leq \frac{1}{2}, x K 2 y, x L (2 y - 1)) = if (s \leq \frac{1}{2}, 1 K 2 s, 1 L (2 s - 1))$
60		ovex	$⊢ 1 K 2 s \in V$
61		ovex	$⊢ 1 L (2 s - 1) \in V$
62	60 61	ifex	$⊢ if (s \leq \frac{1}{2}, 1 K 2 s, 1 L (2 s - 1)) \in V$
63	59 1 62	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 M s = if (s \leq \frac{1}{2}, 1 K 2 s, 1 L (2 s - 1))$
64	51 15 63	sylancr	$⊢ (φ \land s \in [0, 1]) \to 1 M s = if (s \leq \frac{1}{2}, 1 K 2 s, 1 L (2 s - 1))$
65	35	simprd	$⊢ ((φ \land s \in [0, 1]) \land s \leq \frac{1}{2}) \to 1 K 2 s = F (1)$
66	43	simprd	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 1 L (2 s - 1) = G (1)$
67	46	simprd	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to F (1) = G (1)$
68	66 67	eqtr4d	$⊢ ((φ \land s \in [0, 1]) \land \neg s \leq \frac{1}{2}) \to 1 L (2 s - 1) = F (1)$
69	65 68	ifeqda	$⊢ (φ \land s \in [0, 1]) \to if (s \leq \frac{1}{2}, 1 K 2 s, 1 L (2 s - 1)) = F (1)$
70	64 69	eqtrd	$⊢ (φ \land s \in [0, 1]) \to 1 M s = F (1)$
71	2 4 13 50 70	isphtpyd	$⊢ φ \to M \in (F PHtpy (J) H)$

Metamath Proof Explorer

Theorem phtpycc

Proof