Metamath Proof Explorer

Theorem cvmliftlem10

Description: Lemma for cvmlift . The function K is going to be our complete lifted path, formed by unioning together all the Q functions (each of which is defined on one segment [ ( M - 1 ) / N , M / N ] of the interval). Here we prove by induction that K is a continuous function and a lift of G by applying cvmliftlem6 , cvmliftlem7 (to show it is a function and a lift), cvmliftlem8 (to show it is continuous), and cvmliftlem9 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste gives that K is well-defined and continuous). (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 >. } >. } ) )
cvmliftlem.k 
|- K = U_ k e. ( 1 ... N ) ( Q ` k )
cvmliftlem10.1 
|- ( ch <-> ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )
Assertion cvmliftlem10 
|- ( ph -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / 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 cvmliftlem.k 
 |-  K = U_ k e. ( 1 ... N ) ( Q ` k )
14 cvmliftlem10.1 
 |-  ( ch <-> ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )
15 nnuz 
 |-  NN = ( ZZ>= ` 1 )
16 8 15 eleqtrdi 
 |-  ( ph -> N e. ( ZZ>= ` 1 ) )
17 eluzfz2 
 |-  ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
18 16 17 syl 
 |-  ( ph -> N e. ( 1 ... N ) )
19 eleq1 
 |-  ( y = 1 -> ( y e. ( 1 ... N ) <-> 1 e. ( 1 ... N ) ) )
20 oveq2 
 |-  ( y = 1 -> ( 1 ... y ) = ( 1 ... 1 ) )
21 1z 
 |-  1 e. ZZ
22 fzsn 
 |-  ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
23 21 22 ax-mp 
 |-  ( 1 ... 1 ) = { 1 }
24 20 23 eqtrdi 
 |-  ( y = 1 -> ( 1 ... y ) = { 1 } )
25 24 iuneq1d 
 |-  ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. { 1 } ( Q ` k ) )
26 1ex 
 |-  1 e. _V
27 fveq2 
 |-  ( k = 1 -> ( Q ` k ) = ( Q ` 1 ) )
28 26 27 iunxsn 
 |-  U_ k e. { 1 } ( Q ` k ) = ( Q ` 1 )
29 25 28 eqtrdi 
 |-  ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = ( Q ` 1 ) )
30 oveq1 
 |-  ( y = 1 -> ( y / N ) = ( 1 / N ) )
31 30 oveq2d 
 |-  ( y = 1 -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( 1 / N ) ) )
32 31 oveq2d 
 |-  ( y = 1 -> ( L |`t ( 0 [,] ( y / N ) ) ) = ( L |`t ( 0 [,] ( 1 / N ) ) ) )
33 32 oveq1d 
 |-  ( y = 1 -> ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
34 29 33 eleq12d 
 |-  ( y = 1 -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) <-> ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) ) )
