# 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}=\bigcup {C}$
cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
Assertion cvmlift2 ${⊢}{\phi }\to \exists !{f}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{C}\right)\phantom{\rule{.4em}{0ex}}\left({F}\circ {f}={G}\wedge 0{f}0={P}\right)$

### Proof

Step Hyp Ref Expression
1 cvmlift2.b ${⊢}{B}=\bigcup {C}$
2 cvmlift2.f ${⊢}{\phi }\to {F}\in \left({C}\mathrm{CovMap}{J}\right)$
3 cvmlift2.g ${⊢}{\phi }\to {G}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{J}\right)$
4 cvmlift2.p ${⊢}{\phi }\to {P}\in {B}$
5 cvmlift2.i ${⊢}{\phi }\to {F}\left({P}\right)=0{G}0$
6 coeq2 ${⊢}{h}={g}\to {F}\circ {h}={F}\circ {g}$
7 oveq1 ${⊢}{w}={z}\to {w}{G}0={z}{G}0$
8 7 cbvmptv ${⊢}\left({w}\in \left[0,1\right]⟼{w}{G}0\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)$
9 8 a1i ${⊢}{h}={g}\to \left({w}\in \left[0,1\right]⟼{w}{G}0\right)=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)$
10 6 9 eqeq12d ${⊢}{h}={g}\to \left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)↔{F}\circ {g}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\right)$
11 fveq1 ${⊢}{h}={g}\to {h}\left(0\right)={g}\left(0\right)$
12 11 eqeq1d ${⊢}{h}={g}\to \left({h}\left(0\right)={P}↔{g}\left(0\right)={P}\right)$
13 10 12 anbi12d ${⊢}{h}={g}\to \left(\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)↔\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {g}\left(0\right)={P}\right)\right)$
14 13 cbvriotavw ${⊢}\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{z}{G}0\right)\wedge {g}\left(0\right)={P}\right)\right)$
15 coeq2 ${⊢}{k}={g}\to {F}\circ {k}={F}\circ {g}$
16 oveq2 ${⊢}{w}={z}\to {u}{G}{w}={u}{G}{z}$
17 16 cbvmptv ${⊢}\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)$
18 17 a1i ${⊢}{k}={g}\to \left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)$
19 15 18 eqeq12d ${⊢}{k}={g}\to \left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)↔{F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)\right)$
20 fveq1 ${⊢}{k}={g}\to {k}\left(0\right)={g}\left(0\right)$
21 20 eqeq1d ${⊢}{k}={g}\to \left({k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)↔{g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)$
22 19 21 anbi12d ${⊢}{k}={g}\to \left(\left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)\wedge {k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)↔\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)$
23 22 cbvriotavw ${⊢}\left(\iota {k}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)\wedge {k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)$
24 oveq1 ${⊢}{u}={x}\to {u}{G}{z}={x}{G}{z}$
25 24 mpteq2dv ${⊢}{u}={x}\to \left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)$
26 25 eqeq2d ${⊢}{u}={x}\to \left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)↔{F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\right)$
27 fveq2 ${⊢}{u}={x}\to \left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)$
28 27 eqeq2d ${⊢}{u}={x}\to \left({g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)↔{g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)$
29 26 28 anbi12d ${⊢}{u}={x}\to \left(\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)↔\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)$
30 29 riotabidv ${⊢}{u}={x}\to \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{u}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)$
31 23 30 syl5eq ${⊢}{u}={x}\to \left(\iota {k}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)\wedge {k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)$
32 31 fveq1d ${⊢}{u}={x}\to \left(\iota {k}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)\wedge {k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)\left({v}\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)\left({v}\right)$
33 fveq2 ${⊢}{v}={y}\to \left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)\left({v}\right)=\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)\left({y}\right)$
34 32 33 cbvmpov ${⊢}\left({u}\in \left[0,1\right],{v}\in \left[0,1\right]⟼\left(\iota {k}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {k}=\left({w}\in \left[0,1\right]⟼{u}{G}{w}\right)\wedge {k}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({u}\right)\right)\right)\left({v}\right)\right)=\left({x}\in \left[0,1\right],{y}\in \left[0,1\right]⟼\left(\iota {g}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {g}=\left({z}\in \left[0,1\right]⟼{x}{G}{z}\right)\wedge {g}\left(0\right)=\left(\iota {h}\in \left(\mathrm{II}\mathrm{Cn}{C}\right)|\left({F}\circ {h}=\left({w}\in \left[0,1\right]⟼{w}{G}0\right)\wedge {h}\left(0\right)={P}\right)\right)\left({x}\right)\right)\right)\left({y}\right)\right)$
35 1 2 3 4 5 14 34 cvmlift2lem13 ${⊢}{\phi }\to \exists !{f}\in \left(\left(\mathrm{II}{×}_{t}\mathrm{II}\right)\mathrm{Cn}{C}\right)\phantom{\rule{.4em}{0ex}}\left({F}\circ {f}={G}\wedge 0{f}0={P}\right)$