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	⊢ 𝐵 = ∪ 𝐶
Assertion	cvmlift	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )

Proof

Step	Hyp	Ref	Expression
1		cvmlift.1	⊢ 𝐵 = ∪ 𝐶
2		eqid	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } )
3	2	cvmscbv	⊢ ( 𝑘 ∈ 𝐽 ↦ { 𝑠 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑠 = ( ◡ 𝐹 “ 𝑘 ) ∧ ∀ 𝑢 ∈ 𝑠 ( ∀ 𝑣 ∈ ( 𝑠 ∖ { 𝑢 } ) ( 𝑢 ∩ 𝑣 ) = ∅ ∧ ( 𝐹 ↾ 𝑢 ) ∈ ( ( 𝐶 ↾t 𝑢 ) Homeo ( 𝐽 ↾t 𝑘 ) ) ) ) } ) = ( 𝑎 ∈ 𝐽 ↦ { 𝑏 ∈ ( 𝒫 𝐶 ∖ { ∅ } ) ∣ ( ∪ 𝑏 = ( ◡ 𝐹 “ 𝑎 ) ∧ ∀ 𝑐 ∈ 𝑏 ( ∀ 𝑑 ∈ ( 𝑏 ∖ { 𝑐 } ) ( 𝑐 ∩ 𝑑 ) = ∅ ∧ ( 𝐹 ↾ 𝑐 ) ∈ ( ( 𝐶 ↾t 𝑐 ) Homeo ( 𝐽 ↾t 𝑎 ) ) ) ) } )
4		eqid	⊢ ∪ 𝐽 = ∪ 𝐽
5		simpll	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
6		simplr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → 𝐺 ∈ ( II Cn 𝐽 ) )
7		simprl	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → 𝑃 ∈ 𝐵 )
8		simprr	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) )
9	3 1 4 5 6 7 8	cvmliftlem15	⊢ ( ( ( 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) ∧ 𝐺 ∈ ( II Cn 𝐽 ) ) ∧ ( 𝑃 ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 0 ) ) ) → ∃! 𝑓 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 0 ) = 𝑃 ) )