Metamath Proof Explorer


Theorem 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 X , y 0 1 if y 1 2 x L 2 y x M 2 y 1
htpycc.2 φ J TopOn X
htpycc.4 φ F J Cn K
htpycc.5 φ G J Cn K
htpycc.6 φ H J Cn K
htpycc.7 φ L F J Htpy K G
htpycc.8 φ M G J Htpy K H
Assertion htpycc φ N F J Htpy K H

Proof

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