# 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 ‘ 𝐽 ) 𝐹 ) )