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∈CCovMapJ
cvmlift2.g ⊢φ→G∈II×tIICnJ
cvmlift2.p ⊢φ→P∈B
cvmlift2.i ⊢φ→F⁡P=0G0
Assertion cvmlift2 ⊢φ→∃!f∈II×tIICnCF∘f=G∧0f0=P

Proof

Step Hyp Ref Expression
1 cvmlift2.b ⊢B=⋃C
2 cvmlift2.f ⊢φ→F∈CCovMapJ
3 cvmlift2.g ⊢φ→G∈II×tIICnJ
4 cvmlift2.p ⊢φ→P∈B
5 cvmlift2.i ⊢φ→F⁡P=0G0
6 coeq2 ⊢h=g→F∘h=F∘g
7 oveq1 ⊢w=z→wG0=zG0
8 7 cbvmptv ⊢w∈01⟼wG0=z∈01⟼zG0
9 8 a1i ⊢h=g→w∈01⟼wG0=z∈01⟼zG0
10 6 9 eqeq12d ⊢h=g→F∘h=w∈01⟼wG0↔F∘g=z∈01⟼zG0
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∈01⟼wG0∧h⁡0=P↔F∘g=z∈01⟼zG0∧g⁡0=P
14 13 cbvriotavw ⊢ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P=ιg∈IICnC|F∘g=z∈01⟼zG0∧g⁡0=P
15 coeq2 ⊢k=g→F∘k=F∘g
16 oveq2 ⊢w=z→uGw=uGz
17 16 cbvmptv ⊢w∈01⟼uGw=z∈01⟼uGz
18 17 a1i ⊢k=g→w∈01⟼uGw=z∈01⟼uGz
19 15 18 eqeq12d ⊢k=g→F∘k=w∈01⟼uGw↔F∘g=z∈01⟼uGz
20 fveq1 ⊢k=g→k⁡0=g⁡0
21 20 eqeq1d ⊢k=g→k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u↔g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u
22 19 21 anbi12d ⊢k=g→F∘k=w∈01⟼uGw∧k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u↔F∘g=z∈01⟼uGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u
23 22 cbvriotavw ⊢ιk∈IICnC|F∘k=w∈01⟼uGw∧k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u=ιg∈IICnC|F∘g=z∈01⟼uGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u
24 oveq1 ⊢u=x→uGz=xGz
25 24 mpteq2dv ⊢u=x→z∈01⟼uGz=z∈01⟼xGz
26 25 eqeq2d ⊢u=x→F∘g=z∈01⟼uGz↔F∘g=z∈01⟼xGz
27 fveq2 ⊢u=x→ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x
28 27 eqeq2d ⊢u=x→g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u↔g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x
29 26 28 anbi12d ⊢u=x→F∘g=z∈01⟼uGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u↔F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x
30 29 riotabidv ⊢u=x→ιg∈IICnC|F∘g=z∈01⟼uGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u=ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x
31 23 30 eqtrid ⊢u=x→ιk∈IICnC|F∘k=w∈01⟼uGw∧k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u=ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x
32 31 fveq1d ⊢u=x→ιk∈IICnC|F∘k=w∈01⟼uGw∧k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u⁡v=ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x⁡v
33 fveq2 ⊢v=y→ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x⁡v=ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x⁡y
34 32 33 cbvmpov ⊢u∈01,v∈01⟼ιk∈IICnC|F∘k=w∈01⟼uGw∧k⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡u⁡v=x∈01,y∈01⟼ιg∈IICnC|F∘g=z∈01⟼xGz∧g⁡0=ιh∈IICnC|F∘h=w∈01⟼wG0∧h⁡0=P⁡x⁡y
35 1 2 3 4 5 14 34 cvmlift2lem13 ⊢φ→∃!f∈II×tIICnCF∘f=G∧0f0=P