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 ⊢ 𝐵 = ∪ 𝐶
cvmliftpht.m ⊢ 𝑀 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmliftpht.n ⊢ 𝑁 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
cvmliftpht.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftpht.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftpht.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
cvmliftpht.g ⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐻 )
Assertion cvmliftpht ( 𝜑 → 𝑀 ( ≃ph ‘ 𝐶 ) 𝑁 )

Proof

Step Hyp Ref Expression
1 cvmliftpht.b ⊢ 𝐵 = ∪ 𝐶
2 cvmliftpht.m ⊢ 𝑀 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
3 cvmliftpht.n ⊢ 𝑁 = ( ℩ 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐻 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )
4 cvmliftpht.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
5 cvmliftpht.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
6 cvmliftpht.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
7 cvmliftpht.g ⊢ ( 𝜑 → 𝐺 ( ≃ph ‘ 𝐽 ) 𝐻 )
8 isphtpc ⊢ ( 𝐺 ( ≃ph ‘ 𝐽 ) 𝐻 ↔ ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
9 7 8 sylib ⊢ ( 𝜑 → ( 𝐺 ∈ ( II Cn 𝐽 ) ∧ 𝐻 ∈ ( II Cn 𝐽 ) ∧ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ) )
10 9 simp1d ⊢ ( 𝜑 → 𝐺 ∈ ( II Cn 𝐽 ) )
11 1 2 4 10 5 6 cvmliftiota ⊢ ( 𝜑 → ( 𝑀 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝑀 ) = 𝐺 ∧ ( 𝑀 ‘ 0 ) = 𝑃 ) )
12 11 simp1d ⊢ ( 𝜑 → 𝑀 ∈ ( II Cn 𝐶 ) )
13 9 simp2d ⊢ ( 𝜑 → 𝐻 ∈ ( II Cn 𝐽 ) )
14 phtpc01 ⊢ ( 𝐺 ( ≃ph ‘ 𝐽 ) 𝐻 → ( ( 𝐺 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
15 7 14 syl ⊢ ( 𝜑 → ( ( 𝐺 ‘ 0 ) = ( 𝐻 ‘ 0 ) ∧ ( 𝐺 ‘ 1 ) = ( 𝐻 ‘ 1 ) ) )
16 15 simpld ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 𝐻 ‘ 0 ) )
17 6 16 eqtrd ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐻 ‘ 0 ) )
18 1 3 4 13 5 17 cvmliftiota ⊢ ( 𝜑 → ( 𝑁 ∈ ( II Cn 𝐶 ) ∧ ( 𝐹 ∘ 𝑁 ) = 𝐻 ∧ ( 𝑁 ‘ 0 ) = 𝑃 ) )
19 18 simp1d ⊢ ( 𝜑 → 𝑁 ∈ ( II Cn 𝐶 ) )
20 9 simp3d ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ )
21 n0 ⊢ ( ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ≠ ∅ ↔ ∃ 𝑔 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
22 20 21 sylib ⊢ ( 𝜑 → ∃ 𝑔 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
23 4 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
24 10 13 phtpycn ⊢ ( 𝜑 → ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ⊆ ( ( II ×t II ) Cn 𝐽 ) )
25 24 sselda ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝑔 ∈ ( ( II ×t II ) Cn 𝐽 ) )
26 5 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝑃 ∈ 𝐵 )
27 6 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
28 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
29 10 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
30 13 adantr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝐻 ∈ ( II Cn 𝐽 ) )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
32 29 30 31 phtpyi ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( ( 0 𝑔 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝑔 0 ) = ( 𝐺 ‘ 1 ) ) )
33 28 32 mpan2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ( ( 0 𝑔 0 ) = ( 𝐺 ‘ 0 ) ∧ ( 1 𝑔 0 ) = ( 𝐺 ‘ 1 ) ) )
34 33 simpld ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ( 0 𝑔 0 ) = ( 𝐺 ‘ 0 ) )
35 27 34 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ( 𝐹 ‘ 𝑃 ) = ( 0 𝑔 0 ) )
36 1 23 25 26 35 cvmlift2 ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ∃! ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) )
37 reurex ⊢ ( ∃! ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) → ∃ ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) )
38 36 37 syl ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ∃ ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) )
39 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
40 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → 𝑃 ∈ 𝐵 )
41 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
42 10 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
43 13 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → 𝐻 ∈ ( II Cn 𝐽 ) )
44 simplr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) )
45 simprl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) )
46 simprrl ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ( 𝐹 ∘ ℎ ) = 𝑔 )
47 simprrr ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ( 0 ℎ 0 ) = 𝑃 )
48 1 2 3 39 40 41 42 43 44 45 46 47 cvmliftphtlem ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ℎ ∈ ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) )
49 48 ne0d ⊢ ( ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) ∧ ( ℎ ∈ ( ( II ×t II ) Cn 𝐶 ) ∧ ( ( 𝐹 ∘ ℎ ) = 𝑔 ∧ ( 0 ℎ 0 ) = 𝑃 ) ) ) → ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) ≠ ∅ )
50 38 49 rexlimddv ⊢ ( ( 𝜑 ∧ 𝑔 ∈ ( 𝐺 ( PHtpy ‘ 𝐽 ) 𝐻 ) ) → ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) ≠ ∅ )
51 22 50 exlimddv ⊢ ( 𝜑 → ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) ≠ ∅ )
52 isphtpc ⊢ ( 𝑀 ( ≃ph ‘ 𝐶 ) 𝑁 ↔ ( 𝑀 ∈ ( II Cn 𝐶 ) ∧ 𝑁 ∈ ( II Cn 𝐶 ) ∧ ( 𝑀 ( PHtpy ‘ 𝐶 ) 𝑁 ) ≠ ∅ ) )
53 12 19 51 52 syl3anbrc ⊢ ( 𝜑 → 𝑀 ( ≃ph ‘ 𝐶 ) 𝑁 )