35 29 coeq2d 
 |-  ( y = 1 -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. ( Q ` 1 ) ) )
36 31 reseq2d 
 |-  ( y = 1 -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
37 35 36 eqeq12d 
 |-  ( y = 1 -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
38 34 37 anbi12d 
 |-  ( y = 1 -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) )
39 19 38 imbi12d 
 |-  ( y = 1 -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) ) )
40 39 imbi2d 
 |-  ( y = 1 -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) ) ) )
41 eleq1 
 |-  ( y = n -> ( y e. ( 1 ... N ) <-> n e. ( 1 ... N ) ) )
42 oveq2 
 |-  ( y = n -> ( 1 ... y ) = ( 1 ... n ) )
43 42 iuneq1d 
 |-  ( y = n -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
44 oveq1 
 |-  ( y = n -> ( y / N ) = ( n / N ) )
45 44 oveq2d 
 |-  ( y = n -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( n / N ) ) )
46 45 oveq2d 
 |-  ( y = n -> ( L |`t ( 0 [,] ( y / N ) ) ) = ( L |`t ( 0 [,] ( n / N ) ) ) )
47 46 oveq1d 
 |-  ( y = n -> ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) )
48 43 47 eleq12d 
 |-  ( y = n -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) <-> U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) ) )
49 43 coeq2d 
 |-  ( y = n -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) )
50 45 reseq2d 
 |-  ( y = n -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
51 49 50 eqeq12d 
 |-  ( y = n -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
52 48 51 anbi12d 
 |-  ( y = n -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) )
53 41 52 imbi12d 
 |-  ( y = n -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) )
54 53 imbi2d 
 |-  ( y = n -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) ) )
55 eleq1 
 |-  ( y = ( n + 1 ) -> ( y e. ( 1 ... N ) <-> ( n + 1 ) e. ( 1 ... N ) ) )
56 oveq2 
 |-  ( y = ( n + 1 ) -> ( 1 ... y ) = ( 1 ... ( n + 1 ) ) )
57 56 iuneq1d 
 |-  ( y = ( n + 1 ) -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
58 oveq1 
 |-  ( y = ( n + 1 ) -> ( y / N ) = ( ( n + 1 ) / N ) )
59 58 oveq2d 
 |-  ( y = ( n + 1 ) -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( ( n + 1 ) / N ) ) )
60 59 oveq2d 
 |-  ( y = ( n + 1 ) -> ( L |`t ( 0 [,] ( y / N ) ) ) = ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
61 60 oveq1d 
 |-  ( y = ( n + 1 ) -> ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
62 57 61 eleq12d 
 |-  ( y = ( n + 1 ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) ) )
63 57 coeq2d 
 |-  ( y = ( n + 1 ) -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) )
64 59 reseq2d 
 |-  ( y = ( n + 1 ) -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
65 63 64 eqeq12d 
 |-  ( y = ( n + 1 ) -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
66 62 65 anbi12d 
 |-  ( y = ( n + 1 ) -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) )
67 55 66 imbi12d 
 |-  ( y = ( n + 1 ) -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) ) )
68 67 imbi2d 
 |-  ( y = ( n + 1 ) -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) ) ) )
69 eleq1 
 |-  ( y = N -> ( y e. ( 1 ... N ) <-> N e. ( 1 ... N ) ) )
70 oveq2 
 |-  ( y = N -> ( 1 ... y ) = ( 1 ... N ) )
