Metamath Proof Explorer

Theorem cvmliftlem9

Description: Lemma for cvmlift . The Q ( M ) functions are defined on almost disjoint intervals, but they overlap at the edges. Here we show that at these points the Q functions agree on their common domain. (Contributed by Mario Carneiro, 14-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 cvmliftlem9 
|- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` M ) ` ( ( M - 1 ) / N ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) )

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 elfznn 
 |-  ( M e. ( 1 ... N ) -> M e. NN )
14 eqid 
 |-  ( ( ( M - 1 ) / N ) [,] ( M / N ) ) = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
15 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem5 
 |-  ( ( ph /\ M e. NN ) -> ( Q ` M ) = ( z e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
16 13 15 sylan2 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) = ( z e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
17 simpr 
 |-  ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z = ( ( M - 1 ) / N ) ) -> z = ( ( M - 1 ) / N ) )
18 17 fveq2d 
 |-  ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z = ( ( M - 1 ) / N ) ) -> ( G ` z ) = ( G ` ( ( M - 1 ) / N ) ) )
19 18 fveq2d 
 |-  ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z = ( ( M - 1 ) / N ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) = ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) )
20 13 adantl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. NN )
21 20 nnred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
22 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
23 21 22 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. RR )
24 8 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> N e. NN )
25 23 24 nndivred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
26 25 rexrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
27 21 24 nndivred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
28 27 rexrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
29 21 ltm1d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
30 24 nnred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
31 24 nngt0d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
32 ltdiv1 
 |-  ( ( ( M - 1 ) e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
33 23 21 30 31 32 syl112anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
34 29 33 mpbid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) < ( M / N ) )
35 25 27 34 ltled 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
36 lbicc2 
 |-  ( ( ( ( M - 1 ) / N ) e. RR* /\ ( M / N ) e. RR* /\ ( ( M - 1 ) / N ) <_ ( M / N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
37 26 28 35 36 syl3anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
38 fvexd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) e. _V )
39 16 19 37 38 fvmptd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` M ) ` ( ( M - 1 ) / N ) ) = ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) )
40 4 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> F e. ( C CovMap J ) )
41 simpr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. ( 1 ... N ) )
42 1 2 3 4 5 6 7 8 9 10 11 41 cvmliftlem1 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
43 1 2 3 4 5 6 7 8 9 10 11 12 14 cvmliftlem7 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
44 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
45 2 3 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> X )
46 40 44 45 3syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> F : B --> X )
47 ffn 
 |-  ( F : B --> X -> F Fn B )
48 fniniseg 
 |-  ( F Fn B -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) <-> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) ) )
49 46 47 48 3syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) <-> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) ) )
50 43 49 mpbid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) )
51 50 simpld 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
52 50 simprd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
53 1 2 3 4 5 6 7 8 9 10 11 41 14 37 cvmliftlem3 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
54 52 53 eqeltrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
55 eqid 
 |-  ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) = ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b )
56 1 2 55 cvmsiota 
 |-  ( ( F e. ( C CovMap J ) /\ ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) ) ) -> ( ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
57 40 42 51 54 56 syl13anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) )
58 57 simprd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
59 fvres 
 |-  ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) -> ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) )
60 58 59 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) )
61 60 52 eqtrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
62 57 simpld 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) )
63 1 cvmsf1o 
 |-  ( ( F e. ( C CovMap J ) /\ ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) /\ ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) -1-1-onto-> ( 1st ` ( T ` M ) ) )
64 40 42 62 63 syl3anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) -1-1-onto-> ( 1st ` ( T ` M ) ) )
65 f1ocnvfv 
 |-  ( ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) -1-1-onto-> ( 1st ` ( T ` M ) ) /\ ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) -> ( ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) )
66 64 58 65 syl2anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) )
67 61 66 mpd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` ( ( M - 1 ) / N ) ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) )
68 39 67 eqtrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` M ) ` ( ( M - 1 ) / N ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) )