# 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 ) )`