phtpcco2

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

	Ref	Expression
Hypotheses	phtpcco2.f	$⊢ φ \to F ≃_{ph} (J) G$
	phtpcco2.p	$⊢ φ \to P \in (J Cn K)$
Assertion	phtpcco2	$⊢ φ \to (P \circ F) ≃_{ph} (K) (P \circ G)$

Proof

Step	Hyp	Ref	Expression
1		phtpcco2.f	$⊢ φ \to F ≃_{ph} (J) G$
2		phtpcco2.p	$⊢ φ \to P \in (J Cn K)$
3		isphtpc	$⊢ F ≃_{ph} (J) G \leftrightarrow (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$
4	1 3	sylib	$⊢ φ \to (F \in (II Cn J) \land G \in (II Cn J) \land F PHtpy (J) G \neq \emptyset)$
5	4	simp1d	$⊢ φ \to F \in (II Cn J)$
6		cnco	$⊢ (F \in (II Cn J) \land P \in (J Cn K)) \to P \circ F \in (II Cn K)$
7	5 2 6	syl2anc	$⊢ φ \to P \circ F \in (II Cn K)$
8	4	simp2d	$⊢ φ \to G \in (II Cn J)$
9		cnco	$⊢ (G \in (II Cn J) \land P \in (J Cn K)) \to P \circ G \in (II Cn K)$
10	8 2 9	syl2anc	$⊢ φ \to P \circ G \in (II Cn K)$
11	4	simp3d	$⊢ φ \to F PHtpy (J) G \neq \emptyset$
12		n0	$⊢ F PHtpy (J) G \neq \emptyset \leftrightarrow \exists f f \in (F PHtpy (J) G)$
13	11 12	sylib	$⊢ φ \to \exists f f \in (F PHtpy (J) G)$
14	5	adantr	$⊢ (φ \land f \in (F PHtpy (J) G)) \to F \in (II Cn J)$
15	8	adantr	$⊢ (φ \land f \in (F PHtpy (J) G)) \to G \in (II Cn J)$
16	2	adantr	$⊢ (φ \land f \in (F PHtpy (J) G)) \to P \in (J Cn K)$
17		simpr	$⊢ (φ \land f \in (F PHtpy (J) G)) \to f \in (F PHtpy (J) G)$
18	14 15 16 17	phtpyco2	$⊢ (φ \land f \in (F PHtpy (J) G)) \to P \circ f \in ((P \circ F) PHtpy (K) (P \circ G))$
19	18	ne0d	$⊢ (φ \land f \in (F PHtpy (J) G)) \to (P \circ F) PHtpy (K) (P \circ G) \neq \emptyset$
20	13 19	exlimddv	$⊢ φ \to (P \circ F) PHtpy (K) (P \circ G) \neq \emptyset$
21		isphtpc	$⊢ (P \circ F) ≃_{ph} (K) (P \circ G) \leftrightarrow (P \circ F \in (II Cn K) \land P \circ G \in (II Cn K) \land (P \circ F) PHtpy (K) (P \circ G) \neq \emptyset)$
22	7 10 20 21	syl3anbrc	$⊢ φ \to (P \circ F) ≃_{ph} (K) (P \circ G)$

Metamath Proof Explorer

Theorem phtpcco2

Proof