htpyco2

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

	Ref	Expression
Hypotheses	htpyco2.f	$⊢ φ \to F \in (J Cn K)$
	htpyco2.g	$⊢ φ \to G \in (J Cn K)$
	htpyco2.p	$⊢ φ \to P \in (K Cn L)$
	htpyco2.h	$⊢ φ \to H \in (F (J Htpy K) G)$
Assertion	htpyco2	$⊢ φ \to P \circ H \in ((P \circ F) (J Htpy L) (P \circ G))$

Proof

Step	Hyp	Ref	Expression
1		htpyco2.f	$⊢ φ \to F \in (J Cn K)$
2		htpyco2.g	$⊢ φ \to G \in (J Cn K)$
3		htpyco2.p	$⊢ φ \to P \in (K Cn L)$
4		htpyco2.h	$⊢ φ \to H \in (F (J Htpy K) G)$
5		cntop1	$⊢ F \in (J Cn K) \to J \in Top$
6	1 5	syl	$⊢ φ \to J \in Top$
7		toptopon2	$⊢ J \in Top \leftrightarrow J \in TopOn (⋃ J)$
8	6 7	sylib	$⊢ φ \to J \in TopOn (⋃ J)$
9		cnco	$⊢ (F \in (J Cn K) \land P \in (K Cn L)) \to P \circ F \in (J Cn L)$
10	1 3 9	syl2anc	$⊢ φ \to P \circ F \in (J Cn L)$
11		cnco	$⊢ (G \in (J Cn K) \land P \in (K Cn L)) \to P \circ G \in (J Cn L)$
12	2 3 11	syl2anc	$⊢ φ \to P \circ G \in (J Cn L)$
13	8 1 2	htpycn	$⊢ φ \to F (J Htpy K) G \subseteq (J \times_{t} II) Cn K$
14	13 4	sseldd	$⊢ φ \to H \in ((J \times_{t} II) Cn K)$
15		cnco	$⊢ (H \in ((J \times_{t} II) Cn K) \land P \in (K Cn L)) \to P \circ H \in ((J \times_{t} II) Cn L)$
16	14 3 15	syl2anc	$⊢ φ \to P \circ H \in ((J \times_{t} II) Cn L)$
17	8 1 2 4	htpyi	$⊢ (φ \land s \in ⋃ J) \to (s H 0 = F (s) \land s H 1 = G (s))$
18	17	simpld	$⊢ (φ \land s \in ⋃ J) \to s H 0 = F (s)$
19	18	fveq2d	$⊢ (φ \land s \in ⋃ J) \to P (s H 0) = P (F (s))$
20		iitopon	$⊢ II \in TopOn ([0, 1])$
21		txtopon	$⊢ (J \in TopOn (⋃ J) \land II \in TopOn ([0, 1])) \to J \times_{t} II \in TopOn (⋃ J \times [0, 1])$
22	8 20 21	sylancl	$⊢ φ \to J \times_{t} II \in TopOn (⋃ J \times [0, 1])$
23		cntop2	$⊢ F \in (J Cn K) \to K \in Top$
24	1 23	syl	$⊢ φ \to K \in Top$
25		toptopon2	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
26	24 25	sylib	$⊢ φ \to K \in TopOn (⋃ K)$
27		cnf2	$⊢ (J \times_{t} II \in TopOn (⋃ J \times [0, 1]) \land K \in TopOn (⋃ K) \land H \in ((J \times_{t} II) Cn K)) \to H : ⋃ J \times [0, 1] ⟶ ⋃ K$
28	22 26 14 27	syl3anc	$⊢ φ \to H : ⋃ J \times [0, 1] ⟶ ⋃ K$
29		simpr	$⊢ (φ \land s \in ⋃ J) \to s \in ⋃ J$
30		0elunit	$⊢ 0 \in [0, 1]$
31		opelxpi	$⊢ (s \in ⋃ J \land 0 \in [0, 1]) \to ⟨s, 0⟩ \in (⋃ J \times [0, 1])$
32	29 30 31	sylancl	$⊢ (φ \land s \in ⋃ J) \to ⟨s, 0⟩ \in (⋃ J \times [0, 1])$
33		fvco3	$⊢ (H : ⋃ J \times [0, 1] ⟶ ⋃ K \land ⟨s, 0⟩ \in (⋃ J \times [0, 1])) \to (P \circ H) (⟨s, 0⟩) = P (H (⟨s, 0⟩))$
34	28 32 33	syl2an2r	$⊢ (φ \land s \in ⋃ J) \to (P \circ H) (⟨s, 0⟩) = P (H (⟨s, 0⟩))$
35		df-ov	$⊢ s (P \circ H) 0 = (P \circ H) (⟨s, 0⟩)$
36		df-ov	$⊢ s H 0 = H (⟨s, 0⟩)$
37	36	fveq2i	$⊢ P (s H 0) = P (H (⟨s, 0⟩))$
38	34 35 37	3eqtr4g	$⊢ (φ \land s \in ⋃ J) \to s (P \circ H) 0 = P (s H 0)$
39		eqid	$⊢ ⋃ J = ⋃ J$
40		eqid	$⊢ ⋃ K = ⋃ K$
41	39 40	cnf	$⊢ F \in (J Cn K) \to F : ⋃ J ⟶ ⋃ K$
42	1 41	syl	$⊢ φ \to F : ⋃ J ⟶ ⋃ K$
43		fvco3	$⊢ (F : ⋃ J ⟶ ⋃ K \land s \in ⋃ J) \to (P \circ F) (s) = P (F (s))$
44	42 43	sylan	$⊢ (φ \land s \in ⋃ J) \to (P \circ F) (s) = P (F (s))$
45	19 38 44	3eqtr4d	$⊢ (φ \land s \in ⋃ J) \to s (P \circ H) 0 = (P \circ F) (s)$
46	17	simprd	$⊢ (φ \land s \in ⋃ J) \to s H 1 = G (s)$
47	46	fveq2d	$⊢ (φ \land s \in ⋃ J) \to P (s H 1) = P (G (s))$
48		1elunit	$⊢ 1 \in [0, 1]$
49		opelxpi	$⊢ (s \in ⋃ J \land 1 \in [0, 1]) \to ⟨s, 1⟩ \in (⋃ J \times [0, 1])$
50	29 48 49	sylancl	$⊢ (φ \land s \in ⋃ J) \to ⟨s, 1⟩ \in (⋃ J \times [0, 1])$
51		fvco3	$⊢ (H : ⋃ J \times [0, 1] ⟶ ⋃ K \land ⟨s, 1⟩ \in (⋃ J \times [0, 1])) \to (P \circ H) (⟨s, 1⟩) = P (H (⟨s, 1⟩))$
52	28 50 51	syl2an2r	$⊢ (φ \land s \in ⋃ J) \to (P \circ H) (⟨s, 1⟩) = P (H (⟨s, 1⟩))$
53		df-ov	$⊢ s (P \circ H) 1 = (P \circ H) (⟨s, 1⟩)$
54		df-ov	$⊢ s H 1 = H (⟨s, 1⟩)$
55	54	fveq2i	$⊢ P (s H 1) = P (H (⟨s, 1⟩))$
56	52 53 55	3eqtr4g	$⊢ (φ \land s \in ⋃ J) \to s (P \circ H) 1 = P (s H 1)$
57	39 40	cnf	$⊢ G \in (J Cn K) \to G : ⋃ J ⟶ ⋃ K$
58	2 57	syl	$⊢ φ \to G : ⋃ J ⟶ ⋃ K$
59		fvco3	$⊢ (G : ⋃ J ⟶ ⋃ K \land s \in ⋃ J) \to (P \circ G) (s) = P (G (s))$
60	58 59	sylan	$⊢ (φ \land s \in ⋃ J) \to (P \circ G) (s) = P (G (s))$
61	47 56 60	3eqtr4d	$⊢ (φ \land s \in ⋃ J) \to s (P \circ H) 1 = (P \circ G) (s)$
62	8 10 12 16 45 61	ishtpyd	$⊢ φ \to P \circ H \in ((P \circ F) (J Htpy L) (P \circ G))$

Metamath Proof Explorer

Theorem htpyco2

Proof