htpycc

Description: Concatenate two homotopies. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

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

Proof

Step	Hyp	Ref	Expression
1		htpycc.1	$⊢ N = (x \in X, y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1)))$
2		htpycc.2	$⊢ φ \to J \in TopOn (X)$
3		htpycc.4	$⊢ φ \to F \in (J Cn K)$
4		htpycc.5	$⊢ φ \to G \in (J Cn K)$
5		htpycc.6	$⊢ φ \to H \in (J Cn K)$
6		htpycc.7	$⊢ φ \to L \in (F (J Htpy K) G)$
7		htpycc.8	$⊢ φ \to M \in (G (J Htpy K) H)$
8		iitopon	$⊢ II \in TopOn ([0, 1])$
9	8	a1i	$⊢ φ \to II \in TopOn ([0, 1])$
10		eqid	$⊢ topGen (ran (.)) = topGen (ran (.))$
11		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] = topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]$
12		eqid	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] = topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]$
13		dfii2	$⊢ II = topGen (ran (.)) ↾_{𝑡} [0, 1]$
14		0red	$⊢ φ \to 0 \in ℝ$
15		1red	$⊢ φ \to 1 \in ℝ$
16		halfre	$⊢ \frac{1}{2} \in ℝ$
17		halfge0	$⊢ 0 \leq \frac{1}{2}$
18		1re	$⊢ 1 \in ℝ$
19		halflt1	$⊢ \frac{1}{2} < 1$
20	16 18 19	ltleii	$⊢ \frac{1}{2} \leq 1$
21		elicc01	$⊢ \frac{1}{2} \in [0, 1] \leftrightarrow (\frac{1}{2} \in ℝ \land 0 \leq \frac{1}{2} \land \frac{1}{2} \leq 1)$
22	16 17 20 21	mpbir3an	$⊢ \frac{1}{2} \in [0, 1]$
23	22	a1i	$⊢ φ \to \frac{1}{2} \in [0, 1]$
24	2 3 4 6	htpyi	$⊢ (φ \land s \in X) \to (s L 0 = F (s) \land s L 1 = G (s))$
25	24	simprd	$⊢ (φ \land s \in X) \to s L 1 = G (s)$
26	2 4 5 7	htpyi	$⊢ (φ \land s \in X) \to (s M 0 = G (s) \land s M 1 = H (s))$
27	26	simpld	$⊢ (φ \land s \in X) \to s M 0 = G (s)$
28	25 27	eqtr4d	$⊢ (φ \land s \in X) \to s L 1 = s M 0$
29	28	ralrimiva	$⊢ φ \to \forall s \in X s L 1 = s M 0$
30		oveq1	$⊢ s = x \to s L 1 = x L 1$
31		oveq1	$⊢ s = x \to s M 0 = x M 0$
32	30 31	eqeq12d	$⊢ s = x \to (s L 1 = s M 0 \leftrightarrow x L 1 = x M 0)$
33	32	rspccva	$⊢ (\forall s \in X s L 1 = s M 0 \land x \in X) \to x L 1 = x M 0$
34	29 33	sylan	$⊢ (φ \land x \in X) \to x L 1 = x M 0$
35	34	adantrl	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x L 1 = x M 0$
36		simprl	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to y = \frac{1}{2}$
37	36	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y = 2 (\frac{1}{2})$
38		2cn	$⊢ 2 \in ℂ$
39		2ne0	$⊢ 2 \neq 0$
40	38 39	recidi	$⊢ 2 (\frac{1}{2}) = 1$
41	37 40	syl6eq	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y = 1$
42	41	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x L 2 y = x L 1$
43	41	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y - 1 = 1 - 1$
44		1m1e0	$⊢ 1 - 1 = 0$
45	43 44	syl6eq	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y - 1 = 0$
46	45	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x M (2 y - 1) = x M 0$
47	35 42 46	3eqtr4d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x L 2 y = x M (2 y - 1)$
48		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
49		0re	$⊢ 0 \in ℝ$
50		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
51	49 16 50	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
52		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
53	48 51 52	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
54	53	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
55	54 2	cnmpt2nd	$⊢ φ \to (y \in [0, \frac{1}{2}], x \in X ⟼ x) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} J) Cn J)$
56	54 2	cnmpt1st	$⊢ φ \to (y \in [0, \frac{1}{2}], x \in X ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} J) Cn (topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]))$
57	11	iihalf1cn	$⊢ (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
58	57	a1i	$⊢ φ \to (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
59		oveq2	$⊢ z = y \to 2 z = 2 y$
60	54 2 56 54 58 59	cnmpt21	$⊢ φ \to (y \in [0, \frac{1}{2}], x \in X ⟼ 2 y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} J) Cn II)$
61	2 3 4	htpycn	$⊢ φ \to F (J Htpy K) G \subseteq (J \times_{t} II) Cn K$
62	61 6	sseldd	$⊢ φ \to L \in ((J \times_{t} II) Cn K)$
63	54 2 55 60 62	cnmpt22f	$⊢ φ \to (y \in [0, \frac{1}{2}], x \in X ⟼ x L 2 y) \in (((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) \times_{t} J) Cn K)$
64		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
65	16 18 64	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
66		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
67	48 65 66	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
68	67	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
69	68 2	cnmpt2nd	$⊢ φ \to (y \in [\frac{1}{2}, 1], x \in X ⟼ x) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} J) Cn J)$
70	68 2	cnmpt1st	$⊢ φ \to (y \in [\frac{1}{2}, 1], x \in X ⟼ y) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} J) Cn (topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]))$
71	12	iihalf2cn	$⊢ (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
72	71	a1i	$⊢ φ \to (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
73	59	oveq1d	$⊢ z = y \to 2 z - 1 = 2 y - 1$
74	68 2 70 68 72 73	cnmpt21	$⊢ φ \to (y \in [\frac{1}{2}, 1], x \in X ⟼ 2 y - 1) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} J) Cn II)$
75	2 4 5	htpycn	$⊢ φ \to G (J Htpy K) H \subseteq (J \times_{t} II) Cn K$
76	75 7	sseldd	$⊢ φ \to M \in ((J \times_{t} II) Cn K)$
77	68 2 69 74 76	cnmpt22f	$⊢ φ \to (y \in [\frac{1}{2}, 1], x \in X ⟼ x M (2 y - 1)) \in (((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) \times_{t} J) Cn K)$
78	10 11 12 13 14 15 23 2 47 63 77	cnmpopc	$⊢ φ \to (y \in [0, 1], x \in X ⟼ if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1))) \in ((II \times_{t} J) Cn K)$
79	9 2 78	cnmptcom	$⊢ φ \to (x \in X, y \in [0, 1] ⟼ if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1))) \in ((J \times_{t} II) Cn K)$
80	1 79	eqeltrid	$⊢ φ \to N \in ((J \times_{t} II) Cn K)$
81		simpr	$⊢ (φ \land s \in X) \to s \in X$
82		0elunit	$⊢ 0 \in [0, 1]$
83		simpr	$⊢ (x = s \land y = 0) \to y = 0$
84	83 17	eqbrtrdi	$⊢ (x = s \land y = 0) \to y \leq \frac{1}{2}$
85	84	iftrued	$⊢ (x = s \land y = 0) \to if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1)) = x L 2 y$
86		simpl	$⊢ (x = s \land y = 0) \to x = s$
87	83	oveq2d	$⊢ (x = s \land y = 0) \to 2 y = 2 \cdot 0$
88		2t0e0	$⊢ 2 \cdot 0 = 0$
89	87 88	syl6eq	$⊢ (x = s \land y = 0) \to 2 y = 0$
90	86 89	oveq12d	$⊢ (x = s \land y = 0) \to x L 2 y = s L 0$
91	85 90	eqtrd	$⊢ (x = s \land y = 0) \to if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1)) = s L 0$
92		ovex	$⊢ s L 0 \in V$
93	91 1 92	ovmpoa	$⊢ (s \in X \land 0 \in [0, 1]) \to s N 0 = s L 0$
94	81 82 93	sylancl	$⊢ (φ \land s \in X) \to s N 0 = s L 0$
95	24	simpld	$⊢ (φ \land s \in X) \to s L 0 = F (s)$
96	94 95	eqtrd	$⊢ (φ \land s \in X) \to s N 0 = F (s)$
97		1elunit	$⊢ 1 \in [0, 1]$
98	16 18	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
99	19 98	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
100		simpr	$⊢ (x = s \land y = 1) \to y = 1$
101	100	breq1d	$⊢ (x = s \land y = 1) \to (y \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
102	99 101	mtbiri	$⊢ (x = s \land y = 1) \to \neg y \leq \frac{1}{2}$
103	102	iffalsed	$⊢ (x = s \land y = 1) \to if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1)) = x M (2 y - 1)$
104		simpl	$⊢ (x = s \land y = 1) \to x = s$
105	100	oveq2d	$⊢ (x = s \land y = 1) \to 2 y = 2 \cdot 1$
106		2t1e2	$⊢ 2 \cdot 1 = 2$
107	105 106	syl6eq	$⊢ (x = s \land y = 1) \to 2 y = 2$
108	107	oveq1d	$⊢ (x = s \land y = 1) \to 2 y - 1 = 2 - 1$
109		2m1e1	$⊢ 2 - 1 = 1$
110	108 109	syl6eq	$⊢ (x = s \land y = 1) \to 2 y - 1 = 1$
111	104 110	oveq12d	$⊢ (x = s \land y = 1) \to x M (2 y - 1) = s M 1$
112	103 111	eqtrd	$⊢ (x = s \land y = 1) \to if (y \leq \frac{1}{2}, x L 2 y, x M (2 y - 1)) = s M 1$
113		ovex	$⊢ s M 1 \in V$
114	112 1 113	ovmpoa	$⊢ (s \in X \land 1 \in [0, 1]) \to s N 1 = s M 1$
115	81 97 114	sylancl	$⊢ (φ \land s \in X) \to s N 1 = s M 1$
116	26	simprd	$⊢ (φ \land s \in X) \to s M 1 = H (s)$
117	115 116	eqtrd	$⊢ (φ \land s \in X) \to s N 1 = H (s)$
118	2 3 5 80 96 117	ishtpyd	$⊢ φ \to N \in (F (J Htpy K) H)$

Metamath Proof Explorer

Theorem htpycc

Proof