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