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 ) ) )