# Metamath Proof Explorer

## Theorem phtpcco2

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

Ref Expression
Hypotheses phtpcco2.f $⊢ φ → F ≃ ph ⁡ J G$
phtpcco2.p $⊢ φ → P ∈ J Cn K$
Assertion phtpcco2 $⊢ φ → P ∘ F ≃ ph ⁡ K P ∘ G$

### Proof

Step Hyp Ref Expression
1 phtpcco2.f $⊢ φ → F ≃ ph ⁡ J G$
2 phtpcco2.p $⊢ φ → P ∈ J Cn K$
3 isphtpc $⊢ F ≃ ph ⁡ J G ↔ F ∈ II Cn J ∧ G ∈ II Cn J ∧ F PHtpy ⁡ J G ≠ ∅$
4 1 3 sylib $⊢ φ → F ∈ II Cn J ∧ G ∈ II Cn J ∧ F PHtpy ⁡ J G ≠ ∅$
5 4 simp1d $⊢ φ → F ∈ II Cn J$
6 cnco $⊢ F ∈ II Cn J ∧ P ∈ J Cn K → P ∘ F ∈ II Cn K$
7 5 2 6 syl2anc $⊢ φ → P ∘ F ∈ II Cn K$
8 4 simp2d $⊢ φ → G ∈ II Cn J$
9 cnco $⊢ G ∈ II Cn J ∧ P ∈ J Cn K → P ∘ G ∈ II Cn K$
10 8 2 9 syl2anc $⊢ φ → P ∘ G ∈ II Cn K$
11 4 simp3d $⊢ φ → F PHtpy ⁡ J G ≠ ∅$
12 n0 $⊢ F PHtpy ⁡ J G ≠ ∅ ↔ ∃ f f ∈ F PHtpy ⁡ J G$
13 11 12 sylib $⊢ φ → ∃ f f ∈ F PHtpy ⁡ J G$
14 5 adantr $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → F ∈ II Cn J$
15 8 adantr $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → G ∈ II Cn J$
16 2 adantr $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → P ∈ J Cn K$
17 simpr $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → f ∈ F PHtpy ⁡ J G$
18 14 15 16 17 phtpyco2 $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → P ∘ f ∈ P ∘ F PHtpy ⁡ K P ∘ G$
19 18 ne0d $⊢ φ ∧ f ∈ F PHtpy ⁡ J G → P ∘ F PHtpy ⁡ K P ∘ G ≠ ∅$
20 13 19 exlimddv $⊢ φ → P ∘ F PHtpy ⁡ K P ∘ G ≠ ∅$
21 isphtpc $⊢ P ∘ F ≃ ph ⁡ K P ∘ G ↔ P ∘ F ∈ II Cn K ∧ P ∘ G ∈ II Cn K ∧ P ∘ F PHtpy ⁡ K P ∘ G ≠ ∅$
22 7 10 20 21 syl3anbrc $⊢ φ → P ∘ F ≃ ph ⁡ K P ∘ G$