Theorem cvmliftlem10 24942

Description: Lemma for cvmlift 24947. 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 24938, cvmliftlem7 24939 (to show it is a function and a lift), cvmliftlem8 24940 (to show it is continuous), and cvmliftlem9 24941 (to show that different Q functions agree on the intersection of their domains, so that the pasting lemma paste 17320 gives that K is well-defined and continuous). (Contributed by Mario Carneiro, 14-Feb-2015.)

Hypotheses

Ref	Expression
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

Ref	Expression
cvmliftlem10	|- ( ph -> ( K e. ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )

Distinct variable groups:   v, b, z, B   j, b, k, m, n, s, u, x, F, v, z   n, L, z   P, b, k, m, n, u, v, x, z   C, b, j, k, n, s, u, v, z   ph, j, n, s, x, z   N, b, k, m, n, u, v, x, z   S, b, j, k, n, s, u, v, x, z   j, X   G, b, j, k, m, n, s, u, v, x, z   T, b, j, k, m, s, u, v, x, z   J, b, j, k, n, s, u, v, x, z   Q, b, k, m, n, u, v, x, z

Allowed substitution hints:   ph( v, u, k, m, b)   ch( x, z, v, u, j, k, m, n, s, b)   B( x, u, j, k, m, n, s)   C( x, m)   P( j, s)   Q( j, s)   S( m)   T( n)   J( m)   K( x, z, v, u, j, k, m, n, s, b)   L( x, v, u, j, k, m, s, b)   N( j, s)   X( x, z, v, u, k, m, n, s, b)

Proof of Theorem cvmliftlem10

Dummy variable y is distinct from all other variables.

Step	Hyp	Ref	Expression
1		cvmliftlem.n	. . . 4 |- ( ph -> N e. NN )
2		nnuz 10485	. . . 4 |- NN = ( ZZ>= ` 1 )
3	1, 2	syl6eleq 2502	. . 3 |- ( ph -> N e. ( ZZ>= ` 1 ) )
4		eluzfz2 11029	. . 3 |- ( N e. ( ZZ>= ` 1 ) -> N e. ( 1 ... N ) )
5	3, 4	syl 16	. 2 |- ( ph -> N e. ( 1 ... N ) )
6		eleq1 2472	. . . . . 6 |- ( y = 1 -> ( y e. ( 1 ... N ) <-> 1 e. ( 1 ... N ) ) )
7		oveq2 6056	. . . . . . . . . . 11 |- ( y = 1 -> ( 1 ... y ) = ( 1 ... 1 ) )
8		1z 10275	. . . . . . . . . . . 12 |- 1 e. ZZ
9		fzsn 11058	. . . . . . . . . . . 12 |- ( 1 e. ZZ -> ( 1 ... 1 ) = { 1 } )
10	8, 9	ax-mp 8	. . . . . . . . . . 11 |- ( 1 ... 1 ) = { 1 }
11	7, 10	syl6eq 2460	. . . . . . . . . 10 |- ( y = 1 -> ( 1 ... y ) = { 1 } )
12	11	iuneq1d 4084	. . . . . . . . 9 |- ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. { 1 } ( Q ` k ) )
13		1ex 9050	. . . . . . . . . 10 |- 1 e. _V
14		fveq2 5695	. . . . . . . . . 10 |- ( k = 1 -> ( Q ` k ) = ( Q ` 1 ) )
15	13, 14	iunxsn 4138	. . . . . . . . 9 |- U_ k e. { 1 } ( Q ` k ) = ( Q ` 1 )
16	12, 15	syl6eq 2460	. . . . . . . 8 |- ( y = 1 -> U_ k e. ( 1 ... y ) ( Q ` k ) = ( Q ` 1 ) )
17		oveq1 6055	. . . . . . . . . . 11 |- ( y = 1 -> ( y / N ) = ( 1 / N ) )
18	17	oveq2d 6064	. . . . . . . . . 10 |- ( y = 1 -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( 1 / N ) ) )
19	18	oveq2d 6064	. . . . . . . . 9 |- ( y = 1 -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( 1 / N ) ) ) )
20	19	oveq1d 6063	. . . . . . . 8 |- ( y = 1 -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
21	16, 20	eleq12d 2480	. . . . . . 7 |- ( 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 ) ) )
22	16	coeq2d 5002	. . . . . . . 8 |- ( y = 1 -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. ( Q ` 1 ) ) )
23	18	reseq2d 5113	. . . . . . . 8 |- ( y = 1 -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
24	22, 23	eqeq12d 2426	. . . . . . 7 |- ( y = 1 -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
25	21, 24	anbi12d 692	. . . . . 6 |- ( 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 ) ) ) ) ) )
26	6, 25	imbi12d 312	. . . . 5 |- ( 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 ) ) ) ) ) ) )
27	26	imbi2d 308	. . . 4 |- ( 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 ) ) ) ) ) ) ) )
28		eleq1 2472	. . . . . 6 |- ( y = n -> ( y e. ( 1 ... N ) <-> n e. ( 1 ... N ) ) )
29		oveq2 6056	. . . . . . . . 9 |- ( y = n -> ( 1 ... y ) = ( 1 ... n ) )
30	29	iuneq1d 4084	. . . . . . . 8 |- ( y = n -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
31		oveq1 6055	. . . . . . . . . . 11 |- ( y = n -> ( y / N ) = ( n / N ) )
32	31	oveq2d 6064	. . . . . . . . . 10 |- ( y = n -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( n / N ) ) )
33	32	oveq2d 6064	. . . . . . . . 9 |- ( y = n -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( n / N ) ) ) )
34	33	oveq1d 6063	. . . . . . . 8 |- ( y = n -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
35	30, 34	eleq12d 2480	. . . . . . 7 |- ( 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 ) ) )
36	30	coeq2d 5002	. . . . . . . 8 |- ( y = n -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) )
37	32	reseq2d 5113	. . . . . . . 8 |- ( y = n -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
38	36, 37	eqeq12d 2426	. . . . . . 7 |- ( 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 ) ) ) ) )
39	35, 38	anbi12d 692	. . . . . 6 |- ( 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 ) ) ) ) ) )
40	28, 39	imbi12d 312	. . . . 5 |- ( 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 ) ) ) ) ) ) )
41	40	imbi2d 308	. . . 4 |- ( 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 ) ) ) ) ) ) ) )
42		eleq1 2472	. . . . . 6 |- ( y = ( n + 1 ) -> ( y e. ( 1 ... N ) <-> ( n + 1 ) e. ( 1 ... N ) ) )
43		oveq2 6056	. . . . . . . . 9 |- ( y = ( n + 1 ) -> ( 1 ... y ) = ( 1 ... ( n + 1 ) ) )
44	43	iuneq1d 4084	. . . . . . . 8 |- ( y = ( n + 1 ) -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
45		oveq1 6055	. . . . . . . . . . 11 |- ( y = ( n + 1 ) -> ( y / N ) = ( ( n + 1 ) / N ) )
46	45	oveq2d 6064	. . . . . . . . . 10 |- ( y = ( n + 1 ) -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( ( n + 1 ) / N ) ) )
47	46	oveq2d 6064	. . . . . . . . 9 |- ( y = ( n + 1 ) -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
48	47	oveq1d 6063	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
49	44, 48	eleq12d 2480	. . . . . . 7 |- ( 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 ) ) )
50	44	coeq2d 5002	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) )
51	46	reseq2d 5113	. . . . . . . 8 |- ( y = ( n + 1 ) -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
52	50, 51	eqeq12d 2426	. . . . . . 7 |- ( 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 ) ) ) ) )
53	49, 52	anbi12d 692	. . . . . 6 |- ( 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 ) ) ) ) ) )
54	42, 53	imbi12d 312	. . . . 5 |- ( 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 ) ) ) ) ) ) )
55	54	imbi2d 308	. . . 4 |- ( 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 ) ) ) ) ) ) ) )
56		eleq1 2472	. . . . . 6 |- ( y = N -> ( y e. ( 1 ... N ) <-> N e. ( 1 ... N ) ) )
57		oveq2 6056	. . . . . . . . . 10 |- ( y = N -> ( 1 ... y ) = ( 1 ... N ) )
58	57	iuneq1d 4084	. . . . . . . . 9 |- ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = U_ k e. ( 1 ... N ) ( Q ` k ) )
59		cvmliftlem.k	. . . . . . . . 9 |- K = U_ k e. ( 1 ... N ) ( Q ` k )
60	58, 59	syl6eqr 2462	. . . . . . . 8 |- ( y = N -> U_ k e. ( 1 ... y ) ( Q ` k ) = K )
61		oveq1 6055	. . . . . . . . . . 11 |- ( y = N -> ( y / N ) = ( N / N ) )
62	61	oveq2d 6064	. . . . . . . . . 10 |- ( y = N -> ( 0 [,] ( y / N ) ) = ( 0 [,] ( N / N ) ) )
63	62	oveq2d 6064	. . . . . . . . 9 |- ( y = N -> ( L ↾t ( 0 [,] ( y / N ) ) ) = ( L ↾t ( 0 [,] ( N / N ) ) ) )
64	63	oveq1d 6063	. . . . . . . 8 |- ( y = N -> ( ( L ↾t ( 0 [,] ( y / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( N / N ) ) ) Cn C ) )
65	60, 64	eleq12d 2480	. . . . . . 7 |- ( 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 ) ) )
66	60	coeq2d 5002	. . . . . . . 8 |- ( y = N -> ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( F o. K ) )
67	62	reseq2d 5113	. . . . . . . 8 |- ( y = N -> ( G |` ( 0 [,] ( y / N ) ) ) = ( G |` ( 0 [,] ( N / N ) ) ) )
68	66, 67	eqeq12d 2426	. . . . . . 7 |- ( y = N -> ( ( F o. U_ k e. ( 1 ... y ) ( Q ` k ) ) = ( G |` ( 0 [,] ( y / N ) ) ) <-> ( F o. K ) = ( G |` ( 0 [,] ( N / N ) ) ) ) )
69	65, 68	anbi12d 692	. . . . . 6 |- ( 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 ) ) ) ) ) )
70	56, 69	imbi12d 312	. . . . 5 |- ( 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 ) ) ) ) ) ) )
71	70	imbi2d 308	. . . 4 |- ( 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 ) ) ) ) ) ) ) )
72		eluzfz1 11028	. . . . . . . . 9 |- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
73	3, 72	syl 16	. . . . . . . 8 |- ( ph -> 1 e. ( 1 ... N ) )
74		cvmliftlem.1	. . . . . . . . 9 |- 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 ) ) ) ) } )
75		cvmliftlem.b	. . . . . . . . 9 |- B = U. C
76		cvmliftlem.x	. . . . . . . . 9 |- X = U. J
77		cvmliftlem.f	. . . . . . . . 9 |- ( ph -> F e. ( C CovMap J ) )
78		cvmliftlem.g	. . . . . . . . 9 |- ( ph -> G e. ( II Cn J ) )
79		cvmliftlem.p	. . . . . . . . 9 |- ( ph -> P e. B )
80		cvmliftlem.e	. . . . . . . . 9 |- ( ph -> ( F ` P ) = ( G ` 0 ) )
81		cvmliftlem.t	. . . . . . . . 9 |- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
82		cvmliftlem.a	. . . . . . . . 9 |- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
83		cvmliftlem.l	. . . . . . . . 9 |- L = ( topGen ` ran (,) )
84		cvmliftlem.q	. . . . . . . . 9 |- 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 >. } >. } ) )
85		eqid 2412	. . . . . . . . 9 |- ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) )
86	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem8 24940	. . . . . . . 8 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( Q ` 1 ) e. ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
87	73, 86	mpdan 650	. . . . . . 7 |- ( ph -> ( Q ` 1 ) e. ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) )
88		1m1e0 10032	. . . . . . . . . . . 12 |- ( 1 - 1 ) = 0
89	88	oveq1i 6058	. . . . . . . . . . 11 |- ( ( 1 - 1 ) / N ) = ( 0 / N )
90	1	nncnd 9980	. . . . . . . . . . . 12 |- ( ph -> N e. CC )
91	1	nnne0d 10008	. . . . . . . . . . . 12 |- ( ph -> N =/= 0 )
92	90, 91	div0d 9753	. . . . . . . . . . 11 |- ( ph -> ( 0 / N ) = 0 )
93	89, 92	syl5eq 2456	. . . . . . . . . 10 |- ( ph -> ( ( 1 - 1 ) / N ) = 0 )
94	93	oveq1d 6063	. . . . . . . . 9 |- ( ph -> ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( 0 [,] ( 1 / N ) ) )
95	94	oveq2d 6064	. . . . . . . 8 |- ( ph -> ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( L ↾t ( 0 [,] ( 1 / N ) ) ) )
96	95	oveq1d 6063	. . . . . . 7 |- ( ph -> ( ( L ↾t ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
97	87, 96	eleqtrd 2488	. . . . . 6 |- ( ph -> ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) )
98		simpr 448	. . . . . . . . . 10 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
99	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85	cvmliftlem7 24939	. . . . . . . . . 10 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( 1 - 1 ) / N ) ) } ) )
100	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 85, 98, 99	cvmliftlem6 24938	. . . . . . . . 9 |- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
101	73, 100	mpdan 650	. . . . . . . 8 |- ( ph -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
102	101	simprd 450	. . . . . . 7 |- ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) )
103	94	reseq2d 5113	. . . . . . 7 |- ( ph -> ( G |` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
104	102, 103	eqtrd 2444	. . . . . 6 |- ( ph -> ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) )
105	97, 104	jca 519	. . . . 5 |- ( ph -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) )
106	105	a1d 23	. . . 4 |- ( ph -> ( 1 e. ( 1 ... N ) -> ( ( Q ` 1 ) e. ( ( L ↾t ( 0 [,] ( 1 / N ) ) ) Cn C ) /\ ( F o. ( Q ` 1 ) ) = ( G |` ( 0 [,] ( 1 / N ) ) ) ) ) )
107		elnnuz 10486	. . . . . . . . . . 11 |- ( n e. NN <-> n e. ( ZZ>= ` 1 ) )
108	107	biimpi 187	. . . . . . . . . 10 |- ( n e. NN -> n e. ( ZZ>= ` 1 ) )
109	108	adantl 453	. . . . . . . . 9 |- ( ( ph /\ n e. NN ) -> n e. ( ZZ>= ` 1 ) )
110		peano2fzr 11033	. . . . . . . . . 10 |- ( ( n e. ( ZZ>= ` 1 ) /\ ( n + 1 ) e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
111	110	ex 424	. . . . . . . . 9 |- ( n e. ( ZZ>= ` 1 ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
112	109, 111	syl 16	. . . . . . . 8 |- ( ( ph /\ n e. NN ) -> ( ( n + 1 ) e. ( 1 ... N ) -> n e. ( 1 ... N ) ) )
113	112	imim1d 71	. . . . . . 7 |- ( ( 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 ) ) ) ) ) ) )
114		cvmliftlem10.1	. . . . . . . . . . 11 |- ( 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 ) ) ) ) ) )
115		eqid 2412	. . . . . . . . . . . . 13 |- U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) )
116		0re 9055	. . . . . . . . . . . . . . 15 |- 0 e. RR
117	114	simplbi 447	. . . . . . . . . . . . . . . . . . . 20 |- ( ch -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
118	117	adantl 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n e. NN /\ ( n + 1 ) e. ( 1 ... N ) ) )
119	118	simprd 450	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( n + 1 ) e. ( 1 ... N ) )
120		elfznn 11044	. . . . . . . . . . . . . . . . . 18 |- ( ( n + 1 ) e. ( 1 ... N ) -> ( n + 1 ) e. NN )
121	119, 120	syl 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( n + 1 ) e. NN )
122	121	nnred 9979	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n + 1 ) e. RR )
123	1	adantr 452	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> N e. NN )
124	122, 123	nndivred 10012	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR )
125		iccssre 10956	. . . . . . . . . . . . . . 15 |- ( ( 0 e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
126	116, 124, 125	sylancr 645	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) C_ RR )
127	117	simpld 446	. . . . . . . . . . . . . . . . . . 19 |- ( ch -> n e. NN )
128	127	adantl 453	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> n e. NN )
129	128	nnred 9979	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> n e. RR )
130	129, 123	nndivred 10012	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n / N ) e. RR )
131		icccld 18762	. . . . . . . . . . . . . . . 16 |- ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
132	116, 130, 131	sylancr 645	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
133	83	fveq2i 5698	. . . . . . . . . . . . . . 15 |- ( Clsd ` L ) = ( Clsd ` ( topGen ` ran (,) ) )
134	132, 133	syl6eleqr 2503	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` L ) )
135		ssun1 3478	. . . . . . . . . . . . . . 15 |- ( 0 [,] ( n / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
136	116	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> 0 e. RR )
137	128	nnnn0d 10238	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> n e. NN0 )
138	137	nn0ge0d 10241	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> 0 <_ n )
139	123	nnred 9979	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> N e. RR )
140	123	nngt0d 10007	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> 0 < N )
141		divge0 9843	. . . . . . . . . . . . . . . . . 18 |- ( ( ( n e. RR /\ 0 <_ n ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( n / N ) )
142	129, 138, 139, 140, 141	syl22anc 1185	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> 0 <_ ( n / N ) )
143	129	ltp1d 9905	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> n < ( n + 1 ) )
144		ltdiv1 9838	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 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 1188	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
146	143, 145	mpbid 202	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( n / N ) < ( ( n + 1 ) / N ) )
147	130, 124, 146	ltled 9185	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( n / N ) <_ ( ( n + 1 ) / N ) )
148		elicc2 10939	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 645	. . . . . . . . . . . . . . . . 17 |- ( ( 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 1137	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( ( n + 1 ) / N ) ) )
151		iccsplit 10993	. . . . . . . . . . . . . . . 16 |- ( ( 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 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
153	135, 152	syl5sseqr 3365	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
154		uniretop 18757	. . . . . . . . . . . . . . . 16 |- RR = U. ( topGen ` ran (,) )
155	83	unieqi 3993	. . . . . . . . . . . . . . . 16 |- U. L = U. ( topGen ` ran (,) )
156	154, 155	eqtr4i 2435	. . . . . . . . . . . . . . 15 |- RR = U. L
157	156	restcldi 17199	. . . . . . . . . . . . . 14 |- ( ( ( 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 1184	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
159		icccld 18762	. . . . . . . . . . . . . . . 16 |- ( ( ( n / N ) e. RR /\ ( ( n + 1 ) / N ) e. RR ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
160	130, 124, 159	syl2anc 643	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( topGen ` ran (,) ) ) )
161	160, 133	syl6eleqr 2503	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` L ) )
162		ssun2 3479	. . . . . . . . . . . . . . 15 |- ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
163	162, 152	syl5sseqr 3365	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) C_ ( 0 [,] ( ( n + 1 ) / N ) ) )
164	156	restcldi 17199	. . . . . . . . . . . . . 14 |- ( ( ( 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 1184	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( ( n + 1 ) / N ) ) e. ( Clsd ` ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ) )
166		retop 18756	. . . . . . . . . . . . . . . 16 |- ( topGen ` ran (,) ) e. Top
167	83, 166	eqeltri 2482	. . . . . . . . . . . . . . 15 |- L e. Top
168	156	restuni 17188	. . . . . . . . . . . . . . 15 |- ( ( 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 645	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
170	152, 169	eqtr3d 2446	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) )
171	114	simprbi 451	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 453	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 446	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
174		eqid 2412	. . . . . . . . . . . . . . . . . . 19 |- U. ( L ↾t ( 0 [,] ( n / N ) ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) )
175	174, 75	cnf 17272	. . . . . . . . . . . . . . . . . 18 |- ( 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 16	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( n / N ) ) ) --> B )
177		iccssre 10956	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR /\ ( n / N ) e. RR ) -> ( 0 [,] ( n / N ) ) C_ RR )
178	116, 130, 177	sylancr 645	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) C_ RR )
179	156	restuni 17188	. . . . . . . . . . . . . . . . . . 19 |- ( ( L e. Top /\ ( 0 [,] ( n / N ) ) C_ RR ) -> ( 0 [,] ( n / N ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) ) )
180	167, 178, 179	sylancr 645	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( 0 [,] ( n / N ) ) = U. ( L ↾t ( 0 [,] ( n / N ) ) ) )
181	180	feq2d 5548	. . . . . . . . . . . . . . . . 17 |- ( ( 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 224	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B )
183		eqid 2412	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) )
184		simpr 448	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( n + 1 ) e. ( 1 ... N ) )
185	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem7 24939	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } ) )
186	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183, 184, 185	cvmliftlem6 24938	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 457	. . . . . . . . . . . . . . . . . 18 |- ( ( 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 446	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B )
189	128	nncnd 9980	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> n e. CC )
190		ax-1cn 9012	. . . . . . . . . . . . . . . . . . . . 21 |- 1 e. CC
191		pncan 9275	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
192	189, 190, 191	sylancl 644	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( ( n + 1 ) - 1 ) = n )
193	192	oveq1d 6063	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( ( ( n + 1 ) - 1 ) / N ) = ( n / N ) )
194	193	oveq1d 6063	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
195	194	feq2d 5548	. . . . . . . . . . . . . . . . 17 |- ( ( 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 202	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B )
197		ffun 5560	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B -> Fun U_ k e. ( 1 ... n ) ( Q ` k ) )
198	182, 197	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> Fun U_ k e. ( 1 ... n ) ( Q ` k ) )
199	128, 108	syl 16	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> n e. ( ZZ>= ` 1 ) )
200		eluzfz2 11029	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( n e. ( ZZ>= ` 1 ) -> n e. ( 1 ... n ) )
201	199, 200	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> n e. ( 1 ... n ) )
202		fveq2 5695	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( k = n -> ( Q ` k ) = ( Q ` n ) )
203	202	ssiun2s 4103	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( n e. ( 1 ... n ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
204	201, 203	syl 16	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( Q ` n ) C_ U_ k e. ( 1 ... n ) ( Q ` k ) )
205		peano2rem 9331	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n e. RR -> ( n - 1 ) e. RR )
206	129, 205	syl 16	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( n - 1 ) e. RR )
207	206, 123	nndivred 10012	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR )
208	207	rexrd 9098	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) e. RR* )
209	130	rexrd 9098	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( n / N ) e. RR* )
210	129	ltm1d 9907	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( n - 1 ) < n )
211		ltdiv1 9838	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( n - 1 ) e. RR /\ n e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
212	206, 129, 139, 140, 211	syl112anc 1188	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> ( ( n - 1 ) < n <-> ( ( n - 1 ) / N ) < ( n / N ) ) )
213	210, 212	mpbid 202	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) < ( n / N ) )
214	207, 130, 213	ltled 9185	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( ( n - 1 ) / N ) <_ ( n / N ) )
215		ubicc2 10978	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( n - 1 ) / N ) e. RR* /\ ( n / N ) e. RR* /\ ( ( n - 1 ) / N ) <_ ( n / N ) ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
216	208, 209, 214, 215	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> ( n / N ) e. ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
217	199, 119, 110	syl2anc 643	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ ch ) -> n e. ( 1 ... N ) )
218		eqid 2412	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( n - 1 ) / N ) [,] ( n / N ) ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) )
219		simpr 448	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ n e. ( 1 ... N ) ) -> n e. ( 1 ... N ) )
220	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218	cvmliftlem7 24939	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` ( n - 1 ) ) ` ( ( n - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n - 1 ) / N ) ) } ) )
221	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 218, 219, 220	cvmliftlem6 24938	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ph /\ n e. ( 1 ... N ) ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
222	217, 221	syldan 457	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ph /\ ch ) -> ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B /\ ( F o. ( Q ` n ) ) = ( G |` ( ( ( n - 1 ) / N ) [,] ( n / N ) ) ) ) )
223	222	simpld 446	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ph /\ ch ) -> ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B )
224		fdm 5562	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( Q ` n ) : ( ( ( n - 1 ) / N ) [,] ( n / N ) ) --> B -> dom ( Q ` n ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
225	223, 224	syl 16	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ch ) -> dom ( Q ` n ) = ( ( ( n - 1 ) / N ) [,] ( n / N ) ) )
226	216, 225	eleqtrrd 2489	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( n / N ) e. dom ( Q ` n ) )
227		funssfv 5713	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( 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 ) ) )
228	198, 204, 226, 227	syl3anc 1184	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
229	192	fveq2d 5699	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( Q ` ( ( n + 1 ) - 1 ) ) = ( Q ` n ) )
230	229, 193	fveq12d 5701	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
231	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84	cvmliftlem9 24941	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
232	119, 231	syldan 457	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) )
233	193	fveq2d 5699	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
234	232, 233	eqtr3d 2446	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ph /\ ch ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
235	228, 230, 234	3eqtr2d 2450	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) )
236	235	opeq2d 3959	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. = <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. )
237	236	sneqd 3795	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
238		ffn 5558	. . . . . . . . . . . . . . . . . . . 20 |- ( U_ k e. ( 1 ... n ) ( Q ` k ) : ( 0 [,] ( n / N ) ) --> B -> U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) )
239	182, 238	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... n ) ( Q ` k ) Fn ( 0 [,] ( n / N ) ) )
240		0xr 9095	. . . . . . . . . . . . . . . . . . . . 21 |- 0 e. RR*
241	240	a1i 11	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> 0 e. RR* )
242		ubicc2 10978	. . . . . . . . . . . . . . . . . . . 20 |- ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ 0 <_ ( n / N ) ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
243	241, 209, 142, 242	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n / N ) e. ( 0 [,] ( n / N ) ) )
244		fnressn 5885	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) >. } )
245	239, 243, 244	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = { <. ( n / N ) , ( U_ k e. ( 1 ... n ) ( Q ` k ) ` ( n / N ) ) >. } )
246		ffn 5558	. . . . . . . . . . . . . . . . . . . 20 |- ( ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B -> ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
247	196, 246	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) Fn ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
248	124	rexrd 9098	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> ( ( n + 1 ) / N ) e. RR* )
249		lbicc2 10977	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
250	209, 248, 147, 249	syl3anc 1184	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( n / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
251		fnressn 5885	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( 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 ) ) >. } )
252	247, 250, 251	syl2anc 643	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) = { <. ( n / N ) , ( ( Q ` ( n + 1 ) ) ` ( n / N ) ) >. } )
253	237, 245, 252	3eqtr4d 2454	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) |` { ( n / N ) } ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
254		df-icc 10887	. . . . . . . . . . . . . . . . . . . . 21 |- [,] = ( x e. RR* , y e. RR* |-> { z e. RR* | ( x <_ z /\ z <_ y ) } )
255		xrmaxle 10735	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 0 e. RR* /\ ( n / N ) e. RR* /\ z e. RR* ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) <_ z <-> ( 0 <_ z /\ ( n / N ) <_ z ) ) )
256		xrlemin 10736	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( 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 ) ) ) )
257	254, 255, 256	ixxin 10897	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) ) ) )
258	241, 209, 209, 248, 257	syl22anc 1185	. . . . . . . . . . . . . . . . . . 19 |- ( ( 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 ) ) ) )
259		iftrue 3713	. . . . . . . . . . . . . . . . . . . . 21 |- ( 0 <_ ( n / N ) -> if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) = ( n / N ) )
260	142, 259	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) = ( n / N ) )
261		iftrue 3713	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( n / N ) <_ ( ( n + 1 ) / N ) -> if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) = ( n / N ) )
262	147, 261	syl 16	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ph /\ ch ) -> if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) = ( n / N ) )
263	260, 262	oveq12d 6066	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( if ( 0 <_ ( n / N ) , ( n / N ) , 0 ) [,] if ( ( n / N ) <_ ( ( n + 1 ) / N ) , ( n / N ) , ( ( n + 1 ) / N ) ) ) = ( ( n / N ) [,] ( n / N ) ) )
264		iccid 10925	. . . . . . . . . . . . . . . . . . . 20 |- ( ( n / N ) e. RR* -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
265	209, 264	syl 16	. . . . . . . . . . . . . . . . . . 19 |- ( ( ph /\ ch ) -> ( ( n / N ) [,] ( n / N ) ) = { ( n / N ) } )
266	258, 263, 265	3eqtrd 2448	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = { ( n / N ) } )
267	266	reseq2d 5113	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) } ) )
268	266	reseq2d 5113	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> ( ( Q ` ( n + 1 ) ) |` ( ( 0 [,] ( n / N ) ) i^i ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( Q ` ( n + 1 ) ) |` { ( n / N ) } ) )
269	253, 267, 268	3eqtr4d 2454	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) ) )
270		fresaun 5581	. . . . . . . . . . . . . . . 16 |- ( ( 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 )
271	182, 196, 269, 270	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
272		fzsuc 11060	. . . . . . . . . . . . . . . . . . 19 |- ( n e. ( ZZ>= ` 1 ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
273	199, 272	syl 16	. . . . . . . . . . . . . . . . . 18 |- ( ( ph /\ ch ) -> ( 1 ... ( n + 1 ) ) = ( ( 1 ... n ) u. { ( n + 1 ) } ) )
274	273	iuneq1d 4084	. . . . . . . . . . . . . . . . 17 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) = U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) )
275		iunxun 4140	. . . . . . . . . . . . . . . . . 18 |- 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 ) )
276		ovex 6073	. . . . . . . . . . . . . . . . . . . 20 |- ( n + 1 ) e. _V
277		fveq2 5695	. . . . . . . . . . . . . . . . . . . 20 |- ( k = ( n + 1 ) -> ( Q ` k ) = ( Q ` ( n + 1 ) ) )
278	276, 277	iunxsn 4138	. . . . . . . . . . . . . . . . . . 19 |- U_ k e. { ( n + 1 ) } ( Q ` k ) = ( Q ` ( n + 1 ) )
279	278	uneq2i 3466	. . . . . . . . . . . . . . . . . 18 |- ( 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 ) ) )
280	275, 279	eqtri 2432	. . . . . . . . . . . . . . . . 17 |- U_ k e. ( ( 1 ... n ) u. { ( n + 1 ) } ) ( Q ` k ) = ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) )
281	274, 280	syl6req 2461	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) = U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) )
282	281	feq1d 5547	. . . . . . . . . . . . . . 15 |- ( ( 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 ) )
283	271, 282	mpbid 202	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) --> B )
284	170	feq2d 5548	. . . . . . . . . . . . . 14 |- ( ( 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 ) )
285	283, 284	mpbid 202	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) : U. ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) --> B )
286	281	reseq1d 5112	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
287		fresaunres1 5583	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) )
288	182, 196, 269, 287	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
289	286, 288	eqtr3d 2446	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( 0 [,] ( n / N ) ) ) = U_ k e. ( 1 ... n ) ( Q ` k ) )
290	167	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> L e. Top )
291		ovex 6073	. . . . . . . . . . . . . . . . 17 |- ( 0 [,] ( ( n + 1 ) / N ) ) e. _V
292	291	a1i 11	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( 0 [,] ( ( n + 1 ) / N ) ) e. _V )
293		restabs 17191	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
294	290, 153, 292, 293	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) = ( L ↾t ( 0 [,] ( n / N ) ) ) )
295	294	oveq1d 6063	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( 0 [,] ( n / N ) ) ) Cn C ) = ( ( L ↾t ( 0 [,] ( n / N ) ) ) Cn C ) )
296	173, 289, 295	3eltr4d 2493	. . . . . . . . . . . . 13 |- ( ( 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 ) )
297	74, 75, 76, 77, 78, 79, 80, 1, 81, 82, 83, 84, 183	cvmliftlem8 24940	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ( n + 1 ) e. ( 1 ... N ) ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
298	119, 297	syldan 457	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
299	194	oveq2d 6064	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
300	299	oveq1d 6063	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( L ↾t ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) = ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
301	298, 300	eleqtrd 2488	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( Q ` ( n + 1 ) ) e. ( ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
302	281	reseq1d 5112	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
303		fresaunres2 5582	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
304	182, 196, 269, 303	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( U_ k e. ( 1 ... n ) ( Q ` k ) u. ( Q ` ( n + 1 ) ) ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
305	302, 304	eqtr3d 2446	. . . . . . . . . . . . . 14 |- ( ( ph /\ ch ) -> ( U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( Q ` ( n + 1 ) ) )
306		restabs 17191	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) ) )
307	290, 163, 292, 306	syl3anc 1184	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) = ( L ↾t ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
308	307	oveq1d 6063	. . . . . . . . . . . . . 14 |- ( ( 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 ) )
309	301, 305, 308	3eltr4d 2493	. . . . . . . . . . . . 13 |- ( ( 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 ) )
310	115, 75, 158, 165, 170, 285, 296, 309	paste 17320	. . . . . . . . . . . 12 |- ( ( ph /\ ch ) -> U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) e. ( ( L ↾t ( 0 [,] ( ( n + 1 ) / N ) ) ) Cn C ) )
311	152	reseq2d 5113	. . . . . . . . . . . . 13 |- ( ( ph /\ ch ) -> ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) )
312	172	simprd 450	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... n ) ( Q ` k ) ) = ( G |` ( 0 [,] ( n / N ) ) ) )
313	187	simprd 450	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) )
314	194	reseq2d 5113	. . . . . . . . . . . . . . . 16 |- ( ( ph /\ ch ) -> ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
315	313, 314	eqtrd 2444	. . . . . . . . . . . . . . 15 |- ( ( ph /\ ch ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
316	312, 315	uneq12d 3470	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) )
317		coundi 5338	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
318		resundi 5127	. . . . . . . . . . . . . 14 |- ( G |` ( ( 0 [,] ( n / N ) ) u. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ) = ( ( G |` ( 0 [,] ( n / N ) ) ) u. ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
319	316, 317, 318	3eqtr4g 2469	. . . . . . . . . . . . 13 |- ( ( 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 ) ) ) ) )
320	281	coeq2d 5002	. . . . . . . . . . . . 13 |- ( ( 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 ) ) )
321	311, 319, 320	3eqtr2rd 2451	. . . . . . . . . . . 12 |- ( ( ph /\ ch ) -> ( F o. U_ k e. ( 1 ... ( n + 1 ) ) ( Q ` k ) ) = ( G |` ( 0 [,] ( ( n + 1 ) / N ) ) ) )
322	310, 321	jca 519	. . . . . . . . . . 11 |- ( ( 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 ) ) ) ) )
323	114, 322	sylan2br 463	. . . . . . . . . 10 |- ( ( 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 ) ) ) ) )
324	323	expr 599	. . . . . . . . 9 |- ( ( 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 ) ) ) ) ) )
325	324	expr 599	. . . . . . . 8 |- ( ( 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 ) ) ) ) ) ) )
326	325	a2d 24	. . . . . . 7 |- ( ( ph /\ n e. NN ) -> ( ( ( n + 1 ) e. ( 1 ... N ) -> ( U_ k e. ( 1 ... n ) ( Q ` k