Metamath Proof Explorer

Theorem cvmlift

Description: One of the important properties of covering maps is that any path G in the base space "lifts" to a path f in the covering space such that F o. f = G , and given a starting point P in the covering space this lift is unique. The proof is contained in cvmliftlem1 thru cvmliftlem15 . (Contributed by Mario Carneiro, 16-Feb-2015)

Ref Expression
Hypothesis cvmlift.1 
|- B = U. C
Assertion cvmlift 
|- ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )

Proof

Step Hyp Ref Expression
1 cvmlift.1 
 |-  B = U. C
2 eqid 
 |-  ( 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 ) ) ) ) } ) = ( 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 ) ) ) ) } )
3 2 cvmscbv 
 |-  ( 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 ) ) ) ) } ) = ( a e. J |-> { b e. ( ~P C \ { (/) } ) | ( U. b = ( `' F " a ) /\ A. c e. b ( A. d e. ( b \ { c } ) ( c i^i d ) = (/) /\ ( F |` c ) e. ( ( C |`t c ) Homeo ( J |`t a ) ) ) ) } )
4 eqid 
 |-  U. J = U. J
5 simpll 
 |-  ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> F e. ( C CovMap J ) )
6 simplr 
 |-  ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> G e. ( II Cn J ) )
7 simprl 
 |-  ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> P e. B )
8 simprr 
 |-  ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> ( F ` P ) = ( G ` 0 ) )
9 3 1 4 5 6 7 8 cvmliftlem15 
 |-  ( ( ( F e. ( C CovMap J ) /\ G e. ( II Cn J ) ) /\ ( P e. B /\ ( F ` P ) = ( G ` 0 ) ) ) -> E! f e. ( II Cn C ) ( ( F o. f ) = G /\ ( f ` 0 ) = P ) )