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 φ J TopOn X
ishtpy.3 φ F J Cn K
ishtpy.4 φ G J Cn K
htpycom.6 M = x X , y 0 1 x H 1 y
htpycom.7 φ H F J Htpy K G
Assertion htpycom φ M G J Htpy K F

Proof

Step Hyp Ref Expression
1 ishtpy.1 φ J TopOn X
2 ishtpy.3 φ F J Cn K
3 ishtpy.4 φ G J Cn K
4 htpycom.6 M = x X , y 0 1 x H 1 y
5 htpycom.7 φ H F J Htpy K G
6 iitopon II TopOn 0 1
7 6 a1i φ II TopOn 0 1
8 1 7 cnmpt1st φ x X , y 0 1 x J × t II Cn J
9 1 7 cnmpt2nd φ x X , y 0 1 y J × t II Cn II
10 iirevcn z 0 1 1 z II Cn II
11 10 a1i φ z 0 1 1 z II Cn II
12 oveq2 z = y 1 z = 1 y
13 1 7 9 7 11 12 cnmpt21 φ x X , y 0 1 1 y J × t II Cn II
14 1 2 3 htpycn φ F J Htpy K G J × t II Cn K
15 14 5 sseldd φ H J × t II Cn K
16 1 7 8 13 15 cnmpt22f φ x X , y 0 1 x H 1 y J × t II Cn K
17 4 16 eqeltrid φ M J × t II Cn K
18 simpr φ t X t X
19 0elunit 0 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 V
26 20 24 4 25 ovmpo t X 0 0 1 t M 0 = t H 1
27 18 19 26 sylancl φ t X t M 0 = t H 1
28 1 2 3 5 htpyi φ t X t H 0 = F t t H 1 = G t
29 28 simprd φ t X t H 1 = G t
30 27 29 eqtrd φ t X t M 0 = G t
31 1elunit 1 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 V
37 20 35 4 36 ovmpo t X 1 0 1 t M 1 = t H 0
38 18 31 37 sylancl φ t X t M 1 = t H 0
39 28 simpld φ t X t H 0 = F t
40 38 39 eqtrd φ t X t M 1 = F t
41 1 3 2 17 30 40 ishtpyd φ M G J Htpy K F