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 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
ishtpy.3 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
ishtpy.4 ( 𝜑𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
htpycom.6 𝑀 = ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
htpycom.7 ( 𝜑𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
Assertion htpycom ( 𝜑𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )

Proof

Step Hyp Ref Expression
1 ishtpy.1 ( 𝜑𝐽 ∈ ( TopOn ‘ 𝑋 ) )
2 ishtpy.3 ( 𝜑𝐹 ∈ ( 𝐽 Cn 𝐾 ) )
3 ishtpy.4 ( 𝜑𝐺 ∈ ( 𝐽 Cn 𝐾 ) )
4 htpycom.6 𝑀 = ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) )
5 htpycom.7 ( 𝜑𝐻 ∈ ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) )
6 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
7 6 a1i ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
8 1 7 cnmpt1st ( 𝜑 → ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑥 ) ∈ ( ( 𝐽 ×t II ) Cn 𝐽 ) )
9 1 7 cnmpt2nd ( 𝜑 → ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ 𝑦 ) ∈ ( ( 𝐽 ×t II ) Cn II ) )
10 iirevcn ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑧 ) ) ∈ ( II Cn II )
11 10 a1i ( 𝜑 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑧 ) ) ∈ ( II Cn II ) )
12 oveq2 ( 𝑧 = 𝑦 → ( 1 − 𝑧 ) = ( 1 − 𝑦 ) )
13 1 7 9 7 11 12 cnmpt21 ( 𝜑 → ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑦 ) ) ∈ ( ( 𝐽 ×t II ) Cn II ) )
14 1 2 3 htpycn ( 𝜑 → ( 𝐹 ( 𝐽 Htpy 𝐾 ) 𝐺 ) ⊆ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
15 14 5 sseldd ( 𝜑𝐻 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
16 1 7 8 13 15 cnmpt22f ( 𝜑 → ( 𝑥𝑋 , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐻 ( 1 − 𝑦 ) ) ) ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
17 4 16 eqeltrid ( 𝜑𝑀 ∈ ( ( 𝐽 ×t II ) Cn 𝐾 ) )
18 simpr ( ( 𝜑𝑡𝑋 ) → 𝑡𝑋 )
19 0elunit 0 ∈ ( 0 [,] 1 )
20 oveq1 ( 𝑥 = 𝑡 → ( 𝑥 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 ( 1 − 𝑦 ) ) )
21 oveq2 ( 𝑦 = 0 → ( 1 − 𝑦 ) = ( 1 − 0 ) )
22 1m0e1 ( 1 − 0 ) = 1
23 21 22 eqtrdi ( 𝑦 = 0 → ( 1 − 𝑦 ) = 1 )
24 23 oveq2d ( 𝑦 = 0 → ( 𝑡 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 1 ) )
25 ovex ( 𝑡 𝐻 1 ) ∈ V
26 20 24 4 25 ovmpo ( ( 𝑡𝑋 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑡 𝑀 0 ) = ( 𝑡 𝐻 1 ) )
27 18 19 26 sylancl ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝑀 0 ) = ( 𝑡 𝐻 1 ) )
28 1 2 3 5 htpyi ( ( 𝜑𝑡𝑋 ) → ( ( 𝑡 𝐻 0 ) = ( 𝐹𝑡 ) ∧ ( 𝑡 𝐻 1 ) = ( 𝐺𝑡 ) ) )
29 28 simprd ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝐻 1 ) = ( 𝐺𝑡 ) )
30 27 29 eqtrd ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝑀 0 ) = ( 𝐺𝑡 ) )
31 1elunit 1 ∈ ( 0 [,] 1 )
32 oveq2 ( 𝑦 = 1 → ( 1 − 𝑦 ) = ( 1 − 1 ) )
33 1m1e0 ( 1 − 1 ) = 0
34 32 33 eqtrdi ( 𝑦 = 1 → ( 1 − 𝑦 ) = 0 )
35 34 oveq2d ( 𝑦 = 1 → ( 𝑡 𝐻 ( 1 − 𝑦 ) ) = ( 𝑡 𝐻 0 ) )
36 ovex ( 𝑡 𝐻 0 ) ∈ V
37 20 35 4 36 ovmpo ( ( 𝑡𝑋 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑡 𝑀 1 ) = ( 𝑡 𝐻 0 ) )
38 18 31 37 sylancl ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝑀 1 ) = ( 𝑡 𝐻 0 ) )
39 28 simpld ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝐻 0 ) = ( 𝐹𝑡 ) )
40 38 39 eqtrd ( ( 𝜑𝑡𝑋 ) → ( 𝑡 𝑀 1 ) = ( 𝐹𝑡 ) )
41 1 3 2 17 30 40 ishtpyd ( 𝜑𝑀 ∈ ( 𝐺 ( 𝐽 Htpy 𝐾 ) 𝐹 ) )