Metamath Proof Explorer


Theorem phtpyi

Description: Membership in the class of path homotopies between two continuous functions. (Contributed by Mario Carneiro, 23-Feb-2015)

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

Proof

Step Hyp Ref Expression
1 isphtpy.2 ( 𝜑𝐹 ∈ ( II Cn 𝐽 ) )
2 isphtpy.3 ( 𝜑𝐺 ∈ ( II Cn 𝐽 ) )
3 phtpyi.1 ( 𝜑𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) )
4 1 2 isphtpy ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( PHtpy ‘ 𝐽 ) 𝐺 ) ↔ ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) ) )
5 3 4 mpbid ( 𝜑 → ( 𝐻 ∈ ( 𝐹 ( II Htpy 𝐽 ) 𝐺 ) ∧ ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ) )
6 5 simprd ( 𝜑 → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) )
7 oveq2 ( 𝑠 = 𝐴 → ( 0 𝐻 𝑠 ) = ( 0 𝐻 𝐴 ) )
8 7 eqeq1d ( 𝑠 = 𝐴 → ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ↔ ( 0 𝐻 𝐴 ) = ( 𝐹 ‘ 0 ) ) )
9 oveq2 ( 𝑠 = 𝐴 → ( 1 𝐻 𝑠 ) = ( 1 𝐻 𝐴 ) )
10 9 eqeq1d ( 𝑠 = 𝐴 → ( ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ↔ ( 1 𝐻 𝐴 ) = ( 𝐹 ‘ 1 ) ) )
11 8 10 anbi12d ( 𝑠 = 𝐴 → ( ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ↔ ( ( 0 𝐻 𝐴 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝐴 ) = ( 𝐹 ‘ 1 ) ) ) )
12 11 rspccva ( ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 0 𝐻 𝑠 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝑠 ) = ( 𝐹 ‘ 1 ) ) ∧ 𝐴 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 𝐴 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝐴 ) = ( 𝐹 ‘ 1 ) ) )
13 6 12 sylan ( ( 𝜑𝐴 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝐻 𝐴 ) = ( 𝐹 ‘ 0 ) ∧ ( 1 𝐻 𝐴 ) = ( 𝐹 ‘ 1 ) ) )