Metamath Proof Explorer

Theorem phtpycom

Description: Given a homotopy from F to G , produce a homotopy from G to F . (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ⊢ φ → F ∈ II Cn J
isphtpy.3 ⊢ φ → G ∈ II Cn J
phtpycom.6 ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ x H 1 − y
phtpycom.7 ⊢ φ → H ∈ F PHtpy ⁡ J G
Assertion phtpycom ⊢ φ → K ∈ G PHtpy ⁡ J F

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ φ → F ∈ II Cn J
2 isphtpy.3 ⊢ φ → G ∈ II Cn J
3 phtpycom.6 ⊢ K = x ∈ 0 1 , y ∈ 0 1 ⟼ x H 1 − y
4 phtpycom.7 ⊢ φ → H ∈ F PHtpy ⁡ J G
5 iitopon ⊢ II ∈ TopOn ⁡ 0 1
6 5 a1i ⊢ φ → II ∈ TopOn ⁡ 0 1
7 1 2 phtpyhtpy ⊢ φ → F PHtpy ⁡ J G ⊆ F II Htpy J G
8 7 4 sseldd ⊢ φ → H ∈ F II Htpy J G
9 6 1 2 3 8 htpycom ⊢ φ → K ∈ G II Htpy J F
10 0elunit ⊢ 0 ∈ 0 1
11 simpr ⊢ φ ∧ t ∈ 0 1 → t ∈ 0 1
12 oveq1 ⊢ x = 0 → x H 1 − y = 0 H 1 − y
13 oveq2 ⊢ y = t → 1 − y = 1 − t
14 13 oveq2d ⊢ y = t → 0 H 1 − y = 0 H 1 − t
15 ovex ⊢ 0 H 1 − t ∈ V
16 12 14 3 15 ovmpo ⊢ 0 ∈ 0 1 ∧ t ∈ 0 1 → 0 K t = 0 H 1 − t
17 10 11 16 sylancr ⊢ φ ∧ t ∈ 0 1 → 0 K t = 0 H 1 − t
18 iirev ⊢ t ∈ 0 1 → 1 − t ∈ 0 1
19 1 2 4 phtpyi ⊢ φ ∧ 1 − t ∈ 0 1 → 0 H 1 − t = F ⁡ 0 ∧ 1 H 1 − t = F ⁡ 1
20 18 19 sylan2 ⊢ φ ∧ t ∈ 0 1 → 0 H 1 − t = F ⁡ 0 ∧ 1 H 1 − t = F ⁡ 1
21 20 simpld ⊢ φ ∧ t ∈ 0 1 → 0 H 1 − t = F ⁡ 0
22 1 2 4 phtpy01 ⊢ φ → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
23 22 adantr ⊢ φ ∧ t ∈ 0 1 → F ⁡ 0 = G ⁡ 0 ∧ F ⁡ 1 = G ⁡ 1
24 23 simpld ⊢ φ ∧ t ∈ 0 1 → F ⁡ 0 = G ⁡ 0
25 17 21 24 3eqtrd ⊢ φ ∧ t ∈ 0 1 → 0 K t = G ⁡ 0
26 1elunit ⊢ 1 ∈ 0 1
27 oveq1 ⊢ x = 1 → x H 1 − y = 1 H 1 − y
28 13 oveq2d ⊢ y = t → 1 H 1 − y = 1 H 1 − t
29 ovex ⊢ 1 H 1 − t ∈ V
30 27 28 3 29 ovmpo ⊢ 1 ∈ 0 1 ∧ t ∈ 0 1 → 1 K t = 1 H 1 − t
31 26 11 30 sylancr ⊢ φ ∧ t ∈ 0 1 → 1 K t = 1 H 1 − t
32 20 simprd ⊢ φ ∧ t ∈ 0 1 → 1 H 1 − t = F ⁡ 1
33 23 simprd ⊢ φ ∧ t ∈ 0 1 → F ⁡ 1 = G ⁡ 1
34 31 32 33 3eqtrd ⊢ φ ∧ t ∈ 0 1 → 1 K t = G ⁡ 1
35 2 1 9 25 34 isphtpyd ⊢ φ → K ∈ G PHtpy ⁡ J F