Metamath Proof Explorer

Theorem cvmliftmo

Description: A lift of a continuous function from a connected and locally connected space over a covering map is unique when it exists. (Contributed by Mario Carneiro, 10-Mar-2015) (Revised by NM, 17-Jun-2017)

Ref Expression
Hypotheses cvmliftmo.b ⊢ 𝐵 = ∪ 𝐶
cvmliftmo.y ⊢ 𝑌 = ∪ 𝐾
cvmliftmo.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmliftmo.k ⊢ ( 𝜑 → 𝐾 ∈ Conn )
cvmliftmo.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
cvmliftmo.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
cvmliftmo.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
cvmliftmo.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmliftmo.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
Assertion cvmliftmo ( 𝜑 → ∃* 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmliftmo.b ⊢ 𝐵 = ∪ 𝐶
2 cvmliftmo.y ⊢ 𝑌 = ∪ 𝐾
3 cvmliftmo.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
4 cvmliftmo.k ⊢ ( 𝜑 → 𝐾 ∈ Conn )
5 cvmliftmo.l ⊢ ( 𝜑 → 𝐾 ∈ 𝑛-Locally Conn )
6 cvmliftmo.o ⊢ ( 𝜑 → 𝑂 ∈ 𝑌 )
7 cvmliftmo.g ⊢ ( 𝜑 → 𝐺 ∈ ( 𝐾 Cn 𝐽 ) )
8 cvmliftmo.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
9 cvmliftmo.e ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 𝐺 ‘ 𝑂 ) )
10 3 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
11 4 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝐾 ∈ Conn )
12 5 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝐾 ∈ 𝑛-Locally Conn )
13 6 ad2antrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝑂 ∈ 𝑌 )
14 simplrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝑓 ∈ ( 𝐾 Cn 𝐶 ) )
15 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝑔 ∈ ( 𝐾 Cn 𝐶 ) )
16 simprll ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝐹 ∘ 𝑓 ) = 𝐺 )
17 simprrl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝐹 ∘ 𝑔 ) = 𝐺 )
18 16 17 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ 𝑔 ) )
19 simprlr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝑓 ‘ 𝑂 ) = 𝑃 )
20 simprrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝑔 ‘ 𝑂 ) = 𝑃 )
21 19 20 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → ( 𝑓 ‘ 𝑂 ) = ( 𝑔 ‘ 𝑂 ) )
22 1 2 10 11 12 13 14 15 18 21 cvmliftmoi ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) ∧ ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) ) → 𝑓 = 𝑔 )
23 22 ex ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∧ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ) ) → ( ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) → 𝑓 = 𝑔 ) )
24 23 ralrimivva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∀ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ( ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) → 𝑓 = 𝑔 ) )
25 coeq2 ⊢ ( 𝑓 = 𝑔 → ( 𝐹 ∘ 𝑓 ) = ( 𝐹 ∘ 𝑔 ) )
26 25 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ↔ ( 𝐹 ∘ 𝑔 ) = 𝐺 ) )
27 fveq1 ⊢ ( 𝑓 = 𝑔 → ( 𝑓 ‘ 𝑂 ) = ( 𝑔 ‘ 𝑂 ) )
28 27 eqeq1d ⊢ ( 𝑓 = 𝑔 → ( ( 𝑓 ‘ 𝑂 ) = 𝑃 ↔ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) )
29 26 28 anbi12d ⊢ ( 𝑓 = 𝑔 → ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) )
30 29 rmo4 ⊢ ( ∃* 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ↔ ∀ 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ∀ 𝑔 ∈ ( 𝐾 Cn 𝐶 ) ( ( ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) ∧ ( ( 𝐹 ∘ 𝑔 ) = 𝐺 ∧ ( 𝑔 ‘ 𝑂 ) = 𝑃 ) ) → 𝑓 = 𝑔 ) )
31 24 30 sylibr ⊢ ( 𝜑 → ∃* 𝑓 ∈ ( 𝐾 Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 𝑓 ‘ 𝑂 ) = 𝑃 ) )