Theorem htpyi

Description: A homotopy evaluated at its endpoints. (Contributed by Mario Carneiro, 22-Feb-2015)

	Ref	Expression
Hypotheses	ishtpy.1	|- ( ph -> J e. ( TopOn ` X ) )
	ishtpy.3	|- ( ph -> F e. ( J Cn K ) )
	ishtpy.4	|- ( ph -> G e. ( J Cn K ) )
	htpyi.1	|- ( ph -> H e. ( F ( J Htpy K ) G ) )
Assertion	htpyi	|- ( ( ph /\ A e. X ) -> ( ( A H 0 ) = ( F ` A ) /\ ( A H 1 ) = ( G ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		ishtpy.1	|- ( ph -> J e. ( TopOn ` X ) )
2		ishtpy.3	|- ( ph -> F e. ( J Cn K ) )
3		ishtpy.4	|- ( ph -> G e. ( J Cn K ) )
4		htpyi.1	|- ( ph -> H e. ( F ( J Htpy K ) G ) )
5	1 2 3	ishtpy	|- ( ph -> ( H e. ( F ( J Htpy K ) G ) <-> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) ) )
6	4 5	mpbid	|- ( ph -> ( H e. ( ( J tX II ) Cn K ) /\ A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) ) )
7	6	simprd	|- ( ph -> A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) )
8		oveq1	|- ( s = A -> ( s H 0 ) = ( A H 0 ) )
9		fveq2	|- ( s = A -> ( F ` s ) = ( F ` A ) )
10	8 9	eqeq12d	|- ( s = A -> ( ( s H 0 ) = ( F ` s ) <-> ( A H 0 ) = ( F ` A ) ) )
11		oveq1	|- ( s = A -> ( s H 1 ) = ( A H 1 ) )
12		fveq2	|- ( s = A -> ( G ` s ) = ( G ` A ) )
13	11 12	eqeq12d	|- ( s = A -> ( ( s H 1 ) = ( G ` s ) <-> ( A H 1 ) = ( G ` A ) ) )
14	10 13	anbi12d	|- ( s = A -> ( ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) <-> ( ( A H 0 ) = ( F ` A ) /\ ( A H 1 ) = ( G ` A ) ) ) )
15	14	rspccva	|- ( ( A. s e. X ( ( s H 0 ) = ( F ` s ) /\ ( s H 1 ) = ( G ` s ) ) /\ A e. X ) -> ( ( A H 0 ) = ( F ` A ) /\ ( A H 1 ) = ( G ` A ) ) )
16	7 15	sylan	|- ( ( ph /\ A e. X ) -> ( ( A H 0 ) = ( F ` A ) /\ ( A H 1 ) = ( G ` A ) ) )