71 70 iuneq1d 
 |-  ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... N ) ( Q ` k ) )
72 71 13 eqtr4di 
 |-  ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = K )
73 oveq1 
 |-  ( y = N -> ( y / N ) = ( N / N ) )
74 73 oveq2d 
 |-  ( y = N -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( N / N ) ) )
75 74 oveq2d 
 |-  ( y = N -> ( L |`t ( 0 [,] ( y / N ) ) ) = ( L |`t ( 0 [,] ( N / N ) ) ) )
76 75 oveq1d 
 |-  ( y = N -> ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) )
77 72 76 eleq12d 
 |-  ( y = N -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) <-> K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) ) )
78 72 coeq2d 
 |-  ( y = N -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. K ) )
79 74 reseq2d 
 |-  ( y = N -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( N / N ) ) ) )
80 78 79 eqeq12d 
 |-  ( y = N -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )
81 77 80 anbi12d 
 |-  ( y = N -> ( ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) <-> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) )
82 69 81 imbi12d 
 |-  ( y = N -> ( ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) <-> ( N e. ( 1 ... N ) -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) ) )
83 82 imbi2d 
 |-  ( y = N -> ( ( ph -> ( y e. ( 1 ... N ) -> ( U_ k e. ( 1 ... y ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( y / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) ) ) ) <-> ( ph -> ( N e. ( 1 ... N ) -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) ) ) )
84 eluzfz1 
 |-  ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
85 16 84 syl 
 |-  ( ph -> 1 e. ( 1 ... N ) )
86 eqid 
 |-  ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) )
87 1 2 3 4 5 6 7 8 9 10 11 12 86 cvmliftlem8 
 |-  ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( Q ` 1 ) e. ( ( L |`t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
88 85 87 mpdan 
 |-  ( ph -> ( Q ` 1 ) e. ( ( L |`t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
89 1m1e0 
 |-  ( 1 - 1 ) = 0
90 89 oveq1i 
 |-  ( ( 1 - 1 ) / N ) = ( 0 / N )
91 8 nncnd 
 |-  ( ph -> N e. CC )
92 8 nnne0d 
 |-  ( ph -> N =/= 0 )
93 91 92 div0d 
 |-  ( ph -> ( 0 / N ) = 0 )
94 90 93 syl5eq 
 |-  ( ph -> ( ( 1 - 1 ) / N ) = 0 )
95 94 oveq1d 
 |-  ( ph -> ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( 0 [,] ( 1 / N ) ) )
96 95 oveq2d 
 |-  ( ph -> ( L |`t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( L |`t ( 0 [,] ( 1 / N ) ) ) )
97 96 oveq1d 
 |-  ( ph -> ( ( L |`t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
98 88 97 eleqtrd 
 |-  ( ph -> ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
99 simpr 
 |-  ( ( ph /\ 1 e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
100 1 2 3 4 5 6 7 8 9 10 11 12 86 cvmliftlem7 
 |-  ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( 1 - 1 ) / N ) ) } ) )
101 1 2 3 4 5 6 7 8 9 10 11 12 86 99 100 cvmliftlem6 
 |-  ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
102 85 101 mpdan 
 |-  ( ph -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
103 102 simprd 
 |-  ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) )
104 95 reseq2d 
 |-  ( ph -> ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
105 103 104 eqtrd 
 |-  ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
106 98 105 jca 
 |-  ( ph -> ( ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
107 106 a1d 
 |-  ( ph -> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L |`t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) )
108 elnnuz 
 |-  ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
109 108 biimpi 
 |-  ( n e. NN -> n e. ( ZZ>= ` 1 ) )
110 109 adantl 
 |-  ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
111 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` 1 ) /\ ( n + 1 ) e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
112 111 ex 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
113 110 112 syl 
 |-  ( ( ph /\ n e. NN ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
114 113 imim1d 
 |-  ( ( ph /\ n e. NN ) -> ( ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) -> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) )
115 eqid 
 |-  U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) = U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) )
116 0re 
 |-  0 e. RR
117 14 simplbi 
 |-  ( ch -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
118 117 adantl 
 |-  ( ( ph /\ ch ) -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
119 118 simprd 
 |-  ( ( ph /\ ch ) -> ( n + 1 ) e. ( 1 ... N ) )
120 elfznn 
 |-  ( ( n + 1 ) e. ( 1 ... N ) -> ( n + 1 ) e. NN )
121 119 120 syl 
 |-  ( ( ph /\ ch ) -> ( n + 1 ) e. NN )
122 121 nnred 
 |-  ( ( ph /\ ch ) -> ( n + 1 ) e. RR )
123 8 adantr 
 |-  ( ( ph /\ ch ) -> N e. NN )
124 122 123 nndivred 
 |-  ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR )
125 iccssre 
 |-  ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
126 116 124 125 sylancr 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
127 117 simpld 
 |-  ( ch -> n e. NN )
128 127 adantl 
 |-  ( ( ph /\ ch ) -> n e. NN )
129 128 nnred 
 |-  ( ( ph /\ ch ) -> n e. RR )
130 129 123 nndivred 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. RR )
131 icccld 
 |-  ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
132 116 130 131 sylancr 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
133 11 fveq2i 
 |-  ( Clsd ` L ) = ( Clsd ` ( topGen ` ran (,) ) )
134 132 133 eleqtrrdi 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` L ) )
135 ssun1 
 |-  ( 0 [,] ( n / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
136 116 a1i 
 |-  ( ( ph /\ ch ) -> 0 e. RR )
137 128 nnnn0d 
 |-  ( ( ph /\ ch ) -> n e. NN0 )
138 137 nn0ge0d 
 |-  ( ( ph /\ ch ) -> 0 <_ n )
139 123 nnred 
 |-  ( ( ph /\ ch ) -> N e. RR )
140 123 nngt0d 
 |-  ( ( ph /\ ch ) -> 0 < N )
141 divge0 
 |-  ( ( ( n e. RR /\ 0 <_ n ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( n / N ) )
142 129 138 139 140 141 syl22anc 
 |-  ( ( ph /\ ch ) -> 0 <_ ( n / N ) )
143 129 ltp1d 
 |-  ( ( ph /\ ch ) -> n < ( n + 1 ) )
144 ltdiv1 
 |-  ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
145 129 122 139 140 144 syl112anc 
 |-  ( ( ph /\ ch ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
146 143 145 mpbid 
 |-  ( ( ph /\ ch ) -> ( n / N ) < ( ( n + 1 ) / N ) )
147 130 124 146 ltled 
 |-  ( ( ph /\ ch ) -> ( n / N ) <_ ( ( n + 1 ) / N ) )
148 elicc2 
 |-  ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) <-> ( ( n / N ) e. RR /\ 0 <_ ( n / N ) /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) ) )
149 116 124 148 sylancr 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) <-> ( ( n / N ) e. RR /\ 0 <_ ( n / N ) /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) ) )
150 130 142 147 149 mpbir3and 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) )
151 iccsplit 
 |-  ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR /\ ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
152 136 124 150 151 syl3anc 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
153 135 152 sseqtrrid 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
154 uniretop 
 |-  RR = U. ( topGen ` ran (,) )
