Metamath Proof Explorer

Theorem cvmliftlem5

Description: Lemma for cvmlift . Definition of Q at a successor. This is a function defined on W as ` ``' ( T |`I ) o. G where I is the unique covering set of 2nd( TM ) that contains Q ( M - 1 ) evaluated at the last defined point, namely ( M - 1 ) / N (note that for M = 1 this is using the seed value Q ( 0 ) ( 0 ) = 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 >. } >. } ) )
cvmliftlem5.3 
|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
Assertion cvmliftlem5 
|- ( ( ph /\ M e. NN ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )

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 cvmliftlem5.3 
 |-  W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
14 0z 
 |-  0 e. ZZ
15 simpr 
 |-  ( ( ph /\ M e. NN ) -> M e. NN )
16 nnuz 
 |-  NN = ( ZZ>= ` 1 )
17 1e0p1 
 |-  1 = ( 0 + 1 )
18 17 fveq2i 
 |-  ( ZZ>= ` 1 ) = ( ZZ>= ` ( 0 + 1 ) )
19 16 18 eqtri 
 |-  NN = ( ZZ>= ` ( 0 + 1 ) )
20 15 19 eleqtrdi 
 |-  ( ( ph /\ M e. NN ) -> M e. ( ZZ>= ` ( 0 + 1 ) ) )
21 seqm1 
 |-  ( ( 0 e. ZZ /\ M e. ( ZZ>= ` ( 0 + 1 ) ) ) -> ( 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 >. } >. } ) ) ` M ) = ( ( 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 >. } >. } ) ) ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) ) )
22 14 20 21 sylancr 
 |-  ( ( ph /\ M e. NN ) -> ( 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 >. } >. } ) ) ` M ) = ( ( 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 >. } >. } ) ) ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) ) )
23 12 fveq1i 
 |-  ( Q ` M ) = ( 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 >. } >. } ) ) ` M )
24 12 fveq1i 
 |-  ( Q ` ( M - 1 ) ) = ( 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 >. } >. } ) ) ` ( M - 1 ) )
25 24 oveq1i 
 |-  ( ( Q ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) ) = ( ( 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 >. } >. } ) ) ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) )
26 22 23 25 3eqtr4g 
 |-  ( ( ph /\ M e. NN ) -> ( Q ` M ) = ( ( Q ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) ) )
27 0nnn 
 |-  -. 0 e. NN
28 disjsn 
 |-  ( ( NN i^i { 0 } ) = (/) <-> -. 0 e. NN )
29 27 28 mpbir 
 |-  ( NN i^i { 0 } ) = (/)
30 fnresi 
 |-  ( _I |` NN ) Fn NN
31 c0ex 
 |-  0 e. _V
32 snex 
 |-  { <. 0 , P >. } e. _V
33 31 32 fnsn 
 |-  { <. 0 , { <. 0 , P >. } >. } Fn { 0 }
34 fvun1 
 |-  ( ( ( _I |` NN ) Fn NN /\ { <. 0 , { <. 0 , P >. } >. } Fn { 0 } /\ ( ( NN i^i { 0 } ) = (/) /\ M e. NN ) ) -> ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` M ) = ( ( _I |` NN ) ` M ) )
35 30 33 34 mp3an12 
 |-  ( ( ( NN i^i { 0 } ) = (/) /\ M e. NN ) -> ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` M ) = ( ( _I |` NN ) ` M ) )
36 29 15 35 sylancr 
 |-  ( ( ph /\ M e. NN ) -> ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` M ) = ( ( _I |` NN ) ` M ) )
37 fvresi 
 |-  ( M e. NN -> ( ( _I |` NN ) ` M ) = M )
38 37 adantl 
 |-  ( ( ph /\ M e. NN ) -> ( ( _I |` NN ) ` M ) = M )
39 36 38 eqtrd 
 |-  ( ( ph /\ M e. NN ) -> ( ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) ` M ) = M )
40 39 oveq2d 
 |-  ( ( ph /\ M e. NN ) -> ( ( Q ` ( M - 1 ) ) ( 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 >. } >. } ) ` M ) ) = ( ( Q ` ( M - 1 ) ) ( 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 ) ) ) ) M ) )
41 fvexd 
 |-  ( ph -> ( Q ` ( M - 1 ) ) e. _V )
42 simpr 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> m = M )
43 42 oveq1d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( m - 1 ) = ( M - 1 ) )
44 43 oveq1d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( ( m - 1 ) / N ) = ( ( M - 1 ) / N ) )
45 42 oveq1d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( m / N ) = ( M / N ) )
46 44 45 oveq12d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( ( ( m - 1 ) / N ) [,] ( m / N ) ) = ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
47 46 13 eqtr4di 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( ( ( m - 1 ) / N ) [,] ( m / N ) ) = W )
48 42 fveq2d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( T ` m ) = ( T ` M ) )
49 48 fveq2d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( 2nd ` ( T ` m ) ) = ( 2nd ` ( T ` M ) ) )
50 simpl 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> x = ( Q ` ( M - 1 ) ) )
51 50 44 fveq12d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( x ` ( ( m - 1 ) / N ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) )
52 51 eleq1d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( ( x ` ( ( m - 1 ) / N ) ) e. b <-> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
53 49 52 riotaeqbidv 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) = ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
54 53 reseq2d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) = ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
55 54 cnveqd 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) = `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
56 55 fveq1d 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) = ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) )
57 47 56 mpteq12dv 
 |-  ( ( x = ( Q ` ( M - 1 ) ) /\ m = M ) -> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
58 eqid 
 |-  ( 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 ) ) ) ) = ( 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 ) ) ) )
59 ovex 
 |-  ( ( ( M - 1 ) / N ) [,] ( M / N ) ) e. _V
60 13 59 eqeltri 
 |-  W e. _V
61 60 mptex 
 |-  ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) e. _V
62 57 58 61 ovmpoa 
 |-  ( ( ( Q ` ( M - 1 ) ) e. _V /\ M e. NN ) -> ( ( Q ` ( M - 1 ) ) ( 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 ) ) ) ) M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
63 41 62 sylan 
 |-  ( ( ph /\ M e. NN ) -> ( ( Q ` ( M - 1 ) ) ( 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 ) ) ) ) M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
64 26 40 63 3eqtrd 
 |-  ( ( ph /\ M e. NN ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )