Metamath Proof Explorer

Theorem cvmliftpht

Description: If G and H are path-homotopic, then their lifts M and N are also path-homotopic. (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmliftpht.b ⊢ B = ⋃ C
cvmliftpht.m ⊢ M = ι f ∈ II Cn C | F ∘ f = G ∧ f ⁡ 0 = P
cvmliftpht.n ⊢ N = ι f ∈ II Cn C | F ∘ f = H ∧ f ⁡ 0 = P
cvmliftpht.f ⊢ φ → F ∈ C CovMap J
cvmliftpht.p ⊢ φ → P ∈ B
cvmliftpht.e ⊢ φ → F ⁡ P = G ⁡ 0
cvmliftpht.g ⊢ φ → G ≃ ph ⁡ J H
Assertion cvmliftpht ⊢ φ → M ≃ ph ⁡ C N

Proof

Step Hyp Ref Expression
1 cvmliftpht.b ⊢ B = ⋃ C
2 cvmliftpht.m ⊢ M = ι f ∈ II Cn C | F ∘ f = G ∧ f ⁡ 0 = P
3 cvmliftpht.n ⊢ N = ι f ∈ II Cn C | F ∘ f = H ∧ f ⁡ 0 = P
4 cvmliftpht.f ⊢ φ → F ∈ C CovMap J
5 cvmliftpht.p ⊢ φ → P ∈ B
6 cvmliftpht.e ⊢ φ → F ⁡ P = G ⁡ 0
7 cvmliftpht.g ⊢ φ → G ≃ ph ⁡ J H
8 isphtpc ⊢ G ≃ ph ⁡ J H ↔ G ∈ II Cn J ∧ H ∈ II Cn J ∧ G PHtpy ⁡ J H ≠ ∅
9 7 8 sylib ⊢ φ → G ∈ II Cn J ∧ H ∈ II Cn J ∧ G PHtpy ⁡ J H ≠ ∅
10 9 simp1d ⊢ φ → G ∈ II Cn J
11 1 2 4 10 5 6 cvmliftiota ⊢ φ → M ∈ II Cn C ∧ F ∘ M = G ∧ M ⁡ 0 = P
12 11 simp1d ⊢ φ → M ∈ II Cn C
13 9 simp2d ⊢ φ → H ∈ II Cn J
14 phtpc01 ⊢ G ≃ ph ⁡ J H → G ⁡ 0 = H ⁡ 0 ∧ G ⁡ 1 = H ⁡ 1
15 7 14 syl ⊢ φ → G ⁡ 0 = H ⁡ 0 ∧ G ⁡ 1 = H ⁡ 1
16 15 simpld ⊢ φ → G ⁡ 0 = H ⁡ 0
17 6 16 eqtrd ⊢ φ → F ⁡ P = H ⁡ 0
18 1 3 4 13 5 17 cvmliftiota ⊢ φ → N ∈ II Cn C ∧ F ∘ N = H ∧ N ⁡ 0 = P
19 18 simp1d ⊢ φ → N ∈ II Cn C
20 9 simp3d ⊢ φ → G PHtpy ⁡ J H ≠ ∅
21 n0 ⊢ G PHtpy ⁡ J H ≠ ∅ ↔ ∃ g g ∈ G PHtpy ⁡ J H
22 20 21 sylib ⊢ φ → ∃ g g ∈ G PHtpy ⁡ J H
23 4 adantr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → F ∈ C CovMap J
24 10 13 phtpycn ⊢ φ → G PHtpy ⁡ J H ⊆ II × t II Cn J
25 24 sselda ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → g ∈ II × t II Cn J
26 5 adantr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → P ∈ B
27 6 adantr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → F ⁡ P = G ⁡ 0
28 0elunit ⊢ 0 ∈ 0 1
29 10 adantr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → G ∈ II Cn J
30 13 adantr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → H ∈ II Cn J
31 simpr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → g ∈ G PHtpy ⁡ J H
32 29 30 31 phtpyi ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ 0 ∈ 0 1 → 0 g 0 = G ⁡ 0 ∧ 1 g 0 = G ⁡ 1
33 28 32 mpan2 ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → 0 g 0 = G ⁡ 0 ∧ 1 g 0 = G ⁡ 1
34 33 simpld ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → 0 g 0 = G ⁡ 0
35 27 34 eqtr4d ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → F ⁡ P = 0 g 0
36 1 23 25 26 35 cvmlift2 ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → ∃! h ∈ II × t II Cn C F ∘ h = g ∧ 0 h 0 = P
37 reurex ⊢ ∃! h ∈ II × t II Cn C F ∘ h = g ∧ 0 h 0 = P → ∃ h ∈ II × t II Cn C F ∘ h = g ∧ 0 h 0 = P
38 36 37 syl ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → ∃ h ∈ II × t II Cn C F ∘ h = g ∧ 0 h 0 = P
39 4 ad2antrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → F ∈ C CovMap J
40 5 ad2antrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → P ∈ B
41 6 ad2antrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → F ⁡ P = G ⁡ 0
42 10 ad2antrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → G ∈ II Cn J
43 13 ad2antrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → H ∈ II Cn J
44 simplr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → g ∈ G PHtpy ⁡ J H
45 simprl ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → h ∈ II × t II Cn C
46 simprrl ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → F ∘ h = g
47 simprrr ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → 0 h 0 = P
48 1 2 3 39 40 41 42 43 44 45 46 47 cvmliftphtlem ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → h ∈ M PHtpy ⁡ C N
49 48 ne0d ⊢ φ ∧ g ∈ G PHtpy ⁡ J H ∧ h ∈ II × t II Cn C ∧ F ∘ h = g ∧ 0 h 0 = P → M PHtpy ⁡ C N ≠ ∅
50 38 49 rexlimddv ⊢ φ ∧ g ∈ G PHtpy ⁡ J H → M PHtpy ⁡ C N ≠ ∅
51 22 50 exlimddv ⊢ φ → M PHtpy ⁡ C N ≠ ∅
52 isphtpc ⊢ M ≃ ph ⁡ C N ↔ M ∈ II Cn C ∧ N ∈ II Cn C ∧ M PHtpy ⁡ C N ≠ ∅
53 12 19 51 52 syl3anbrc ⊢ φ → M ≃ ph ⁡ C N