155 11 unieqi 
 |-  U. L = U. ( topGen ` ran (,) )
156 154 155 eqtr4i 
 |-  RR = U. L
157 156 restcldi 
 |-  ( ( ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR /\ ( 0 [,] ( n / N ) ) e. ( Clsd ` L ) /\ ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
158 126 134 153 157 syl3anc 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
159 icccld 
 |-  ( ( ( n / N ) e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
160 130 124 159 syl2anc 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
161 160 133 eleqtrrdi 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` L ) )
162 ssun2 
 |-  ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
163 162 152 sseqtrrid 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
164 156 restcldi 
 |-  ( ( ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` L ) /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
165 126 161 163 164 syl3anc 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
166 retop 
 |-  ( topGen ` ran (,) ) e. Top
167 11 166 eqeltri 
 |-  L e. Top
168 156 restuni 
 |-  ( ( L e. Top /\ ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
169 167 126 168 sylancr 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
170 152 169 eqtr3d 
 |-  ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
171 14 simprbi 
 |-  ( ch -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
172 171 adantl 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) )
173 172 simpld 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) )
174 eqid 
 |-  U. ( L |`t ( 0 [,] ( n / N ) ) ) = U. ( L |`t ( 0 [,] ( n / N ) ) )
175 174 2 cnf 
 |-  ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L |`t ( 0 [,] ( n / N ) ) ) --> B )
176 173 175 syl 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L |`t ( 0 [,] ( n / N ) ) ) --> B )
177 iccssre 
 |-  ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) C_ RR )
178 116 130 177 sylancr 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ RR )
179 156 restuni 
 |-  ( ( L e. Top /\ ( 0 [,] ( n / N ) ) C_ RR ) -> ( 0 [,] ( n / N ) ) = U. ( L |`t ( 0 [,] ( n / N ) ) ) )
180 167 178 179 sylancr 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) = U. ( L |`t ( 0 [,] ( n / N ) ) ) )
181 180 feq2d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B <-> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L |`t ( 0 [,] ( n / N ) ) ) --> B ) )
182 176 181 mpbird 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B )
183 eqid 
 |-  ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) )
184 simpr 
 |-  ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( n + 1 ) e. ( 1 ... N ) )
185 1 2 3 4 5 6 7 8 9 10 11 12 183 cvmliftlem7 
 |-  ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } ) )
186 1 2 3 4 5 6 7 8 9 10 11 12 183 184 185 cvmliftlem6 
 |-  ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
187 119 186 syldan 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
188 187 simpld 
 |-  ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B )
189 128 nncnd 
 |-  ( ( ph /\ ch ) -> n e. CC )
190 ax-1cn 
 |-  1 e. CC
191 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
192 189 190 191 sylancl 
 |-  ( ( ph /\ ch ) -> ( ( n + 1 ) - 1 ) = n )
193 192 oveq1d 
 |-  ( ( ph /\ ch ) -> ( ( ( n + 1 ) - 1 ) / N ) = ( n / N ) )
194 193 oveq1d 
 |-  ( ( ph /\ ch ) -> ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
195 194 feq2d 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B <-> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B ) )
196 188 195 mpbid 
 |-  ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B )
197 176 ffund 
 |-  ( ( ph /\ ch ) -> Fun U_ k e. ( 1 ... n ) ( Q ` k ) )
198 128 109 syl 
 |-  ( ( ph /\ ch ) -> n e. ( ZZ>= ` 1 ) )
199 eluzfz2 
 |-  ( n e. ( ZZ>= ` 1 ) -> n e. ( 1 ... n ) )
200 198 199 syl 
 |-  ( ( ph /\ ch ) -> n e. ( 1 ... n ) )
201 fveq2 
 |-  ( k = n -> ( Q ` k ) = ( Q ` n ) )
202 201 ssiun2s 
 |-  ( n e. ( 1 ... n ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
203 200 202 syl 
 |-  ( ( ph /\ ch ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
204 peano2rem 
 |-  ( n e. RR -> ( n - 1 ) e. RR )
205 129 204 syl 
 |-  ( ( ph /\ ch ) -> ( n - 1 ) e. RR )
206 205 123 nndivred 
 |-  ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR )
207 206 rexrd 
 |-  ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR* )
208 130 rexrd 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. RR* )
209 129 ltm1d 
 |-  ( ( ph /\ ch ) -> ( n - 1 ) < n )
210 ltdiv1 
 |-  ( ( ( n - 1 ) e. RR /\ n e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
211 205 129 139 140 210 syl112anc 
 |-  ( ( ph /\ ch ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
212 209 211 mpbid 
 |-  ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) < ( n / N ) )
213 206 130 212 ltled 
 |-  ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) <_ ( n / N ) )
214 ubicc2 
 |-  ( ( ( ( n - 1 ) / N ) e. RR* /\ ( n / N ) e. RR* /\ ( ( n - 1 ) / N ) <_ ( n / N ) ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
215 207 208 213 214 syl3anc 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
216 198 119 111 syl2anc 
 |-  ( ( ph /\ ch ) -> n e. ( 1 ... N ) )
217 eqid 
 |-  ( ( ( n - 1 ) / N ) [,] ( n / N ) ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) )
218 simpr 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
219 1 2 3 4 5 6 7 8 9 10 11 12 217 cvmliftlem7 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` ( n - 1 ) ) ` ( ( n - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n - 1 ) / N ) ) } ) )
220 1 2 3 4 5 6 7 8 9 10 11 12 217 218 219 cvmliftlem6 
 |-  ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
221 216 220 syldan 
 |-  ( ( ph /\ ch ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
222 221 simpld 
 |-  ( ( ph /\ ch ) -> ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B )
223 222 fdmd 
 |-  ( ( ph /\ ch ) -> dom ( Q ` n ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
224 215 223 eleqtrrd 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. dom ( Q ` n ) )
225 funssfv 
 |-  ( ( Fun U_ k e. ( 1 ... n ) ( Q ` k ) /\ ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) /\ ( n / N ) e. dom ( Q ` n ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
226 197 203 224 225 syl3anc 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
227 192 fveq2d 
 |-  ( ( ph /\ ch ) -> ( Q ` ( ( n + 1 ) - 1 ) ) = ( Q ` n ) )
228 227 193 fveq12d 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
229 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem9 
 |-  ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
230 119 229 syldan 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
231 193 fveq2d 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
232 230 231 eqtr3d 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
233 226 228 232 3eqtr2d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
234 233 opeq2d 
 |-  ( ( ph /\ ch ) -> <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. = <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. )
235 234 sneqd 
 |-  ( ( ph /\ ch ) -> { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
236 182 ffnd 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) )
237 0xr 
 |-  0 e. RR*
238 237 a1i 
 |-  ( ( ph /\ ch ) -> 0 e. RR* )
239 ubicc2 
 |-  ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ 0 <_ ( n / N ) ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
240 238 208 142 239 syl3anc 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
241 fnressn 
 |-  ( ( U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) /\ ( n / N ) e. ( 0 [,] ( n / N ) ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } )
242 236 240 241 syl2anc 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } )
243 196 ffnd 
 |-  ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
244 124 rexrd 
 |-  ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR* )
245 lbicc2 
 |-  ( ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
246 208 244 147 245 syl3anc 
 |-  ( ( ph /\ ch ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
247 fnressn 
 |-  ( ( ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) /\ ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) -> ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
248 243 246 247 syl2anc 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
249 235 242 248 3eqtr4d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
250 df-icc 
 |-  [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
251 xrmaxle 
 |-  ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ z e. RR* ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) <_ z <-> ( 0 <_ z /\ ( n / N ) <_ z ) ) )
252 xrlemin 
 |-  ( ( z e. RR* /\ ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* ) -> ( z <_ if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) <-> ( z <_ ( n / N ) /\ z <_ ( ( n + 1 ) / N ) ) ) )
253 250 251 252 ixxin 
 |-  ( ( ( 0 e. RR* /\ ( n / N ) e. RR* ) /\ ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* ) ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) )
254 238 208 208 244 253 syl22anc 
 |-  ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) )
255 142 iftrued 
 |-  ( ( ph /\ ch ) -> if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) = ( n / N ) )
256 147 iftrued 
 |-  ( ( ph /\ ch ) -> if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) = ( n / N ) )
257 255 256 oveq12d 
 |-  ( ( ph /\ ch ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) = ( ( n / N ) [,] ( n / N ) ) )
258 iccid 
 |-  ( ( n / N ) e. RR* -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
259 208 258 syl 
 |-  ( ( ph /\ ch ) -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
260 254 257 259 3eqtrd 
 |-  ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = { ( n / N ) } )
261 260 reseq2d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) )
262 260 reseq2d 
 |-  ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
263 249 261 262 3eqtr4d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
264 fresaun 
 |-  ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
265 182 196 263 264 syl3anc 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
266 fzsuc 
 |-  ( n e. ( ZZ>= ` 1 ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
267 198 266 syl 
 |-  ( ( ph /\ ch ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
268 267 iuneq1d 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) = U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) )
269 iunxun 
 |-  U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. U_ k e. { ( n + 1 ) } ( Q ` k ) )
270 ovex 
 |-  ( n + 1 ) e. _V
271 fveq2 
 |-  ( k = ( n + 1 ) -> ( Q ` k ) = ( Q ` ( n + 1 ) ) )
272 270 271 iunxsn 
 |-  U_ k e. { ( n + 1 ) } ( Q ` k ) = ( Q ` ( n + 1 ) )
273 272 uneq2i 
 |-  ( U_ k e. ( 1 ... n ) ( Q ` k ) u. U_ k e. { ( n + 1 ) } ( Q ` k ) ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) )
274 269 273 eqtri 
 |-  U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) )
275 268 274 eqtr2di 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
276 275 feq1d 
 |-  ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B ) )
277 265 276 mpbid 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
278 170 feq2d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B <-> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) --> B ) )
279 277 278 mpbid 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : U. ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) --> B )
280 275 reseq1d 
 |-  ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) )
281 fresaunres1 
 |-  ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
282 182 196 263 281 syl3anc 
 |-  ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
283 280 282 eqtr3d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
284 167 a1i 
 |-  ( ( ph /\ ch ) -> L e. Top )
285 ovex 
 |-  ( 0 [,] ( ( n + 1 ) / N ) ) e. _V
286 285 a1i 
 |-  ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) e. _V )
287 restabs 
 |-  ( ( L e. Top /\ ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) /\ ( 0 [,] ( ( n + 1 ) / N ) ) e. _V ) -> ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( 0 [,] ( n / N ) ) ) = ( L |`t ( 0 [,] ( n / N ) ) ) )
