Metamath Proof Explorer

Theorem cvmliftlem7

Description: Lemma for cvmlift . Prove by induction that every Q function is well-defined (we can immediately follow this theorem with cvmliftlem6 to show functionality and lifting of Q ). (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 >. } >. } ) )
cvmliftlem5.3 
|- W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
Assertion cvmliftlem7 
|- ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )

Proof

Step Hyp Ref Expression
1 cvmliftlem.1 
 |-  S = ( k e. J |-> { s e. ( ~P C \ { (/) } ) | ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F |` u ) e. ( ( C |`t u ) Homeo ( J |`t k ) ) ) ) } )
2 cvmliftlem.b 
 |-  B = U. C
3 cvmliftlem.x 
 |-  X = U. J
4 cvmliftlem.f 
 |-  ( ph -> F e. ( C CovMap J ) )
5 cvmliftlem.g 
 |-  ( ph -> G e. ( II Cn J ) )
6 cvmliftlem.p 
 |-  ( ph -> P e. B )
7 cvmliftlem.e 
 |-  ( ph -> ( F ` P ) = ( G ` 0 ) )
8 cvmliftlem.n 
 |-  ( ph -> N e. NN )
9 cvmliftlem.t 
 |-  ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
10 cvmliftlem.a 
 |-  ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
11 cvmliftlem.l 
 |-  L = ( topGen ` ran (,) )
12 cvmliftlem.q 
 |-  Q = seq 0 ( ( x e. _V , m e. NN |-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) |-> ( `' ( F |` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I |` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
13 cvmliftlem5.3 
 |-  W = ( ( ( M - 1 ) / N ) [,] ( M / N ) )
14 fzssp1 
 |-  ( 0 ... ( N - 1 ) ) C_ ( 0 ... ( ( N - 1 ) + 1 ) )
15 8 nncnd 
 |-  ( ph -> N e. CC )
16 15 adantr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> N e. CC )
17 ax-1cn 
 |-  1 e. CC
18 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
19 16 17 18 sylancl 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( N - 1 ) + 1 ) = N )
20 19 oveq2d 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 ... ( ( N - 1 ) + 1 ) ) = ( 0 ... N ) )
21 14 20 sseqtrid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( 0 ... ( N - 1 ) ) C_ ( 0 ... N ) )
22 simpr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> M e. ( 1 ... N ) )
23 elfzelz 
 |-  ( M e. ( 1 ... N ) -> M e. ZZ )
24 8 nnzd 
 |-  ( ph -> N e. ZZ )
25 elfzm1b 
 |-  ( ( M e. ZZ /\ N e. ZZ ) -> ( M e. ( 1 ... N ) <-> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
26 23 24 25 syl2anr 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M e. ( 1 ... N ) <-> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) ) )
27 22 26 mpbid 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. ( 0 ... ( N - 1 ) ) )
28 21 27 sseldd 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( M - 1 ) e. ( 0 ... N ) )
29 elfznn0 
 |-  ( ( M - 1 ) e. ( 0 ... N ) -> ( M - 1 ) e. NN0 )
30 29 adantl 
 |-  ( ( ph /\ ( M - 1 ) e. ( 0 ... N ) ) -> ( M - 1 ) e. NN0 )
31 eleq1 
 |-  ( y = 0 -> ( y e. ( 0 ... N ) <-> 0 e. ( 0 ... N ) ) )
32 fveq2 
 |-  ( y = 0 -> ( Q ` y ) = ( Q ` 0 ) )
33 oveq1 
 |-  ( y = 0 -> ( y / N ) = ( 0 / N ) )
34 32 33 fveq12d 
 |-  ( y = 0 -> ( ( Q ` y ) ` ( y / N ) ) = ( ( Q ` 0 ) ` ( 0 / N ) ) )
35 fvoveq1 
 |-  ( y = 0 -> ( G ` ( y / N ) ) = ( G ` ( 0 / N ) ) )
36 35 sneqd 
 |-  ( y = 0 -> { ( G ` ( y / N ) ) } = { ( G ` ( 0 / N ) ) } )
37 36 imaeq2d 
 |-  ( y = 0 -> ( `' F " { ( G ` ( y / N ) ) } ) = ( `' F " { ( G ` ( 0 / N ) ) } ) )
38 34 37 eleq12d 
 |-  ( y = 0 -> ( ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) <-> ( ( Q ` 0 ) ` ( 0 / N ) ) e. ( `' F " { ( G ` ( 0 / N ) ) } ) ) )
