Metamath Proof Explorer

Theorem cvmliftlem6

Description: Lemma for cvmlift . Induction step for cvmliftlem7 . Assuming that Q ( M - 1 ) is defined at ( M - 1 ) / N and is a preimage of G ( ( M - 1 ) / N ) , the next segment Q ( M ) is also defined and is a function on W which is a lift G for this segment. This follows explicitly from the definition Q ( M ) =`' ( F |`I ) o. G since G is in 1st( FM ) for the entire interval so that ` ``' ( F |`I ) maps this into I and F o. Q maps back to 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 >. } >. } ) )
cvmliftlem5.3 
|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
cvmliftlem6.1 
|- ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
cvmliftlem6.2 
|- ( ( ph /\ ps ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
Assertion cvmliftlem6 
|- ( ( ph /\ ps ) -> ( ( Q ` M ) : W --> B /\ ( F o. ( Q ` M ) ) = ( G |` W ) ) )

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 cvmliftlem6.1 
 |-  ( ( ph /\ ps ) -> M e. ( 1 ... N ) )
15 cvmliftlem6.2 
 |-  ( ( ph /\ ps ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
16 14 adantrr 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> M e. ( 1 ... N ) )
17 1 2 3 4 5 6 7 8 9 10 11 16 cvmliftlem1 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
18 1 cvmsss 
 |-  ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 2nd ` ( T ` M ) ) C_ C )
19 17 18 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( 2nd ` ( T ` M ) ) C_ C )
20 4 adantr 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> F e. ( C CovMap J ) )
21 15 adantrr 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
22 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
23 2 3 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> X )
24 20 22 23 3syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> F : B --> X )
25 ffn 
 |-  ( F : B --> X -> F Fn B )
26 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 ) ) ) ) )
27 24 25 26 3syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( ( 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 ) ) ) ) )
28 21 27 mpbid 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) ) )
29 28 simpld 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
30 28 simprd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
31 elfznn 
 |-  ( M e. ( 1 ... N ) -> M e. NN )
32 16 31 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> M e. NN )
33 32 nnred 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> M e. RR )
34 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
35 33 34 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( M - 1 ) e. RR )
36 8 adantr 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> N e. NN )
37 35 36 nndivred 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) e. RR )
38 37 rexrd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) e. RR* )
39 33 36 nndivred 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( M / N ) e. RR )
40 39 rexrd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( M / N ) e. RR* )
41 33 ltm1d 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( M - 1 ) < M )
42 36 nnred 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> N e. RR )
43 36 nngt0d 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> 0 < N )
44 ltdiv1 
 |-  ( ( ( M - 1 ) e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
45 35 33 42 43 44 syl112anc 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
46 41 45 mpbid 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) < ( M / N ) )
47 37 39 46 ltled 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
48 lbicc2 
 |-  ( ( ( ( M - 1 ) / N ) e. RR* /\ ( M / N ) e. RR* /\ ( ( M - 1 ) / N ) <_ ( M / N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
49 38 40 47 48 syl3anc 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
50 49 13 eleqtrrdi 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( M - 1 ) / N ) e. W )
51 1 2 3 4 5 6 7 8 9 10 11 16 13 50 cvmliftlem3 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
52 30 51 eqeltrd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
53 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 )
54 1 2 53 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 ) ) )
55 20 17 29 52 54 syl13anc 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( 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 ) ) )
56 55 simpld 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) )
57 19 56 sseldd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. C )
58 elssuni 
 |-  ( ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. C -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) C_ U. C )
59 57 58 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) C_ U. C )
60 59 2 sseqtrrdi 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) C_ B )
61 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 ) ) )
62 20 17 56 61 syl3anc 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( 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 ) ) )
63 f1ocnv 
 |-  ( ( 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 ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( 1st ` ( T ` M ) ) -1-1-onto-> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
64 f1of 
 |-  ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( 1st ` ( T ` M ) ) -1-1-onto-> ( 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 ) ) : ( 1st ` ( T ` M ) ) --> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
65 62 63 64 3syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) : ( 1st ` ( T ` M ) ) --> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
66 simprr 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> z e. W )
67 1 2 3 4 5 6 7 8 9 10 11 16 13 66 cvmliftlem3 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
68 65 67 ffvelrnd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) e. ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) )
69 60 68 sseldd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) e. B )
70 69 anassrs 
 |-  ( ( ( ph /\ ps ) /\ z e. W ) -> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) e. B )
71 70 fmpttd 
 |-  ( ( ph /\ ps ) -> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) : W --> B )
72 14 31 syl 
 |-  ( ( ph /\ ps ) -> M e. NN )
73 1 2 3 4 5 6 7 8 9 10 11 12 13 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 ) ) ) )
74 72 73 syldan 
 |-  ( ( ph /\ ps ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
75 74 feq1d 
 |-  ( ( ph /\ ps ) -> ( ( Q ` M ) : W --> B <-> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) : W --> B ) )
76 71 75 mpbird 
 |-  ( ( ph /\ ps ) -> ( Q ` M ) : W --> B )
77 fvres 
 |-  ( z e. W -> ( ( G |` W ) ` z ) = ( G ` z ) )
78 66 77 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( G |` W ) ` z ) = ( G ` z ) )
79 f1ocnvfv2 
 |-  ( ( ( 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 ) ) /\ ( G ` z ) e. ( 1st ` ( T ` M ) ) ) -> ( ( F |` ( 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 ) ) ` ( G ` z ) ) ) = ( G ` z ) )
80 62 67 79 syl2anc 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( F |` ( 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 ) ) ` ( G ` z ) ) ) = ( G ` z ) )
81 fvres 
 |-  ( ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) 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 ) ) ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) = ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
82 68 81 syl 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( ( F |` ( 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 ) ) ` ( G ` z ) ) ) = ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
83 78 80 82 3eqtr2rd 
 |-  ( ( ph /\ ( ps /\ z e. W ) ) -> ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) = ( ( G |` W ) ` z ) )
84 83 anassrs 
 |-  ( ( ( ph /\ ps ) /\ z e. W ) -> ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) = ( ( G |` W ) ` z ) )
85 84 mpteq2dva 
 |-  ( ( ph /\ ps ) -> ( z e. W |-> ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) = ( z e. W |-> ( ( G |` W ) ` z ) ) )
86 4 22 23 3syl 
 |-  ( ph -> F : B --> X )
87 86 adantr 
 |-  ( ( ph /\ ps ) -> F : B --> X )
88 87 feqmptd 
 |-  ( ( ph /\ ps ) -> F = ( y e. B |-> ( F ` y ) ) )
89 fveq2 
 |-  ( y = ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) -> ( F ` y ) = ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
90 70 74 88 89 fmptco 
 |-  ( ( ph /\ ps ) -> ( F o. ( Q ` M ) ) = ( z e. W |-> ( F ` ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) )
91 iiuni 
 |-  ( 0 [,] 1 ) = U. II
92 91 3 cnf 
 |-  ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
93 5 92 syl 
 |-  ( ph -> G : ( 0 [,] 1 ) --> X )
94 93 adantr 
 |-  ( ( ph /\ ps ) -> G : ( 0 [,] 1 ) --> X )
95 1 2 3 4 5 6 7 8 9 10 11 14 13 cvmliftlem2 
 |-  ( ( ph /\ ps ) -> W C_ ( 0 [,] 1 ) )
96 94 95 fssresd 
 |-  ( ( ph /\ ps ) -> ( G |` W ) : W --> X )
97 96 feqmptd 
 |-  ( ( ph /\ ps ) -> ( G |` W ) = ( z e. W |-> ( ( G |` W ) ` z ) ) )
98 85 90 97 3eqtr4d 
 |-  ( ( ph /\ ps ) -> ( F o. ( Q ` M ) ) = ( G |` W ) )
99 76 98 jca 
 |-  ( ( ph /\ ps ) -> ( ( Q ` M ) : W --> B /\ ( F o. ( Q ` M ) ) = ( G |` W ) ) )