Metamath Proof Explorer

Theorem htpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses ishtpy.1 
|- ( ph -> J e. ( TopOn ` X ) )
ishtpy.3 
|- ( ph -> F e. ( J Cn K ) )
ishtpy.4 
|- ( ph -> G e. ( J Cn K ) )
htpycom.6 
|- M = ( x e. X , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )
htpycom.7 
|- ( ph -> H e. ( F ( J Htpy K ) G ) )
Assertion htpycom 
|- ( ph -> M e. ( G ( J Htpy K ) F ) )

Proof

Step Hyp Ref Expression
1 ishtpy.1 
 |-  ( ph -> J e. ( TopOn ` X ) )
2 ishtpy.3 
 |-  ( ph -> F e. ( J Cn K ) )
3 ishtpy.4 
 |-  ( ph -> G e. ( J Cn K ) )
4 htpycom.6 
 |-  M = ( x e. X , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) )
5 htpycom.7 
 |-  ( ph -> H e. ( F ( J Htpy K ) G ) )
6 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
7 6 a1i 
 |-  ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
8 1 7 cnmpt1st 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> x ) e. ( ( J tX II ) Cn J ) )
9 1 7 cnmpt2nd 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> y ) e. ( ( J tX II ) Cn II ) )
10 iirevcn 
 |-  ( z e. ( 0 [,] 1 ) |-> ( 1 - z ) ) e. ( II Cn II )
11 10 a1i 
 |-  ( ph -> ( z e. ( 0 [,] 1 ) |-> ( 1 - z ) ) e. ( II Cn II ) )
12 oveq2 
 |-  ( z = y -> ( 1 - z ) = ( 1 - y ) )
13 1 7 9 7 11 12 cnmpt21 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> ( 1 - y ) ) e. ( ( J tX II ) Cn II ) )
14 1 2 3 htpycn 
 |-  ( ph -> ( F ( J Htpy K ) G ) C_ ( ( J tX II ) Cn K ) )
15 14 5 sseldd 
 |-  ( ph -> H e. ( ( J tX II ) Cn K ) )
16 1 7 8 13 15 cnmpt22f 
 |-  ( ph -> ( x e. X , y e. ( 0 [,] 1 ) |-> ( x H ( 1 - y ) ) ) e. ( ( J tX II ) Cn K ) )
17 4 16 eqeltrid 
 |-  ( ph -> M e. ( ( J tX II ) Cn K ) )
18 simpr 
 |-  ( ( ph /\ t e. X ) -> t e. X )
19 0elunit 
 |-  0 e. ( 0 [,] 1 )
20 oveq1 
 |-  ( x = t -> ( x H ( 1 - y ) ) = ( t H ( 1 - y ) ) )
21 oveq2 
 |-  ( y = 0 -> ( 1 - y ) = ( 1 - 0 ) )
22 1m0e1 
 |-  ( 1 - 0 ) = 1
23 21 22 eqtrdi 
 |-  ( y = 0 -> ( 1 - y ) = 1 )
24 23 oveq2d 
 |-  ( y = 0 -> ( t H ( 1 - y ) ) = ( t H 1 ) )
25 ovex 
 |-  ( t H 1 ) e. _V
26 20 24 4 25 ovmpo 
 |-  ( ( t e. X /\ 0 e. ( 0 [,] 1 ) ) -> ( t M 0 ) = ( t H 1 ) )
27 18 19 26 sylancl 
 |-  ( ( ph /\ t e. X ) -> ( t M 0 ) = ( t H 1 ) )
28 1 2 3 5 htpyi 
 |-  ( ( ph /\ t e. X ) -> ( ( t H 0 ) = ( F ` t ) /\ ( t H 1 ) = ( G ` t ) ) )
29 28 simprd 
 |-  ( ( ph /\ t e. X ) -> ( t H 1 ) = ( G ` t ) )
30 27 29 eqtrd 
 |-  ( ( ph /\ t e. X ) -> ( t M 0 ) = ( G ` t ) )
31 1elunit 
 |-  1 e. ( 0 [,] 1 )
32 oveq2 
 |-  ( y = 1 -> ( 1 - y ) = ( 1 - 1 ) )
33 1m1e0 
 |-  ( 1 - 1 ) = 0
34 32 33 eqtrdi 
 |-  ( y = 1 -> ( 1 - y ) = 0 )
35 34 oveq2d 
 |-  ( y = 1 -> ( t H ( 1 - y ) ) = ( t H 0 ) )
36 ovex 
 |-  ( t H 0 ) e. _V
37 20 35 4 36 ovmpo 
 |-  ( ( t e. X /\ 1 e. ( 0 [,] 1 ) ) -> ( t M 1 ) = ( t H 0 ) )
38 18 31 37 sylancl 
 |-  ( ( ph /\ t e. X ) -> ( t M 1 ) = ( t H 0 ) )
39 28 simpld 
 |-  ( ( ph /\ t e. X ) -> ( t H 0 ) = ( F ` t ) )
40 38 39 eqtrd 
 |-  ( ( ph /\ t e. X ) -> ( t M 1 ) = ( F ` t ) )
41 1 3 2 17 30 40 ishtpyd 
 |-  ( ph -> M e. ( G ( J Htpy K ) F ) )