39 31 38 imbi12d 
 |-  ( y = 0 -> ( ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) <-> ( 0 e. ( 0 ... N ) -> ( ( Q ` 0 ) ` ( 0 / N ) ) e. ( `' F " { ( G ` ( 0 / N ) ) } ) ) ) )
40 39 imbi2d 
 |-  ( y = 0 -> ( ( ph -> ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) ) <-> ( ph -> ( 0 e. ( 0 ... N ) -> ( ( Q ` 0 ) ` ( 0 / N ) ) e. ( `' F " { ( G ` ( 0 / N ) ) } ) ) ) ) )
41 eleq1 
 |-  ( y = n -> ( y e. ( 0 ... N ) <-> n e. ( 0 ... N ) ) )
42 fveq2 
 |-  ( y = n -> ( Q ` y ) = ( Q ` n ) )
43 oveq1 
 |-  ( y = n -> ( y / N ) = ( n / N ) )
44 42 43 fveq12d 
 |-  ( y = n -> ( ( Q ` y ) ` ( y / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
45 fvoveq1 
 |-  ( y = n -> ( G ` ( y / N ) ) = ( G ` ( n / N ) ) )
46 45 sneqd 
 |-  ( y = n -> { ( G ` ( y / N ) ) } = { ( G ` ( n / N ) ) } )
47 46 imaeq2d 
 |-  ( y = n -> ( `' F " { ( G ` ( y / N ) ) } ) = ( `' F " { ( G ` ( n / N ) ) } ) )
48 44 47 eleq12d 
 |-  ( y = n -> ( ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) <-> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) )
49 41 48 imbi12d 
 |-  ( y = n -> ( ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) <-> ( n e. ( 0 ... N ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) )
50 49 imbi2d 
 |-  ( y = n -> ( ( ph -> ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) ) <-> ( ph -> ( n e. ( 0 ... N ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) ) )
51 eleq1 
 |-  ( y = ( n + 1 ) -> ( y e. ( 0 ... N ) <-> ( n + 1 ) e. ( 0 ... N ) ) )
52 fveq2 
 |-  ( y = ( n + 1 ) -> ( Q ` y ) = ( Q ` ( n + 1 ) ) )
53 oveq1 
 |-  ( y = ( n + 1 ) -> ( y / N ) = ( ( n + 1 ) / N ) )
54 52 53 fveq12d 
 |-  ( y = ( n + 1 ) -> ( ( Q ` y ) ` ( y / N ) ) = ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) )
55 fvoveq1 
 |-  ( y = ( n + 1 ) -> ( G ` ( y / N ) ) = ( G ` ( ( n + 1 ) / N ) ) )
56 55 sneqd 
 |-  ( y = ( n + 1 ) -> { ( G ` ( y / N ) ) } = { ( G ` ( ( n + 1 ) / N ) ) } )
57 56 imaeq2d 
 |-  ( y = ( n + 1 ) -> ( `' F " { ( G ` ( y / N ) ) } ) = ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) )
58 54 57 eleq12d 
 |-  ( y = ( n + 1 ) -> ( ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) <-> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) ) )
59 51 58 imbi12d 
 |-  ( y = ( n + 1 ) -> ( ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) <-> ( ( n + 1 ) e. ( 0 ... N ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) ) ) )
60 59 imbi2d 
 |-  ( y = ( n + 1 ) -> ( ( ph -> ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) ) <-> ( ph -> ( ( n + 1 ) e. ( 0 ... N ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) ) ) ) )
61 eleq1 
 |-  ( y = ( M - 1 ) -> ( y e. ( 0 ... N ) <-> ( M - 1 ) e. ( 0 ... N ) ) )
62 fveq2 
 |-  ( y = ( M - 1 ) -> ( Q ` y ) = ( Q ` ( M - 1 ) ) )
63 oveq1 
 |-  ( y = ( M - 1 ) -> ( y / N ) = ( ( M - 1 ) / N ) )
