Metamath Proof Explorer

Theorem cvmlift2

Description: A two-dimensional version of cvmlift . There is a unique lift of functions on the unit square II tX II which commutes with the covering map. (Contributed by Mario Carneiro, 1-Jun-2015)

Ref Expression
Hypotheses cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
Assertion cvmlift2 ( 𝜑 → ∃! 𝑓 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 0 𝑓 0 ) = 𝑃 ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ 𝐵 = ∪ 𝐶
2 cvmlift2.f ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐶 CovMap 𝐽 ) )
3 cvmlift2.g ⊢ ( 𝜑 → 𝐺 ∈ ( ( II ×t II ) Cn 𝐽 ) )
4 cvmlift2.p ⊢ ( 𝜑 → 𝑃 ∈ 𝐵 )
5 cvmlift2.i ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑃 ) = ( 0 𝐺 0 ) )
6 coeq2 ⊢ ( ℎ = 𝑔 → ( 𝐹 ∘ ℎ ) = ( 𝐹 ∘ 𝑔 ) )
7 oveq1 ⊢ ( 𝑤 = 𝑧 → ( 𝑤 𝐺 0 ) = ( 𝑧 𝐺 0 ) )
8 7 cbvmptv ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) )
9 8 a1i ⊢ ( ℎ = 𝑔 → ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) )
10 6 9 eqeq12d ⊢ ( ℎ = 𝑔 → ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ) )
11 fveq1 ⊢ ( ℎ = 𝑔 → ( ℎ ‘ 0 ) = ( 𝑔 ‘ 0 ) )
12 11 eqeq1d ⊢ ( ℎ = 𝑔 → ( ( ℎ ‘ 0 ) = 𝑃 ↔ ( 𝑔 ‘ 0 ) = 𝑃 ) )
13 10 12 anbi12d ⊢ ( ℎ = 𝑔 → ( ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) ) )
14 13 cbvriotavw ⊢ ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑧 𝐺 0 ) ) ∧ ( 𝑔 ‘ 0 ) = 𝑃 ) )
15 coeq2 ⊢ ( 𝑘 = 𝑔 → ( 𝐹 ∘ 𝑘 ) = ( 𝐹 ∘ 𝑔 ) )
16 oveq2 ⊢ ( 𝑤 = 𝑧 → ( 𝑢 𝐺 𝑤 ) = ( 𝑢 𝐺 𝑧 ) )
17 16 cbvmptv ⊢ ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) )
18 17 a1i ⊢ ( 𝑘 = 𝑔 → ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) )
19 15 18 eqeq12d ⊢ ( 𝑘 = 𝑔 → ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ) )
20 fveq1 ⊢ ( 𝑘 = 𝑔 → ( 𝑘 ‘ 0 ) = ( 𝑔 ‘ 0 ) )
21 20 eqeq1d ⊢ ( 𝑘 = 𝑔 → ( ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ↔ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) )
22 19 21 anbi12d ⊢ ( 𝑘 = 𝑔 → ( ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ∧ ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) )
23 22 cbvriotavw ⊢ ( ℩ 𝑘 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ∧ ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) )
24 oveq1 ⊢ ( 𝑢 = 𝑥 → ( 𝑢 𝐺 𝑧 ) = ( 𝑥 𝐺 𝑧 ) )
25 24 mpteq2dv ⊢ ( 𝑢 = 𝑥 → ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) )
26 25 eqeq2d ⊢ ( 𝑢 = 𝑥 → ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ↔ ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ) )
27 fveq2 ⊢ ( 𝑢 = 𝑥 → ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) )
28 27 eqeq2d ⊢ ( 𝑢 = 𝑥 → ( ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ↔ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) )
29 26 28 anbi12d ⊢ ( 𝑢 = 𝑥 → ( ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ↔ ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) )
30 29 riotabidv ⊢ ( 𝑢 = 𝑥 → ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) )
31 23 30 syl5eq ⊢ ( 𝑢 = 𝑥 → ( ℩ 𝑘 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ∧ ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) = ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) )
32 31 fveq1d ⊢ ( 𝑢 = 𝑥 → ( ( ℩ 𝑘 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ∧ ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) ‘ 𝑣 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) ‘ 𝑣 ) )
33 fveq2 ⊢ ( 𝑣 = 𝑦 → ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) ‘ 𝑣 ) = ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
34 32 33 cbvmpov ⊢ ( 𝑢 ∈ ( 0 [,] 1 ) , 𝑣 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑘 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑘 ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑢 𝐺 𝑤 ) ) ∧ ( 𝑘 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑢 ) ) ) ‘ 𝑣 ) ) = ( 𝑥 ∈ ( 0 [,] 1 ) , 𝑦 ∈ ( 0 [,] 1 ) ↦ ( ( ℩ 𝑔 ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ 𝑔 ) = ( 𝑧 ∈ ( 0 [,] 1 ) ↦ ( 𝑥 𝐺 𝑧 ) ) ∧ ( 𝑔 ‘ 0 ) = ( ( ℩ ℎ ∈ ( II Cn 𝐶 ) ( ( 𝐹 ∘ ℎ ) = ( 𝑤 ∈ ( 0 [,] 1 ) ↦ ( 𝑤 𝐺 0 ) ) ∧ ( ℎ ‘ 0 ) = 𝑃 ) ) ‘ 𝑥 ) ) ) ‘ 𝑦 ) )
35 1 2 3 4 5 14 34 cvmlift2lem13 ⊢ ( 𝜑 → ∃! 𝑓 ∈ ( ( II ×t II ) Cn 𝐶 ) ( ( 𝐹 ∘ 𝑓 ) = 𝐺 ∧ ( 0 𝑓 0 ) = 𝑃 ) )