phtpyco2

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

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

Proof

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

Metamath Proof Explorer

Theorem phtpyco2

Proof