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 ⊢ B = ⋃ C
cvmlift2.f ⊢ φ → F ∈ C CovMap J
cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
cvmlift2.p ⊢ φ → P ∈ B
cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
Assertion cvmlift2 ⊢ φ → ∃! f ∈ II × t II Cn C F ∘ f = G ∧ 0 f 0 = P

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢ B = ⋃ C
2 cvmlift2.f ⊢ φ → F ∈ C CovMap J
3 cvmlift2.g ⊢ φ → G ∈ II × t II Cn J
4 cvmlift2.p ⊢ φ → P ∈ B
5 cvmlift2.i ⊢ φ → F ⁡ P = 0 G 0
6 coeq2 ⊢ h = g → F ∘ h = F ∘ g
7 oveq1 ⊢ w = z → w G 0 = z G 0
8 7 cbvmptv ⊢ w ∈ 0 1 ⟼ w G 0 = z ∈ 0 1 ⟼ z G 0
9 8 a1i ⊢ h = g → w ∈ 0 1 ⟼ w G 0 = z ∈ 0 1 ⟼ z G 0
10 6 9 eqeq12d ⊢ h = g → F ∘ h = w ∈ 0 1 ⟼ w G 0 ↔ F ∘ g = z ∈ 0 1 ⟼ z G 0
11 fveq1 ⊢ h = g → h ⁡ 0 = g ⁡ 0
12 11 eqeq1d ⊢ h = g → h ⁡ 0 = P ↔ g ⁡ 0 = P
13 10 12 anbi12d ⊢ h = g → F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ↔ F ∘ g = z ∈ 0 1 ⟼ z G 0 ∧ g ⁡ 0 = P
14 13 cbvriotavw ⊢ ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ z G 0 ∧ g ⁡ 0 = P
15 coeq2 ⊢ k = g → F ∘ k = F ∘ g
16 oveq2 ⊢ w = z → u G w = u G z
17 16 cbvmptv ⊢ w ∈ 0 1 ⟼ u G w = z ∈ 0 1 ⟼ u G z
18 17 a1i ⊢ k = g → w ∈ 0 1 ⟼ u G w = z ∈ 0 1 ⟼ u G z
19 15 18 eqeq12d ⊢ k = g → F ∘ k = w ∈ 0 1 ⟼ u G w ↔ F ∘ g = z ∈ 0 1 ⟼ u G z
20 fveq1 ⊢ k = g → k ⁡ 0 = g ⁡ 0
21 20 eqeq1d ⊢ k = g → k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ↔ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u
22 19 21 anbi12d ⊢ k = g → F ∘ k = w ∈ 0 1 ⟼ u G w ∧ k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ↔ F ∘ g = z ∈ 0 1 ⟼ u G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u
23 22 cbvriotavw ⊢ ι k ∈ II Cn C | F ∘ k = w ∈ 0 1 ⟼ u G w ∧ k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ u G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u
24 oveq1 ⊢ u = x → u G z = x G z
25 24 mpteq2dv ⊢ u = x → z ∈ 0 1 ⟼ u G z = z ∈ 0 1 ⟼ x G z
26 25 eqeq2d ⊢ u = x → F ∘ g = z ∈ 0 1 ⟼ u G z ↔ F ∘ g = z ∈ 0 1 ⟼ x G z
27 fveq2 ⊢ u = x → ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x
28 27 eqeq2d ⊢ u = x → g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ↔ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x
29 26 28 anbi12d ⊢ u = x → F ∘ g = z ∈ 0 1 ⟼ u G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ↔ F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x
30 29 riotabidv ⊢ u = x → ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ u G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x
31 23 30 syl5eq ⊢ u = x → ι k ∈ II Cn C | F ∘ k = w ∈ 0 1 ⟼ u G w ∧ k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x
32 31 fveq1d ⊢ u = x → ι k ∈ II Cn C | F ∘ k = w ∈ 0 1 ⟼ u G w ∧ k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ⁡ v = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x ⁡ v
33 fveq2 ⊢ v = y → ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x ⁡ v = ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x ⁡ y
34 32 33 cbvmpov ⊢ u ∈ 0 1 , v ∈ 0 1 ⟼ ι k ∈ II Cn C | F ∘ k = w ∈ 0 1 ⟼ u G w ∧ k ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ u ⁡ v = x ∈ 0 1 , y ∈ 0 1 ⟼ ι g ∈ II Cn C | F ∘ g = z ∈ 0 1 ⟼ x G z ∧ g ⁡ 0 = ι h ∈ II Cn C | F ∘ h = w ∈ 0 1 ⟼ w G 0 ∧ h ⁡ 0 = P ⁡ x ⁡ y
35 1 2 3 4 5 14 34 cvmlift2lem13 ⊢ φ → ∃! f ∈ II × t II Cn C F ∘ f = G ∧ 0 f 0 = P