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		2thalfe1	$⊢ 2 (\frac{1}{2}) = 1$
39	37 38	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y = 1$
40	39	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x L 2 y = x L 1$
41	39	oveq1d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y - 1 = 1 - 1$
42		1m1e0	$⊢ 1 - 1 = 0$
43	41 42	eqtrdi	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to 2 y - 1 = 0$
44	43	oveq2d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x M (2 y - 1) = x M 0$
45	35 40 44	3eqtr4d	$⊢ (φ \land (y = \frac{1}{2} \land x \in X)) \to x L 2 y = x M (2 y - 1)$
46		retopon	$⊢ topGen (ran (.)) \in TopOn (ℝ)$
47		0re	$⊢ 0 \in ℝ$
48		iccssre	$⊢ (0 \in ℝ \land \frac{1}{2} \in ℝ) \to [0, \frac{1}{2}] \subseteq ℝ$
49	47 16 48	mp2an	$⊢ [0, \frac{1}{2}] \subseteq ℝ$
50		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [0, \frac{1}{2}] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
51	46 49 50	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
52	51	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}] \in TopOn ([0, \frac{1}{2}])$
53	52 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)$
54	52 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}]))$
55	11	iihalf1cn	$⊢ (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
56	55	a1i	$⊢ φ \to (z \in [0, \frac{1}{2}] ⟼ 2 z) \in ((topGen (ran (.)) ↾_{𝑡} [0, \frac{1}{2}]) Cn II)$
57		oveq2	$⊢ z = y \to 2 z = 2 y$
58	52 2 54 52 56 57	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)$
59	2 3 4	htpycn	$⊢ φ \to F (J Htpy K) G \subseteq (J \times_{t} II) Cn K$
60	59 6	sseldd	$⊢ φ \to L \in ((J \times_{t} II) Cn K)$
61	52 2 53 58 60	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)$
62		iccssre	$⊢ (\frac{1}{2} \in ℝ \land 1 \in ℝ) \to [\frac{1}{2}, 1] \subseteq ℝ$
63	16 18 62	mp2an	$⊢ [\frac{1}{2}, 1] \subseteq ℝ$
64		resttopon	$⊢ (topGen (ran (.)) \in TopOn (ℝ) \land [\frac{1}{2}, 1] \subseteq ℝ) \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
65	46 63 64	mp2an	$⊢ topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
66	65	a1i	$⊢ φ \to topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1] \in TopOn ([\frac{1}{2}, 1])$
67	66 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)$
68	66 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]))$
69	12	iihalf2cn	$⊢ (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
70	69	a1i	$⊢ φ \to (z \in [\frac{1}{2}, 1] ⟼ 2 z - 1) \in ((topGen (ran (.)) ↾_{𝑡} [\frac{1}{2}, 1]) Cn II)$
71	57	oveq1d	$⊢ z = y \to 2 z - 1 = 2 y - 1$
72	66 2 68 66 70 71	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)$
73	2 4 5	htpycn	$⊢ φ \to G (J Htpy K) H \subseteq (J \times_{t} II) Cn K$
74	73 7	sseldd	$⊢ φ \to M \in ((J \times_{t} II) Cn K)$
75	66 2 67 72 74	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)$
76	10 11 12 13 14 15 23 2 45 61 75	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)$
77	9 2 76	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)$
78	1 77	eqeltrid	$⊢ φ \to N \in ((J \times_{t} II) Cn K)$
79		simpr	$⊢ (φ \land s \in X) \to s \in X$
80		0elunit	$⊢ 0 \in [0, 1]$
81		simpr	$⊢ (x = s \land y = 0) \to y = 0$
82	81 17	eqbrtrdi	$⊢ (x = s \land y = 0) \to y \leq \frac{1}{2}$
83	82	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$
84		simpl	$⊢ (x = s \land y = 0) \to x = s$
85	81	oveq2d	$⊢ (x = s \land y = 0) \to 2 y = 2 \cdot 0$
86		2t0e0	$⊢ 2 \cdot 0 = 0$
87	85 86	eqtrdi	$⊢ (x = s \land y = 0) \to 2 y = 0$
88	84 87	oveq12d	$⊢ (x = s \land y = 0) \to x L 2 y = s L 0$
89	83 88	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$
90		ovex	$⊢ s L 0 \in V$
91	89 1 90	ovmpoa	$⊢ (s \in X \land 0 \in [0, 1]) \to s N 0 = s L 0$
92	79 80 91	sylancl	$⊢ (φ \land s \in X) \to s N 0 = s L 0$
93	24	simpld	$⊢ (φ \land s \in X) \to s L 0 = F (s)$
94	92 93	eqtrd	$⊢ (φ \land s \in X) \to s N 0 = F (s)$
95		1elunit	$⊢ 1 \in [0, 1]$
96	16 18	ltnlei	$⊢ \frac{1}{2} < 1 \leftrightarrow \neg 1 \leq \frac{1}{2}$
97	19 96	mpbi	$⊢ \neg 1 \leq \frac{1}{2}$
98		simpr	$⊢ (x = s \land y = 1) \to y = 1$
99	98	breq1d	$⊢ (x = s \land y = 1) \to (y \leq \frac{1}{2} \leftrightarrow 1 \leq \frac{1}{2})$
100	97 99	mtbiri	$⊢ (x = s \land y = 1) \to \neg y \leq \frac{1}{2}$
101	100	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)$
102		simpl	$⊢ (x = s \land y = 1) \to x = s$
103	98	oveq2d	$⊢ (x = s \land y = 1) \to 2 y = 2 \cdot 1$
104		2t1e2	$⊢ 2 \cdot 1 = 2$
105	103 104	eqtrdi	$⊢ (x = s \land y = 1) \to 2 y = 2$
106	105	oveq1d	$⊢ (x = s \land y = 1) \to 2 y - 1 = 2 - 1$
107		2m1e1	$⊢ 2 - 1 = 1$
108	106 107	eqtrdi	$⊢ (x = s \land y = 1) \to 2 y - 1 = 1$
109	102 108	oveq12d	$⊢ (x = s \land y = 1) \to x M (2 y - 1) = s M 1$
110	101 109	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$
111		ovex	$⊢ s M 1 \in V$
112	110 1 111	ovmpoa	$⊢ (s \in X \land 1 \in [0, 1]) \to s N 1 = s M 1$
113	79 95 112	sylancl	$⊢ (φ \land s \in X) \to s N 1 = s M 1$
114	26	simprd	$⊢ (φ \land s \in X) \to s M 1 = H (s)$
115	113 114	eqtrd	$⊢ (φ \land s \in X) \to s N 1 = H (s)$
116	2 3 5 78 94 115	ishtpyd	$⊢ φ \to N \in (F (J Htpy K) H)$

Metamath Proof Explorer

Theorem htpycc

Proof