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 = U. C
cvmlift2.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift2.g 
|- ( ph -> G e. ( ( II tX II ) Cn J ) )
cvmlift2.p 
|- ( ph -> P e. B )
cvmlift2.i 
|- ( ph -> ( F ` P ) = ( 0 G 0 ) )
Assertion cvmlift2 
|- ( ph -> E! f e. ( ( II tX II ) Cn C ) ( ( F o. f ) = G /\ ( 0 f 0 ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmlift2.b 
 |-  B = U. C
2 cvmlift2.f 
 |-  ( ph -> F e. ( C CovMap J ) )
3 cvmlift2.g 
 |-  ( ph -> G e. ( ( II tX II ) Cn J ) )
4 cvmlift2.p 
 |-  ( ph -> P e. B )
5 cvmlift2.i 
 |-  ( ph -> ( F ` P ) = ( 0 G 0 ) )
6 coeq2 
 |-  ( h = g -> ( F o. h ) = ( F o. g ) )
7 oveq1 
 |-  ( w = z -> ( w G 0 ) = ( z G 0 ) )
8 7 cbvmptv 
 |-  ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) )
9 8 a1i 
 |-  ( h = g -> ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) )
10 6 9 eqeq12d 
 |-  ( h = g -> ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) <-> ( F o. g ) = ( z e. ( 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 o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) <-> ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( g ` 0 ) = P ) ) )
14 13 cbvriotavw 
 |-  ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( z G 0 ) ) /\ ( g ` 0 ) = P ) )
15 coeq2 
 |-  ( k = g -> ( F o. k ) = ( F o. g ) )
16 oveq2 
 |-  ( w = z -> ( u G w ) = ( u G z ) )
17 16 cbvmptv 
 |-  ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) )
18 17 a1i 
 |-  ( k = g -> ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) )
19 15 18 eqeq12d 
 |-  ( k = g -> ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) <-> ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) ) )
20 fveq1 
 |-  ( k = g -> ( k ` 0 ) = ( g ` 0 ) )
21 20 eqeq1d 
 |-  ( k = g -> ( ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) <-> ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) )
22 19 21 anbi12d 
 |-  ( k = g -> ( ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) /\ ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) <-> ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) )
23 22 cbvriotavw 
 |-  ( iota_ k e. ( II Cn C ) ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) /\ ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 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 e. ( 0 [,] 1 ) |-> ( u G z ) ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) )
26 25 eqeq2d 
 |-  ( u = x -> ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) <-> ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) ) )
27 fveq2 
 |-  ( u = x -> ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) )
28 27 eqeq2d 
 |-  ( u = x -> ( ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) <-> ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) )
29 26 28 anbi12d 
 |-  ( u = x -> ( ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) <-> ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) )
30 29 riotabidv 
 |-  ( u = x -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( u G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) )
31 23 30 syl5eq 
 |-  ( u = x -> ( iota_ k e. ( II Cn C ) ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) /\ ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) )
32 31 fveq1d 
 |-  ( u = x -> ( ( iota_ k e. ( II Cn C ) ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) /\ ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) ` v ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) ` v ) )
33 fveq2 
 |-  ( v = y -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) ` v ) = ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) ` y ) )
34 32 33 cbvmpov 
 |-  ( u e. ( 0 [,] 1 ) , v e. ( 0 [,] 1 ) |-> ( ( iota_ k e. ( II Cn C ) ( ( F o. k ) = ( w e. ( 0 [,] 1 ) |-> ( u G w ) ) /\ ( k ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` u ) ) ) ` v ) ) = ( x e. ( 0 [,] 1 ) , y e. ( 0 [,] 1 ) |-> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( z e. ( 0 [,] 1 ) |-> ( x G z ) ) /\ ( g ` 0 ) = ( ( iota_ h e. ( II Cn C ) ( ( F o. h ) = ( w e. ( 0 [,] 1 ) |-> ( w G 0 ) ) /\ ( h ` 0 ) = P ) ) ` x ) ) ) ` y ) )
35 1 2 3 4 5 14 34 cvmlift2lem13 
 |-  ( ph -> E! f e. ( ( II tX II ) Cn C ) ( ( F o. f ) = G /\ ( 0 f 0 ) = P ) )