288 284 153 286 287 syl3anc 
 |-  ( ( ph /\ ch ) -> ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( 0 [,] ( n / N ) ) ) = ( L |`t ( 0 [,] ( n / N ) ) ) )
289 288 oveq1d 
 |-  ( ( ph /\ ch ) -> ( ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( 0 [,] ( n / N ) ) ) Cn C ) = ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) )
290 173 283 289 3eltr4d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) e. ( ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( 0 [,] ( n / N ) ) ) Cn C ) )
291 1 2 3 4 5 6 7 8 9 10 11 12 183 cvmliftlem8 
 |-  ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( Q ` ( n + 1 ) ) e. ( ( L |`t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
292 119 291 syldan 
 |-  ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L |`t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
293 194 oveq2d 
 |-  ( ( ph /\ ch ) -> ( L |`t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
294 293 oveq1d 
 |-  ( ( ph /\ ch ) -> ( ( L |`t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) = ( ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
295 292 294 eleqtrd 
 |-  ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
296 275 reseq1d 
 |-  ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
297 fresaunres2 
 |-  ( ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B /\ ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
298 182 196 263 297 syl3anc 
 |-  ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
299 296 298 eqtr3d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
300 restabs 
 |-  ( ( L e. Top /\ ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) /\ ( 0 [,] ( ( n + 1 ) / N ) ) e. _V ) -> ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
301 284 163 286 300 syl3anc 
 |-  ( ( ph /\ ch ) -> ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
302 301 oveq1d 
 |-  ( ( ph /\ ch ) -> ( ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) = ( ( L |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
303 295 299 302 3eltr4d 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) e. ( ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) |`t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
304 115 2 158 165 170 279 290 303 paste 
 |-  ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
305 152 reseq2d 
 |-  ( ( ph /\ ch ) -> ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
306 172 simprd 
 |-  ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
307 187 simprd 
 |-  ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) )
308 194 reseq2d 
 |-  ( ( ph /\ ch ) -> ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
309 307 308 eqtrd 
 |-  ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
310 306 309 uneq12d 
 |-  ( ( ph /\ ch ) -> ( ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) u. ( F o. ( Q ` ( n + 1 ) ) ) ) = ( ( G |` ( 0 [,] ( n / N ) ) ) u. ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
311 coundi 
 |-  ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) u. ( F o. ( Q ` ( n + 1 ) ) ) )
312 resundi 
 |-  ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( G |` ( 0 [,] ( n / N ) ) ) u. ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
313 310 311 312 3eqtr4g 
 |-  ( ( ph /\ ch ) -> ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
314 275 coeq2d 
 |-  ( ( ph /\ ch ) -> ( F o. ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) ) = ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) )
315 305 313 314 3eqtr2rd 
 |-  ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
316 304 315 jca 
 |-  ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
317 14 316 sylan2br 
 |-  ( ( ph /\ ( ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) /\ ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
318 317 expr 
 |-  ( ( ph /\ ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) )
319 114 318 animpimp2impd 
 |-  ( n e. NN -> ( ( ph -> ( n e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( n / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) ) ) ) -> ( ph -> ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L |`t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) /\ ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) ) ) ) ) )
320 40 54 68 83 107 319 nnind 
 |-  ( N e. NN -> ( ph -> ( N e. ( 1 ... N ) -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) ) )
321 8 320 mpcom 
 |-  ( ph -> ( N e. ( 1 ... N ) -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) ) )
322 18 321 mpd 
 |-  ( ph -> ( K e. ( ( L |`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )