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 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
isphtpy.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
phtpycom.6 ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
phtpycom.7 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
Assertion phtpycom ( 𝜑 → 𝐾 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 ⊢ ( 𝜑 → 𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
3 phtpycom.6 ⊢ 𝐾 = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
4 phtpycom.7 ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
5 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
6 5 a1i ⊢ ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
7 1 2 phtpyhtpy ⊢ ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
8 7 4 sseldd ⊢ ( 𝜑 → 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
9 6 1 2 3 8 htpycom ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 ( II Htpy 𝐽 ) 𝐹 ) )
10 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
11 simpr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
12 oveq1 ⊢ ( 𝑥 = 0 → ( 𝑥 𝐻 ( 1 − 𝑦 ) ) = ( 0 𝐻 ( 1 − 𝑦 ) ) )
13 oveq2 ⊢ ( 𝑦 = 𝑡 → ( 1 − 𝑦 ) = ( 1 − 𝑡 ) )
14 13 oveq2d ⊢ ( 𝑦 = 𝑡 → ( 0 𝐻 ( 1 − 𝑦 ) ) = ( 0 𝐻 ( 1 − 𝑡 ) ) )
15 ovex ⊢ ( 0 𝐻 ( 1 − 𝑡 ) ) ∈ V
16 12 14 3 15 ovmpo ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 0 𝐾 𝑡 ) = ( 0 𝐻 ( 1 − 𝑡 ) ) )
17 10 11 16 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 0 𝐾 𝑡 ) = ( 0 𝐻 ( 1 − 𝑡 ) ) )
18 iirev ⊢ ( 𝑡 ∈ ( 0 [,] 1 ) → ( 1 − 𝑡 ) ∈ ( 0 [,] 1 ) )
19 1 2 4 phtpyi ⊢ ( ( 𝜑 ∧ ( 1 − 𝑡 ) ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 1 ) ) )
20 18 19 sylan2 ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 1 ) ) )
21 20 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 0 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 0 ) )
22 1 2 4 phtpy01 ⊢ ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
23 22 adantr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )
24 23 simpld ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
25 17 21 24 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 0 𝐾 𝑡 ) = ( 𝐺 ‘ 0 ) )
26 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
27 oveq1 ⊢ ( 𝑥 = 1 → ( 𝑥 𝐻 ( 1 − 𝑦 ) ) = ( 1 𝐻 ( 1 − 𝑦 ) ) )
28 13 oveq2d ⊢ ( 𝑦 = 𝑡 → ( 1 𝐻 ( 1 − 𝑦 ) ) = ( 1 𝐻 ( 1 − 𝑡 ) ) )
29 ovex ⊢ ( 1 𝐻 ( 1 − 𝑡 ) ) ∈ V
30 27 28 3 29 ovmpo ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 𝐾 𝑡 ) = ( 1 𝐻 ( 1 − 𝑡 ) ) )
31 26 11 30 sylancr ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 𝐾 𝑡 ) = ( 1 𝐻 ( 1 − 𝑡 ) ) )
32 20 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 𝐻 ( 1 − 𝑡 ) ) = ( 𝐹 ‘ 1 ) )
33 23 simprd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
34 31 32 33 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 𝐾 𝑡 ) = ( 𝐺 ‘ 1 ) )
35 2 1 9 25 34 isphtpyd ⊢ ( 𝜑 → 𝐾 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐹 ) )