Metamath Proof Explorer

Theorem cvmliftlem8

Description: Lemma for cvmlift . The functions Q are continuous functions because they are defined as ` ``' ( F |`I ) o. G where G is continuous and ` ( F |`I ) is a homeomorphism. (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 ) )
Assertion cvmliftlem8 
|- ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L |`t W ) Cn C ) )

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 elfznn 
 |-  ( M e. ( 1 ... N ) -> M e. NN )
15 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 ) ) ) )
16 14 15 sylan2 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) = ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) )
17 4 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> F e. ( C CovMap J ) )
18 cvmtop1 
 |-  ( F e. ( C CovMap J ) -> C e. Top )
19 cnrest2r 
 |-  ( C e. Top -> ( ( L |`t W ) Cn ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) C_ ( ( L |`t W ) Cn C ) )
20 17 18 19 3syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L |`t W ) Cn ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) C_ ( ( L |`t W ) Cn C ) )
21 retopon 
 |-  ( topGen ` ran (,) ) e. ( TopOn ` RR )
22 11 21 eqeltri 
 |-  L e. ( TopOn ` RR )
23 simpr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. ( 1 ... N ) )
24 1 2 3 4 5 6 7 8 9 10 11 23 13 cvmliftlem2 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ ( 0 [,] 1 ) )
25 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
26 24 25 sstrdi 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> W C_ RR )
27 resttopon 
 |-  ( ( L e. ( TopOn ` RR ) /\ W C_ RR ) -> ( L |`t W ) e. ( TopOn ` W ) )
28 22 26 27 sylancr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( L |`t W ) e. ( TopOn ` W ) )
29 eqid 
 |-  ( II |`t W ) = ( II |`t W )
30 iitopon 
 |-  II e. ( TopOn ` ( 0 [,] 1 ) )
31 30 a1i 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> II e. ( TopOn ` ( 0 [,] 1 ) ) )
32 5 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> G e. ( II Cn J ) )
33 iiuni 
 |-  ( 0 [,] 1 ) = U. II
34 33 3 cnf 
 |-  ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
35 32 34 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> G : ( 0 [,] 1 ) --> X )
36 35 feqmptd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> G = ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) )
37 36 32 eqeltrrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. ( 0 [,] 1 ) |-> ( G ` z ) ) e. ( II Cn J ) )
38 29 31 24 37 cnmpt1res 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( II |`t W ) Cn J ) )
39 dfii2 
 |-  II = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
40 11 oveq1i 
 |-  ( L |`t ( 0 [,] 1 ) ) = ( ( topGen ` ran (,) ) |`t ( 0 [,] 1 ) )
41 39 40 eqtr4i 
 |-  II = ( L |`t ( 0 [,] 1 ) )
42 41 oveq1i 
 |-  ( II |`t W ) = ( ( L |`t ( 0 [,] 1 ) ) |`t W )
43 retop 
 |-  ( topGen ` ran (,) ) e. Top
44 11 43 eqeltri 
 |-  L e. Top
45 44 a1i 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> L e. Top )
46 ovexd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 [,] 1 ) e. _V )
47 restabs 
 |-  ( ( L e. Top /\ W C_ ( 0 [,] 1 ) /\ ( 0 [,] 1 ) e. _V ) -> ( ( L |`t ( 0 [,] 1 ) ) |`t W ) = ( L |`t W ) )
48 45 24 46 47 syl3anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( L |`t ( 0 [,] 1 ) ) |`t W ) = ( L |`t W ) )
49 42 48 eqtrid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( II |`t W ) = ( L |`t W ) )
50 49 oveq1d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( II |`t W ) Cn J ) = ( ( L |`t W ) Cn J ) )
51 38 50 eleqtrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn J ) )
52 cvmtop2 
 |-  ( F e. ( C CovMap J ) -> J e. Top )
53 17 52 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> J e. Top )
54 3 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
55 53 54 sylib 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> J e. ( TopOn ` X ) )
56 simprl 
 |-  ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> M e. ( 1 ... N ) )
57 simprr 
 |-  ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> z e. W )
58 1 2 3 4 5 6 7 8 9 10 11 56 13 57 cvmliftlem3 
 |-  ( ( ph /\ ( M e. ( 1 ... N ) /\ z e. W ) ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
59 58 anassrs 
 |-  ( ( ( ph /\ M e. ( 1 ... N ) ) /\ z e. W ) -> ( G ` z ) e. ( 1st ` ( T ` M ) ) )
60 59 fmpttd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) : W --> ( 1st ` ( T ` M ) ) )
61 60 frnd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) )
62 1 2 3 4 5 6 7 8 9 10 11 23 cvmliftlem1 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) )
63 1 cvmsrcl 
 |-  ( ( 2nd ` ( T ` M ) ) e. ( S ` ( 1st ` ( T ` M ) ) ) -> ( 1st ` ( T ` M ) ) e. J )
64 elssuni 
 |-  ( ( 1st ` ( T ` M ) ) e. J -> ( 1st ` ( T ` M ) ) C_ U. J )
65 62 63 64 3syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ U. J )
66 65 3 sseqtrrdi 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 1st ` ( T ` M ) ) C_ X )
67 cnrest2 
 |-  ( ( J e. ( TopOn ` X ) /\ ran ( z e. W |-> ( G ` z ) ) C_ ( 1st ` ( T ` M ) ) /\ ( 1st ` ( T ` M ) ) C_ X ) -> ( ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn J ) <-> ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn ( J |`t ( 1st ` ( T ` M ) ) ) ) ) )
68 55 61 66 67 syl3anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn J ) <-> ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn ( J |`t ( 1st ` ( T ` M ) ) ) ) ) )
69 51 68 mpbid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( G ` z ) ) e. ( ( L |`t W ) Cn ( J |`t ( 1st ` ( T ` M ) ) ) ) )
70 1 2 3 4 5 6 7 8 9 10 11 12 13 cvmliftlem7 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
71 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
72 2 3 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> X )
73 17 71 72 3syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> F : B --> X )
74 ffn 
 |-  ( F : B --> X -> F Fn B )
75 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 ) ) ) ) )
76 73 74 75 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 ) ) ) ) )
77 70 76 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 ) ) ) )
78 77 simpld 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. B )
79 77 simprd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) = ( G ` ( ( M - 1 ) / N ) ) )
80 14 adantl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. NN )
81 80 nnred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. RR )
82 peano2rem 
 |-  ( M e. RR -> ( M - 1 ) e. RR )
83 81 82 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. RR )
84 8 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> N e. NN )
85 83 84 nndivred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR )
86 85 rexrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. RR* )
87 81 84 nndivred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR )
88 87 rexrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M / N ) e. RR* )
89 81 ltm1d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) < M )
90 84 nnred 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> N e. RR )
91 84 nngt0d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> 0 < N )
92 ltdiv1 
 |-  ( ( ( M - 1 ) e. RR /\ M e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
93 83 81 90 91 92 syl112anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) < M <-> ( ( M - 1 ) / N ) < ( M / N ) ) )
94 89 93 mpbid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) < ( M / N ) )
95 85 87 94 ltled 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) <_ ( M / N ) )
96 lbicc2 
 |-  ( ( ( ( M - 1 ) / N ) e. RR* /\ ( M / N ) e. RR* /\ ( ( M - 1 ) / N ) <_ ( M / N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
97 86 88 95 96 syl3anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. ( ( ( M - 1 ) / N ) [,] ( M / N ) ) )
98 97 13 eleqtrrdi 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( M - 1 ) / N ) e. W )
99 1 2 3 4 5 6 7 8 9 10 11 23 13 98 cvmliftlem3 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( G ` ( ( M - 1 ) / N ) ) e. ( 1st ` ( T ` M ) ) )
100 79 99 eqeltrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F ` ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) ) e. ( 1st ` ( T ` M ) ) )
101 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 )
102 1 2 101 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 ) ) )
103 17 62 78 100 102 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 ) ) )
104 103 simpld 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) e. ( 2nd ` ( T ` M ) ) )
105 1 cvmshmeo 
 |-  ( ( ( 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 ) ) e. ( ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J |`t ( 1st ` ( T ` M ) ) ) ) )
106 62 104 105 syl2anc 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J |`t ( 1st ` ( T ` M ) ) ) ) )
107 hmeocnvcn 
 |-  ( ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) Homeo ( J |`t ( 1st ` ( T ` M ) ) ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( J |`t ( 1st ` ( T ` M ) ) ) Cn ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
108 106 107 syl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) e. ( ( J |`t ( 1st ` ( T ` M ) ) ) Cn ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
109 28 69 108 cnmpt11f 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) e. ( ( L |`t W ) Cn ( C |`t ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ) )
110 20 109 sseldd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( z e. W |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` M ) ) ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) e. ( ( L |`t W ) Cn C ) )
111 16 110 eqeltrd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( Q ` M ) e. ( ( L |`t W ) Cn C ) )