# 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
`|- ( ph -> F e. ( II Cn J ) )`
isphtpy.3
`|- ( ph -> G e. ( II Cn J ) )`
phtpyi.1
`|- ( ph -> H e. ( F ( PHtpy ` J ) G ) )`
Assertion phtpyi
`|- ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) )`

### Proof

Step Hyp Ref Expression
1 isphtpy.2
` |-  ( ph -> F e. ( II Cn J ) )`
2 isphtpy.3
` |-  ( ph -> G e. ( II Cn J ) )`
3 phtpyi.1
` |-  ( ph -> H e. ( F ( PHtpy ` J ) G ) )`
4 1 2 isphtpy
` |-  ( ph -> ( H e. ( F ( PHtpy ` J ) G ) <-> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) ) )`
5 3 4 mpbid
` |-  ( ph -> ( H e. ( F ( II Htpy J ) G ) /\ A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) ) )`
6 5 simprd
` |-  ( ph -> A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) )`
7 oveq2
` |-  ( s = A -> ( 0 H s ) = ( 0 H A ) )`
8 7 eqeq1d
` |-  ( s = A -> ( ( 0 H s ) = ( F ` 0 ) <-> ( 0 H A ) = ( F ` 0 ) ) )`
9 oveq2
` |-  ( s = A -> ( 1 H s ) = ( 1 H A ) )`
10 9 eqeq1d
` |-  ( s = A -> ( ( 1 H s ) = ( F ` 1 ) <-> ( 1 H A ) = ( F ` 1 ) ) )`
11 8 10 anbi12d
` |-  ( s = A -> ( ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) <-> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) ) )`
12 11 rspccva
` |-  ( ( A. s e. ( 0 [,] 1 ) ( ( 0 H s ) = ( F ` 0 ) /\ ( 1 H s ) = ( F ` 1 ) ) /\ A e. ( 0 [,] 1 ) ) -> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) )`
13 6 12 sylan
` |-  ( ( ph /\ A e. ( 0 [,] 1 ) ) -> ( ( 0 H A ) = ( F ` 0 ) /\ ( 1 H A ) = ( F ` 1 ) ) )`