htpyco1

Description: Compose a homotopy with a continuous map. (Contributed by Mario Carneiro, 10-Mar-2015)

	Ref	Expression
Hypotheses	htpyco1.n	\|- N = ( x e. X , y e. ( 0 [,] 1 ) \|-> ( ( P ` x ) H y ) )
	htpyco1.j	\|- ( ph -> J e. ( TopOn ` X ) )
	htpyco1.p	\|- ( ph -> P e. ( J Cn K ) )
	htpyco1.f	\|- ( ph -> F e. ( K Cn L ) )
	htpyco1.g	\|- ( ph -> G e. ( K Cn L ) )
	htpyco1.h	\|- ( ph -> H e. ( F ( K Htpy L ) G ) )
Assertion	htpyco1	\|- ( ph -> N e. ( ( F o. P ) ( J Htpy L ) ( G o. P ) ) )

Proof

Step	Hyp	Ref	Expression
1		htpyco1.n	\|- N = ( x e. X , y e. ( 0 [,] 1 ) \|-> ( ( P ` x ) H y ) )
2		htpyco1.j	\|- ( ph -> J e. ( TopOn ` X ) )
3		htpyco1.p	\|- ( ph -> P e. ( J Cn K ) )
4		htpyco1.f	\|- ( ph -> F e. ( K Cn L ) )
5		htpyco1.g	\|- ( ph -> G e. ( K Cn L ) )
6		htpyco1.h	\|- ( ph -> H e. ( F ( K Htpy L ) G ) )
7		cnco	\|- ( ( P e. ( J Cn K ) /\ F e. ( K Cn L ) ) -> ( F o. P ) e. ( J Cn L ) )
8	3 4 7	syl2anc	\|- ( ph -> ( F o. P ) e. ( J Cn L ) )
9		cnco	\|- ( ( P e. ( J Cn K ) /\ G e. ( K Cn L ) ) -> ( G o. P ) e. ( J Cn L ) )
10	3 5 9	syl2anc	\|- ( ph -> ( G o. P ) e. ( J Cn L ) )
11		iitopon	\|- II e. ( TopOn ` ( 0 [,] 1 ) )
12	11	a1i	\|- ( ph -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
13	2 12	cnmpt1st	\|- ( ph -> ( x e. X , y e. ( 0 [,] 1 ) \|-> x ) e. ( ( J tX II ) Cn J ) )
14	2 12 13 3	cnmpt21f	\|- ( ph -> ( x e. X , y e. ( 0 [,] 1 ) \|-> ( P ` x ) ) e. ( ( J tX II ) Cn K ) )
15	2 12	cnmpt2nd	\|- ( ph -> ( x e. X , y e. ( 0 [,] 1 ) \|-> y ) e. ( ( J tX II ) Cn II ) )
16		cntop2	\|- ( P e. ( J Cn K ) -> K e. Top )
17	3 16	syl	\|- ( ph -> K e. Top )
18		toptopon2	\|- ( K e. Top <-> K e. ( TopOn ` U. K ) )
19	17 18	sylib	\|- ( ph -> K e. ( TopOn ` U. K ) )
20	19 4 5	htpycn	\|- ( ph -> ( F ( K Htpy L ) G ) C_ ( ( K tX II ) Cn L ) )
21	20 6	sseldd	\|- ( ph -> H e. ( ( K tX II ) Cn L ) )
22	2 12 14 15 21	cnmpt22f	\|- ( ph -> ( x e. X , y e. ( 0 [,] 1 ) \|-> ( ( P ` x ) H y ) ) e. ( ( J tX II ) Cn L ) )
23	1 22	eqeltrid	\|- ( ph -> N e. ( ( J tX II ) Cn L ) )
24		cnf2	\|- ( ( J e. ( TopOn ` X ) /\ K e. ( TopOn ` U. K ) /\ P e. ( J Cn K ) ) -> P : X --> U. K )
25	2 19 3 24	syl3anc	\|- ( ph -> P : X --> U. K )
26	25	ffvelrnda	\|- ( ( ph /\ s e. X ) -> ( P ` s ) e. U. K )
27	19 4 5 6	htpyi	\|- ( ( ph /\ ( P ` s ) e. U. K ) -> ( ( ( P ` s ) H 0 ) = ( F ` ( P ` s ) ) /\ ( ( P ` s ) H 1 ) = ( G ` ( P ` s ) ) ) )
28	26 27	syldan	\|- ( ( ph /\ s e. X ) -> ( ( ( P ` s ) H 0 ) = ( F ` ( P ` s ) ) /\ ( ( P ` s ) H 1 ) = ( G ` ( P ` s ) ) ) )
29	28	simpld	\|- ( ( ph /\ s e. X ) -> ( ( P ` s ) H 0 ) = ( F ` ( P ` s ) ) )
30		simpr	\|- ( ( ph /\ s e. X ) -> s e. X )
31		0elunit	\|- 0 e. ( 0 [,] 1 )
32		fveq2	\|- ( x = s -> ( P ` x ) = ( P ` s ) )
33		id	\|- ( y = 0 -> y = 0 )
34	32 33	oveqan12d	\|- ( ( x = s /\ y = 0 ) -> ( ( P ` x ) H y ) = ( ( P ` s ) H 0 ) )
35		ovex	\|- ( ( P ` s ) H 0 ) e. _V
36	34 1 35	ovmpoa	\|- ( ( s e. X /\ 0 e. ( 0 [,] 1 ) ) -> ( s N 0 ) = ( ( P ` s ) H 0 ) )
37	30 31 36	sylancl	\|- ( ( ph /\ s e. X ) -> ( s N 0 ) = ( ( P ` s ) H 0 ) )
38		fvco3	\|- ( ( P : X --> U. K /\ s e. X ) -> ( ( F o. P ) ` s ) = ( F ` ( P ` s ) ) )
39	25 38	sylan	\|- ( ( ph /\ s e. X ) -> ( ( F o. P ) ` s ) = ( F ` ( P ` s ) ) )
40	29 37 39	3eqtr4d	\|- ( ( ph /\ s e. X ) -> ( s N 0 ) = ( ( F o. P ) ` s ) )
41	28	simprd	\|- ( ( ph /\ s e. X ) -> ( ( P ` s ) H 1 ) = ( G ` ( P ` s ) ) )
42		1elunit	\|- 1 e. ( 0 [,] 1 )
43		id	\|- ( y = 1 -> y = 1 )
44	32 43	oveqan12d	\|- ( ( x = s /\ y = 1 ) -> ( ( P ` x ) H y ) = ( ( P ` s ) H 1 ) )
45		ovex	\|- ( ( P ` s ) H 1 ) e. _V
46	44 1 45	ovmpoa	\|- ( ( s e. X /\ 1 e. ( 0 [,] 1 ) ) -> ( s N 1 ) = ( ( P ` s ) H 1 ) )
47	30 42 46	sylancl	\|- ( ( ph /\ s e. X ) -> ( s N 1 ) = ( ( P ` s ) H 1 ) )
48		fvco3	\|- ( ( P : X --> U. K /\ s e. X ) -> ( ( G o. P ) ` s ) = ( G ` ( P ` s ) ) )
49	25 48	sylan	\|- ( ( ph /\ s e. X ) -> ( ( G o. P ) ` s ) = ( G ` ( P ` s ) ) )
50	41 47 49	3eqtr4d	\|- ( ( ph /\ s e. X ) -> ( s N 1 ) = ( ( G o. P ) ` s ) )
51	2 8 10 23 40 50	ishtpyd	\|- ( ph -> N e. ( ( F o. P ) ( J Htpy L ) ( G o. P ) ) )

Metamath Proof Explorer

Theorem htpyco1

Proof