64 62 63 fveq12d 
 |-  ( y = ( M - 1 ) -> ( ( Q ` y ) ` ( y / N ) ) = ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) )
65 fvoveq1 
 |-  ( y = ( M - 1 ) -> ( G ` ( y / N ) ) = ( G ` ( ( M - 1 ) / N ) ) )
66 65 sneqd 
 |-  ( y = ( M - 1 ) -> { ( G ` ( y / N ) ) } = { ( G ` ( ( M - 1 ) / N ) ) } )
67 66 imaeq2d 
 |-  ( y = ( M - 1 ) -> ( `' F " { ( G ` ( y / N ) ) } ) = ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
68 64 67 eleq12d 
 |-  ( y = ( M - 1 ) -> ( ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) <-> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) ) )
69 61 68 imbi12d 
 |-  ( y = ( M - 1 ) -> ( ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) <-> ( ( M - 1 ) e. ( 0 ... N ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) ) ) )
70 69 imbi2d 
 |-  ( y = ( M - 1 ) -> ( ( ph -> ( y e. ( 0 ... N ) -> ( ( Q ` y ) ` ( y / N ) ) e. ( `' F " { ( G ` ( y / N ) ) } ) ) ) <-> ( ph -> ( ( M - 1 ) e. ( 0 ... N ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) ) ) ) )
71 1 2 3 4 5 6 7 8 9 10 11 12 cvmliftlem4 
 |-  ( Q ` 0 ) = { <. 0 , P >. }
72 71 a1i 
 |-  ( ph -> ( Q ` 0 ) = { <. 0 , P >. } )
73 8 nnne0d 
 |-  ( ph -> N =/= 0 )
74 15 73 div0d 
 |-  ( ph -> ( 0 / N ) = 0 )
75 72 74 fveq12d 
 |-  ( ph -> ( ( Q ` 0 ) ` ( 0 / N ) ) = ( { <. 0 , P >. } ` 0 ) )
76 0nn0 
 |-  0 e. NN0
77 fvsng 
 |-  ( ( 0 e. NN0 /\ P e. B ) -> ( { <. 0 , P >. } ` 0 ) = P )
78 76 6 77 sylancr 
 |-  ( ph -> ( { <. 0 , P >. } ` 0 ) = P )
79 75 78 eqtrd 
 |-  ( ph -> ( ( Q ` 0 ) ` ( 0 / N ) ) = P )
80 74 fveq2d 
 |-  ( ph -> ( G ` ( 0 / N ) ) = ( G ` 0 ) )
81 7 80 eqtr4d 
 |-  ( ph -> ( F ` P ) = ( G ` ( 0 / N ) ) )
82 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
83 4 82 syl 
 |-  ( ph -> F e. ( C Cn J ) )
84 2 3 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> X )
85 ffn 
 |-  ( F : B --> X -> F Fn B )
86 83 84 85 3syl 
 |-  ( ph -> F Fn B )
87 fniniseg 
 |-  ( F Fn B -> ( P e. ( `' F " { ( G ` ( 0 / N ) ) } ) <-> ( P e. B /\ ( F ` P ) = ( G ` ( 0 / N ) ) ) ) )
88 86 87 syl 
 |-  ( ph -> ( P e. ( `' F " { ( G ` ( 0 / N ) ) } ) <-> ( P e. B /\ ( F ` P ) = ( G ` ( 0 / N ) ) ) ) )
89 6 81 88 mpbir2and 
 |-  ( ph -> P e. ( `' F " { ( G ` ( 0 / N ) ) } ) )
90 79 89 eqeltrd 
 |-  ( ph -> ( ( Q ` 0 ) ` ( 0 / N ) ) e. ( `' F " { ( G ` ( 0 / N ) ) } ) )
91 90 a1d 
 |-  ( ph -> ( 0 e. ( 0 ... N ) -> ( ( Q ` 0 ) ` ( 0 / N ) ) e. ( `' F " { ( G ` ( 0 / N ) ) } ) ) )
92 id 
 |-  ( n e. NN0 -> n e. NN0 )
93 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
94 92 93 eleqtrdi 
 |-  ( n e. NN0 -> n e. ( ZZ>= ` 0 ) )
95 94 adantl 
 |-  ( ( ph /\ n e. NN0 ) -> n e. ( ZZ>= ` 0 ) )
