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 e. X , y e. ( 0 [,] 1 ) |-> if ( y <_ ( 1 / 2 ) , ( x L ( 2 x. y ) ) , ( x M ( ( 2 x. y ) - 1 ) ) ) )
htpycc.2 
|- ( ph -> J e. ( TopOn ` X ) )
htpycc.4 
|- ( ph -> F e. ( J Cn K ) )
htpycc.5 
|- ( ph -> G e. ( J Cn K ) )
htpycc.6 
|- ( ph -> H e. ( J Cn K ) )
htpycc.7 
|- ( ph -> L e. ( F ( J Htpy K ) G ) )
htpycc.8 
|- ( ph -> M e. ( G ( J Htpy K ) H ) )
Assertion htpycc 
|- ( ph -> N e. ( F ( J Htpy K ) H ) )

Proof

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