Metamath Proof Explorer

Theorem pcohtpy

Description: Homotopy invariance of path concatenation. (Contributed by Jeff Madsen, 15-Jun-2010) (Revised by Mario Carneiro, 24-Feb-2015)

Ref Expression
Hypotheses pcohtpy.4 ⊢ φ → F ⁡ 1 = G ⁡ 0
pcohtpy.5 ⊢ φ → F ≃ ph ⁡ J H
pcohtpy.6 ⊢ φ → G ≃ ph ⁡ J K
Assertion pcohtpy ⊢ φ → F * 𝑝 ⁡ J G ≃ ph ⁡ J H * 𝑝 ⁡ J K

Proof

Step Hyp Ref Expression
1 pcohtpy.4 ⊢ φ → F ⁡ 1 = G ⁡ 0
2 pcohtpy.5 ⊢ φ → F ≃ ph ⁡ J H
3 pcohtpy.6 ⊢ φ → G ≃ ph ⁡ J K
4 isphtpc ⊢ F ≃ ph ⁡ J H ↔ F ∈ II Cn J ∧ H ∈ II Cn J ∧ F PHtpy ⁡ J H ≠ ∅
5 2 4 sylib ⊢ φ → F ∈ II Cn J ∧ H ∈ II Cn J ∧ F PHtpy ⁡ J H ≠ ∅
6 5 simp1d ⊢ φ → F ∈ II Cn J
7 isphtpc ⊢ G ≃ ph ⁡ J K ↔ G ∈ II Cn J ∧ K ∈ II Cn J ∧ G PHtpy ⁡ J K ≠ ∅
8 3 7 sylib ⊢ φ → G ∈ II Cn J ∧ K ∈ II Cn J ∧ G PHtpy ⁡ J K ≠ ∅
9 8 simp1d ⊢ φ → G ∈ II Cn J
10 6 9 1 pcocn ⊢ φ → F * 𝑝 ⁡ J G ∈ II Cn J
11 5 simp2d ⊢ φ → H ∈ II Cn J
12 8 simp2d ⊢ φ → K ∈ II Cn J
13 phtpc01 ⊢ F ≃ ph ⁡ J H → F ⁡ 0 = H ⁡ 0 ∧ F ⁡ 1 = H ⁡ 1
14 2 13 syl ⊢ φ → F ⁡ 0 = H ⁡ 0 ∧ F ⁡ 1 = H ⁡ 1
15 14 simprd ⊢ φ → F ⁡ 1 = H ⁡ 1
16 phtpc01 ⊢ G ≃ ph ⁡ J K → G ⁡ 0 = K ⁡ 0 ∧ G ⁡ 1 = K ⁡ 1
17 3 16 syl ⊢ φ → G ⁡ 0 = K ⁡ 0 ∧ G ⁡ 1 = K ⁡ 1
18 17 simpld ⊢ φ → G ⁡ 0 = K ⁡ 0
19 1 15 18 3eqtr3d ⊢ φ → H ⁡ 1 = K ⁡ 0
20 11 12 19 pcocn ⊢ φ → H * 𝑝 ⁡ J K ∈ II Cn J
21 5 simp3d ⊢ φ → F PHtpy ⁡ J H ≠ ∅
22 n0 ⊢ F PHtpy ⁡ J H ≠ ∅ ↔ ∃ m m ∈ F PHtpy ⁡ J H
23 21 22 sylib ⊢ φ → ∃ m m ∈ F PHtpy ⁡ J H
24 8 simp3d ⊢ φ → G PHtpy ⁡ J K ≠ ∅
25 n0 ⊢ G PHtpy ⁡ J K ≠ ∅ ↔ ∃ n n ∈ G PHtpy ⁡ J K
26 24 25 sylib ⊢ φ → ∃ n n ∈ G PHtpy ⁡ J K
27 exdistrv ⊢ ∃ m ∃ n m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K ↔ ∃ m m ∈ F PHtpy ⁡ J H ∧ ∃ n n ∈ G PHtpy ⁡ J K
28 23 26 27 sylanbrc ⊢ φ → ∃ m ∃ n m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K
29 1 adantr ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → F ⁡ 1 = G ⁡ 0
30 2 adantr ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → F ≃ ph ⁡ J H
31 3 adantr ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → G ≃ ph ⁡ J K
32 eqid ⊢ x ∈ 0 1 , y ∈ 0 1 ⟼ if x ≤ 1 2 2 ⁢ x m y 2 ⁢ x − 1 n y = x ∈ 0 1 , y ∈ 0 1 ⟼ if x ≤ 1 2 2 ⁢ x m y 2 ⁢ x − 1 n y
33 simprl ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → m ∈ F PHtpy ⁡ J H
34 simprr ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → n ∈ G PHtpy ⁡ J K
35 29 30 31 32 33 34 pcohtpylem ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → x ∈ 0 1 , y ∈ 0 1 ⟼ if x ≤ 1 2 2 ⁢ x m y 2 ⁢ x − 1 n y ∈ F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K
36 35 ne0d ⊢ φ ∧ m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K ≠ ∅
37 36 ex ⊢ φ → m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K ≠ ∅
38 37 exlimdvv ⊢ φ → ∃ m ∃ n m ∈ F PHtpy ⁡ J H ∧ n ∈ G PHtpy ⁡ J K → F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K ≠ ∅
39 28 38 mpd ⊢ φ → F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K ≠ ∅
40 isphtpc ⊢ F * 𝑝 ⁡ J G ≃ ph ⁡ J H * 𝑝 ⁡ J K ↔ F * 𝑝 ⁡ J G ∈ II Cn J ∧ H * 𝑝 ⁡ J K ∈ II Cn J ∧ F * 𝑝 ⁡ J G PHtpy ⁡ J H * 𝑝 ⁡ J K ≠ ∅
41 10 20 39 40 syl3anbrc ⊢ φ → F * 𝑝 ⁡ J G ≃ ph ⁡ J H * 𝑝 ⁡ J K