96 peano2fzr 
 |-  ( ( n e. ( ZZ>= ` 0 ) /\ ( n + 1 ) e. ( 0 ... N ) ) -> n e. ( 0 ... N ) )
97 96 ex 
 |-  ( n e. ( ZZ>= ` 0 ) -> ( ( n + 1 ) e. ( 0 ... N ) -> n e. ( 0 ... N ) ) )
98 95 97 syl 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n + 1 ) e. ( 0 ... N ) -> n e. ( 0 ... N ) ) )
99 98 imim1d 
 |-  ( ( ph /\ n e. NN0 ) -> ( ( n e. ( 0 ... N ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) -> ( ( n + 1 ) e. ( 0 ... N ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) )
100 eqid 
 |-  ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) )
101 simprlr 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) e. ( 0 ... N ) )
102 elfzle2 
 |-  ( ( n + 1 ) e. ( 0 ... N ) -> ( n + 1 ) <_ N )
103 101 102 syl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) <_ N )
104 simprll 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> n e. NN0 )
105 nn0p1nn 
 |-  ( n e. NN0 -> ( n + 1 ) e. NN )
106 104 105 syl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) e. NN )
107 nnuz 
 |-  NN = ( ZZ>= ` 1 )
108 106 107 eleqtrdi 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) e. ( ZZ>= ` 1 ) )
109 24 adantr 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> N e. ZZ )
110 elfz5 
 |-  ( ( ( n + 1 ) e. ( ZZ>= ` 1 ) /\ N e. ZZ ) -> ( ( n + 1 ) e. ( 1 ... N ) <-> ( n + 1 ) <_ N ) )
111 108 109 110 syl2anc 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) e. ( 1 ... N ) <-> ( n + 1 ) <_ N ) )
112 103 111 mpbird 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) e. ( 1 ... N ) )
113 simprr 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) )
114 104 nn0cnd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> n e. CC )
115 pncan 
 |-  ( ( n e. CC /\ 1 e. CC ) -> ( ( n + 1 ) - 1 ) = n )
116 114 17 115 sylancl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) - 1 ) = n )
117 116 fveq2d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( Q ` ( ( n + 1 ) - 1 ) ) = ( Q ` n ) )
118 116 oveq1d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( ( n + 1 ) - 1 ) / N ) = ( n / N ) )
119 117 118 fveq12d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( ( Q ` n ) ` ( n / N ) ) )
120 118 fveq2d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) = ( G ` ( n / N ) ) )
121 120 sneqd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } = { ( G ` ( n / N ) ) } )
122 121 imaeq2d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( `' F " { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } ) = ( `' F " { ( G ` ( n / N ) ) } ) )
123 113 119 122 3eltr4d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` ( ( n + 1 ) - 1 ) ) ` ( ( ( n + 1 ) - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( ( n + 1 ) - 1 ) / N ) ) } ) )
124 1 2 3 4 5 6 7 8 9 10 11 12 100 112 123 cvmliftlem6 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / 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 ) ) ) ) )
125 124 simpld 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B )
126 104 nn0red 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> n e. RR )
127 8 adantr 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> N e. NN )
128 126 127 nndivred 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n / N ) e. RR )
129 128 rexrd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n / N ) e. RR* )
130 peano2re 
 |-  ( n e. RR -> ( n + 1 ) e. RR )
131 126 130 syl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n + 1 ) e. RR )
132 131 127 nndivred 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) / N ) e. RR )
133 132 rexrd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) / N ) e. RR* )
134 126 ltp1d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> n < ( n + 1 ) )
135 127 nnred 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> N e. RR )
136 127 nngt0d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> 0 < N )
137 ltdiv1 
 |-  ( ( n e. RR /\ ( n + 1 ) e. RR /\ ( N e. RR /\ 0 < N ) ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
138 126 131 135 136 137 syl112anc 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n < ( n + 1 ) <-> ( n / N ) < ( ( n + 1 ) / N ) ) )
139 134 138 mpbid 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n / N ) < ( ( n + 1 ) / N ) )
140 128 132 139 ltled 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( n / N ) <_ ( ( n + 1 ) / N ) )
141 ubicc2 
 |-  ( ( ( n / N ) e. RR* /\ ( ( n + 1 ) / N ) e. RR* /\ ( n / N ) <_ ( ( n + 1 ) / N ) ) -> ( ( n + 1 ) / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
142 129 133 140 141 syl3anc 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
143 118 oveq1d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) = ( ( n / N ) [,] ( ( n + 1 ) / N ) ) )
144 142 143 eleqtrrd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( n + 1 ) / N ) e. ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) )
145 125 144 ffvelrnd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. B )
146 124 simprd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) )
147 143 reseq2d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( G |` ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
148 146 147 eqtrd 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( F o. ( Q ` ( n + 1 ) ) ) = ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) )
149 148 fveq1d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( F o. ( Q ` ( n + 1 ) ) ) ` ( ( n + 1 ) / N ) ) = ( ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ` ( ( n + 1 ) / N ) ) )
150 143 feq2d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` ( n + 1 ) ) : ( ( ( ( n + 1 ) - 1 ) / N ) [,] ( ( n + 1 ) / N ) ) --> B <-> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B ) )
151 125 150 mpbid 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B )
152 fvco3 
 |-  ( ( ( Q ` ( n + 1 ) ) : ( ( n / N ) [,] ( ( n + 1 ) / N ) ) --> B /\ ( ( n + 1 ) / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) -> ( ( F o. ( Q ` ( n + 1 ) ) ) ` ( ( n + 1 ) / N ) ) = ( F ` ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) ) )
153 151 142 152 syl2anc 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( F o. ( Q ` ( n + 1 ) ) ) ` ( ( n + 1 ) / N ) ) = ( F ` ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) ) )
154 fvres 
 |-  ( ( ( n + 1 ) / N ) e. ( ( n / N ) [,] ( ( n + 1 ) / N ) ) -> ( ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ` ( ( n + 1 ) / N ) ) = ( G ` ( ( n + 1 ) / N ) ) )
155 142 154 syl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( G |` ( ( n / N ) [,] ( ( n + 1 ) / N ) ) ) ` ( ( n + 1 ) / N ) ) = ( G ` ( ( n + 1 ) / N ) ) )
156 149 153 155 3eqtr3d 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( F ` ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) ) = ( G ` ( ( n + 1 ) / N ) ) )
157 86 adantr 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> F Fn B )
158 fniniseg 
 |-  ( F Fn B -> ( ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) <-> ( ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) ) = ( G ` ( ( n + 1 ) / N ) ) ) ) )
159 157 158 syl 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) <-> ( ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. B /\ ( F ` ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) ) = ( G ` ( ( n + 1 ) / N ) ) ) ) )
160 145 156 159 mpbir2and 
 |-  ( ( ph /\ ( ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) /\ ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) )
161 160 expr 
 |-  ( ( ph /\ ( n e. NN0 /\ ( n + 1 ) e. ( 0 ... N ) ) ) -> ( ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) ) )
162 99 161 animpimp2impd 
 |-  ( n e. NN0 -> ( ( ph -> ( n e. ( 0 ... N ) -> ( ( Q ` n ) ` ( n / N ) ) e. ( `' F " { ( G ` ( n / N ) ) } ) ) ) -> ( ph -> ( ( n + 1 ) e. ( 0 ... N ) -> ( ( Q ` ( n + 1 ) ) ` ( ( n + 1 ) / N ) ) e. ( `' F " { ( G ` ( ( n + 1 ) / N ) ) } ) ) ) ) )
163 40 50 60 70 91 162 nn0ind 
 |-  ( ( M - 1 ) e. NN0 -> ( ph -> ( ( M - 1 ) e. ( 0 ... N ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) ) ) )
164 163 impd 
 |-  ( ( M - 1 ) e. NN0 -> ( ( ph /\ ( M - 1 ) e. ( 0 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) ) )
165 30 164 mpcom 
 |-  ( ( ph /\ ( M - 1 ) e. ( 0 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )
166 28 165 syldan 
 |-  ( ( ph /\ M e. ( 1 ... N ) ) -> ( ( Q ` ( M - 1 ) ) ` ( ( M - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( M - 1 ) / N ) ) } ) )