Metamath Proof Explorer


Theorem phtpy01

Description: Two path-homotopic paths have the same start and end point. (Contributed by Mario Carneiro, 23-Feb-2015)

Ref Expression
Hypotheses isphtpy.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
isphtpy.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
phtpyi.1 ( 𝜑𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
Assertion phtpy01 ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )

Proof

Step Hyp Ref Expression
1 isphtpy.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 phtpyi.1 ( 𝜑𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
4 1elunit 1 ∈ ( 0 [,] 1 )
5 1 2 3 phtpyi ( ( 𝜑 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 1 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 1 ) = ( 𝐹 ‘ 1 ) ) )
6 4 5 mpan2 ( 𝜑 → ( ( 0 𝐻 1 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 1 ) = ( 𝐹 ‘ 1 ) ) )
7 6 simpld ( 𝜑 → ( 0 𝐻 1 ) = ( 𝐹 ‘ 0 ) )
8 0elunit 0 ∈ ( 0 [,] 1 )
9 iitopon II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
10 9 a1i ( 𝜑 → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
11 1 2 phtpyhtpy ( 𝜑 → ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ⊆ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
12 11 3 sseldd ( 𝜑𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) )
13 10 1 2 12 htpyi ( ( 𝜑 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 0 𝐻 1 ) = ( 𝐺 ‘ 0 ) ) )
14 8 13 mpan2 ( 𝜑 → ( ( 0 𝐻 0 ) = ( 𝐹 ‘ 0 ) ∧ ( 0 𝐻 1 ) = ( 𝐺 ‘ 0 ) ) )
15 14 simprd ( 𝜑 → ( 0 𝐻 1 ) = ( 𝐺 ‘ 0 ) )
16 7 15 eqtr3d ( 𝜑 → ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) )
17 6 simprd ( 𝜑 → ( 1 𝐻 1 ) = ( 𝐹 ‘ 1 ) )
18 10 1 2 12 htpyi ( ( 𝜑 ∧ 1 ∈ ( 0 [,] 1 ) ) → ( ( 1 𝐻 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 1 𝐻 1 ) = ( 𝐺 ‘ 1 ) ) )
19 4 18 mpan2 ( 𝜑 → ( ( 1 𝐻 0 ) = ( 𝐹 ‘ 1 ) ∧ ( 1 𝐻 1 ) = ( 𝐺 ‘ 1 ) ) )
20 19 simprd ( 𝜑 → ( 1 𝐻 1 ) = ( 𝐺 ‘ 1 ) )
21 17 20 eqtr3d ( 𝜑 → ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
22 16 21 jca ( 𝜑 → ( ( 𝐹 ‘ 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 𝐹 ‘ 1 ) = ( 𝐺 ‘ 1 ) ) )