htpyco1

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

	Ref	Expression
Hypotheses	htpyco1.n	$⊢ N = (x \in X, y \in [0, 1] ⟼ P (x) H y)$
	htpyco1.j	$⊢ φ \to J \in TopOn (X)$
	htpyco1.p	$⊢ φ \to P \in (J Cn K)$
	htpyco1.f	$⊢ φ \to F \in (K Cn L)$
	htpyco1.g	$⊢ φ \to G \in (K Cn L)$
	htpyco1.h	$⊢ φ \to H \in (F (K Htpy L) G)$
Assertion	htpyco1	$⊢ φ \to N \in ((F \circ P) (J Htpy L) (G \circ P))$

Proof

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

Metamath Proof Explorer

Theorem htpyco1

Proof