Metamath Proof Explorer

Theorem cvmliftlem4

Description: Lemma for cvmlift . The function Q will be our lifted path, defined piecewise on each section [ ( M - 1 ) / N , M / N ] for M e. ( 1 ... N ) . For M = 0 , it is a "seed" value which makes the rest of the recursion work, a singleton function mapping 0 to P . (Contributed by Mario Carneiro, 15-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 >. } >. } ) )
Assertion cvmliftlem4 
|- ( Q ` 0 ) = { <. 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 12 fveq1i 
 |-  ( Q ` 0 ) = ( 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 >. } >. } ) ) ` 0 )
14 0z 
 |-  0 e. ZZ
15 seq1 
 |-  ( 0 e. ZZ -> ( 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 >. } >. } ) ) ` 0 ) = ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` 0 ) )
16 14 15 ax-mp 
 |-  ( 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 >. } >. } ) ) ` 0 ) = ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` 0 )
17 13 16 eqtri 
 |-  ( Q ` 0 ) = ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` 0 )
18 fnresi 
 |-  ( _I |` NN ) Fn NN
19 c0ex 
 |-  0 e. _V
20 snex 
 |-  { <. 0 , P >. } e. _V
21 19 20 fnsn 
 |-  { <. 0 , { <. 0 , P >. } >. } Fn { 0 }
22 0nnn 
 |-  -. 0 e. NN
23 disjsn 
 |-  ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
24 22 23 mpbir 
 |-  ( NN i^i { 0 } ) = (/)
25 19 snid 
 |-  0 e. { 0 }
26 24 25 pm3.2i 
 |-  ( ( NN i^i { 0 } ) = (/) /\ 0 e. { 0 } )
27 fvun2 
 |-  ( ( ( _I |` NN ) Fn NN /\ { <. 0 , { <. 0 , P >. } >. } Fn { 0 } /\ ( ( NN i^i { 0 } ) = (/) /\ 0 e. { 0 } ) ) -> ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` 0 ) = ( { <. 0 , { <. 0 , P >. } >. } ` 0 ) )
28 18 21 26 27 mp3an 
 |-  ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` 0 ) = ( { <. 0 , { <. 0 , P >. } >. } ` 0 )
29 17 28 eqtri 
 |-  ( Q ` 0 ) = ( { <. 0 , { <. 0 , P >. } >. } ` 0 )
30 19 20 fvsn 
 |-  ( { <. 0 , { <. 0 , P >. } >. } ` 0 ) = { <. 0 , P >. }
31 29 30 eqtri 
 |-  ( Q ` 0 ) = { <. 0 , P >. }