cvmliftlem11

	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 )
Assertion	cvmliftlem11	\|- ( ph -> ( K e. ( II Cn C ) /\ ( F o. K ) = G ) )

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		biid	\|- ( ( ( 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 ) ) ) ) ) <-> ( ( 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	1 2 3 4 5 6 7 8 9 10 11 12 13 14	cvmliftlem10	\|- ( ph -> ( K e. ( ( L \|`t ( 0 [,] ( N / N ) ) ) Cn C ) /\ ( F o. K ) = ( G \|` ( 0 [,] ( N / N ) ) ) ) )
16	15	simpld	\|- ( ph -> K e. ( ( L \|`t ( 0 [,] ( N / N ) ) ) Cn C ) )
17	11	a1i	\|- ( ph -> L = ( topGen ` ran (,) ) )
18	8	nncnd	\|- ( ph -> N e. CC )
19	8	nnne0d	\|- ( ph -> N =/= 0 )
20	18 19	dividd	\|- ( ph -> ( N / N ) = 1 )
21	20	oveq2d	\|- ( ph -> ( 0 [,] ( N / N ) ) = ( 0 [,] 1 ) )
22	17 21	oveq12d	\|- ( ph -> ( L \|`t ( 0 [,] ( N / N ) ) ) = ( ( topGen ` ran (,) ) \|`t ( 0 [,] 1 ) ) )
23		dfii2	\|- II = ( ( topGen ` ran (,) ) \|`t ( 0 [,] 1 ) )
24	22 23	eqtr4di	\|- ( ph -> ( L \|`t ( 0 [,] ( N / N ) ) ) = II )
25	24	oveq1d	\|- ( ph -> ( ( L \|`t ( 0 [,] ( N / N ) ) ) Cn C ) = ( II Cn C ) )
26	16 25	eleqtrd	\|- ( ph -> K e. ( II Cn C ) )
27	15	simprd	\|- ( ph -> ( F o. K ) = ( G \|` ( 0 [,] ( N / N ) ) ) )
28	21	reseq2d	\|- ( ph -> ( G \|` ( 0 [,] ( N / N ) ) ) = ( G \|` ( 0 [,] 1 ) ) )
29		iiuni	\|- ( 0 [,] 1 ) = U. II
30	29 3	cnf	\|- ( G e. ( II Cn J ) -> G : ( 0 [,] 1 ) --> X )
31		ffn	\|- ( G : ( 0 [,] 1 ) --> X -> G Fn ( 0 [,] 1 ) )
32		fnresdm	\|- ( G Fn ( 0 [,] 1 ) -> ( G \|` ( 0 [,] 1 ) ) = G )
33	5 30 31 32	4syl	\|- ( ph -> ( G \|` ( 0 [,] 1 ) ) = G )
34	27 28 33	3eqtrd	\|- ( ph -> ( F o. K ) = G )
35	26 34	jca	\|- ( ph -> ( K e. ( II Cn C ) /\ ( F o. K ) = G ) )

Metamath Proof Explorer

Theorem cvmliftlem11

Proof