Definition df-phtpy

Description: Define the class of path homotopies between two paths F , G : II --> X ; these are homotopies (in the sense of df-htpy ) which also preserve both endpoints of the paths throughout the homotopy. Definition of Hatcher p. 25. (Contributed by Jeff Madsen, 2-Sep-2009)

	Ref	Expression
Assertion	df-phtpy	|- PHtpy = ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cphtpy	|- PHtpy
1		vx	|- x
2		ctop	|- Top
3		vf	|- f
4		cii	|- II
5		ccn	|- Cn
6	1	cv	|- x
7	4 6 5	co	|- ( II Cn x )
8		vg	|- g
9		vh	|- h
10	3	cv	|- f
11		chtpy	|- Htpy
12	4 6 11	co	|- ( II Htpy x )
13	8	cv	|- g
14	10 13 12	co	|- ( f ( II Htpy x ) g )
15		vs	|- s
16		cc0	|- 0
17		cicc	|- [,]
18		c1	|- 1
19	16 18 17	co	|- ( 0 [,] 1 )
20	9	cv	|- h
21	15	cv	|- s
22	16 21 20	co	|- ( 0 h s )
23	16 10	cfv	|- ( f ` 0 )
24	22 23	wceq	|- ( 0 h s ) = ( f ` 0 )
25	18 21 20	co	|- ( 1 h s )
26	18 10	cfv	|- ( f ` 1 )
27	25 26	wceq	|- ( 1 h s ) = ( f ` 1 )
28	24 27	wa	|- ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) )
29	28 15 19	wral	|- A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) )
30	29 9 14	crab	|- { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) }
31	3 8 7 7 30	cmpo	|- ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } )
32	1 2 31	cmpt	|- ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )
33	0 32	wceq	|- PHtpy = ( x e. Top |-> ( f e. ( II Cn x ) , g e. ( II Cn x ) |-> { h e. ( f ( II Htpy x ) g ) | A. s e. ( 0 [,] 1 ) ( ( 0 h s ) = ( f ` 0 ) /\ ( 1 h s ) = ( f ` 1 ) ) } ) )