Metamath Proof Explorer

Theorem cvmlift

Description: One of the important properties of covering maps is that any path G in the base space "lifts" to a path f in the covering space such that F o. f = G , and given a starting point P in the covering space this lift is unique. The proof is contained in cvmliftlem1 thru cvmliftlem15 . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypothesis cvmlift.1 ⊢ B = ⋃ C
Assertion cvmlift ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → ∃! f ∈ II Cn C F ∘ f = G ∧ f ⁡ 0 = P

Proof

Step Hyp Ref Expression
1 cvmlift.1 ⊢ B = ⋃ C
2 eqid ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k
3 2 cvmscbv ⊢ k ∈ J ⟼ s ∈ 𝒫 C ∖ ∅ | ⋃ s = F -1 k ∧ ∀ u ∈ s ∀ v ∈ s ∖ u u ∩ v = ∅ ∧ F ↾ u ∈ C ↾ 𝑡 u Homeo J ↾ 𝑡 k = a ∈ J ⟼ b ∈ 𝒫 C ∖ ∅ | ⋃ b = F -1 a ∧ ∀ c ∈ b ∀ d ∈ b ∖ c c ∩ d = ∅ ∧ F ↾ c ∈ C ↾ 𝑡 c Homeo J ↾ 𝑡 a
4 eqid ⊢ ⋃ J = ⋃ J
5 simpll ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → F ∈ C CovMap J
6 simplr ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → G ∈ II Cn J
7 simprl ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → P ∈ B
8 simprr ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → F ⁡ P = G ⁡ 0
9 3 1 4 5 6 7 8 cvmliftlem15 ⊢ F ∈ C CovMap J ∧ G ∈ II Cn J ∧ P ∈ B ∧ F ⁡ P = G ⁡ 0 → ∃! f ∈ II Cn C F ∘ f = G ∧ f ⁡ 0 = P