Metamath Proof Explorer

Theorem cvmliftlem14

Description: Lemma for cvmlift . Putting the results of cvmliftlem11 , cvmliftlem13 and cvmliftmo together, we have that K is a continuous function, satisfies F o. K = G and K ( 0 ) = P , and is equal to any other function which also has these properties, so it follows that K is the unique lift of G . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypotheses cvmliftlem.1 
|- S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
cvmliftlem.b 
|- B = U. C
cvmliftlem.x 
|- X = U. J
cvmliftlem.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmliftlem.g 
|- ( ph -> G e. ( II Cn J ) )
cvmliftlem.p 
|- ( ph -> P e. B )
cvmliftlem.e 
|- ( ph -> ( F ` P ) = ( G ` 0 ) )
cvmliftlem.n 
|- ( ph -> N e. NN )
cvmliftlem.t 
|- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
cvmliftlem.a 
|- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
cvmliftlem.l 
|- L = ( topGen ` ran (,) )
cvmliftlem.q 
|- Q = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
cvmliftlem.k 
|- K = U_ k e. ( 1 ... N ) ( Q ` k )
Assertion cvmliftlem14 
|- ( ph -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmliftlem.b 
 |-  B = U. C
3 cvmliftlem.x 
 |-  X = U. J
4 cvmliftlem.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmliftlem.g 
 |-  ( ph -> G e. ( II Cn J ) )
6 cvmliftlem.p 
 |-  ( ph -> P e. B )
7 cvmliftlem.e 
 |-  ( ph -> ( F ` P ) = ( G ` 0 ) )
8 cvmliftlem.n 
 |-  ( ph -> N e. NN )
9 cvmliftlem.t 
 |-  ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
10 cvmliftlem.a 
 |-  ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
11 cvmliftlem.l 
 |-  L = ( topGen ` ran (,) )
12 cvmliftlem.q 
 |-  Q = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
13 cvmliftlem.k 
 |-  K = U_ k e. ( 1 ... N ) ( Q ` k )
14 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem11 
 |-  ( ph -> ( K e. ( II Cn C ) /\ ( F o. K ) = G ) )
15 14 simpld 
 |-  ( ph -> K e. ( II Cn C ) )
16 14 simprd 
 |-  ( ph -> ( F o. K ) = G )
17 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem13 
 |-  ( ph -> ( K ` 0 ) = P )
18 coeq2 
 |-  ( f = K -> ( F o. f ) = ( F o. K ) )
19 18 eqeq1d 
 |-  ( f = K -> ( ( F o. f ) = G <-> ( F o. K ) = G ) )
20 fveq1 
 |-  ( f = K -> ( f ` 0 ) = ( K ` 0 ) )
21 20 eqeq1d 
 |-  ( f = K -> ( ( f ` 0 ) = P <-> ( K ` 0 ) = P ) )
22 19 21 anbi12d 
 |-  ( f = K -> ( ( ( F o. f ) = G /\ ( f ` 0 ) = P ) <-> ( ( F o. K ) = G /\ ( K ` 0 ) = P ) ) )
23 22 rspcev 
 |-  ( ( K e. ( II Cn C ) /\ ( ( F o. K ) = G /\ ( K ` 0 ) = P ) ) -> E. f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
24 15 16 17 23 syl12anc 
 |-  ( ph -> E. f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
25 iiuni 
 |-  ( 0 [,] 1 ) = U. II
26 iiconn 
 |-  II e. Conn
27 26 a1i 
 |-  ( ph -> II e. Conn )
28 iinllyconn 
 |-  II e. N-Locally Conn
29 28 a1i 
 |-  ( ph -> II e. N-Locally Conn )
30 0elunit 
 |-  0 e. ( 0 [,] 1 )
31 30 a1i 
 |-  ( ph -> 0 e. ( 0 [,] 1 ) )
32 2 25 4 27 29 31 5 6 7 cvmliftmo 
 |-  ( ph -> E* f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )
33 reu5 
 |-  ( E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) <-> ( E. f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) /\ E* f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) ) )
34 24 32 33 sylanbrc 
 |-  ( ph -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )