cvmliftlem13

Description: Lemma for cvmlift . The initial value of K is P because Q ( 1 ) is a subset of K which takes value P at 0 . (Contributed by Mario Carneiro, 16-Feb-2015)

	Ref	Expression
Hypotheses	cvmliftlem.1	\|- S = ( k e. J \|-> { s e. ( ~P C \ { (/) } ) \| ( U. s = ( `' F " k ) /\ A. u e. s ( A. v e. ( s \ { u } ) ( u i^i v ) = (/) /\ ( F \|` u ) e. ( ( C \|`t u ) Homeo ( J \|`t k ) ) ) ) } )
	cvmliftlem.b	\|- B = U. C
	cvmliftlem.x	\|- X = U. J
	cvmliftlem.f	\|- ( ph -> F e. ( C CovMap J ) )
	cvmliftlem.g	\|- ( ph -> G e. ( II Cn J ) )
	cvmliftlem.p	\|- ( ph -> P e. B )
	cvmliftlem.e	\|- ( ph -> ( F ` P ) = ( G ` 0 ) )
	cvmliftlem.n	\|- ( ph -> N e. NN )
	cvmliftlem.t	\|- ( ph -> T : ( 1 ... N ) --> U_ j e. J ( { j } X. ( S ` j ) ) )
	cvmliftlem.a	\|- ( ph -> A. k e. ( 1 ... N ) ( G " ( ( ( k - 1 ) / N ) [,] ( k / N ) ) ) C_ ( 1st ` ( T ` k ) ) )
	cvmliftlem.l	\|- L = ( topGen ` ran (,) )
	cvmliftlem.q	\|- Q = seq 0 ( ( x e. _V , m e. NN \|-> ( z e. ( ( ( m - 1 ) / N ) [,] ( m / N ) ) \|-> ( `' ( F \|` ( iota_ b e. ( 2nd ` ( T ` m ) ) ( x ` ( ( m - 1 ) / N ) ) e. b ) ) ` ( G ` z ) ) ) ) , ( ( _I \|` NN ) u. { <. 0 , { <. 0 , P >. } >. } ) )
	cvmliftlem.k	\|- K = U_ k e. ( 1 ... N ) ( Q ` k )
Assertion	cvmliftlem13	\|- ( ph -> ( K ` 0 ) = P )

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	1 2 3 4 5 6 7 8 9 10 11 12 13	cvmliftlem11	\|- ( ph -> ( K e. ( II Cn C ) /\ ( F o. K ) = G ) )
15	14	simpld	\|- ( ph -> K e. ( II Cn C ) )
16		iiuni	\|- ( 0 [,] 1 ) = U. II
17	16 2	cnf	\|- ( K e. ( II Cn C ) -> K : ( 0 [,] 1 ) --> B )
18	15 17	syl	\|- ( ph -> K : ( 0 [,] 1 ) --> B )
19	18	ffund	\|- ( ph -> Fun K )
20		nnuz	\|- NN = ( ZZ>= ` 1 )
21	8 20	eleqtrdi	\|- ( ph -> N e. ( ZZ>= ` 1 ) )
22		eluzfz1	\|- ( N e. ( ZZ>= ` 1 ) -> 1 e. ( 1 ... N ) )
23	21 22	syl	\|- ( ph -> 1 e. ( 1 ... N ) )
24		fveq2	\|- ( k = 1 -> ( Q ` k ) = ( Q ` 1 ) )
25	24	ssiun2s	\|- ( 1 e. ( 1 ... N ) -> ( Q ` 1 ) C_ U_ k e. ( 1 ... N ) ( Q ` k ) )
26	23 25	syl	\|- ( ph -> ( Q ` 1 ) C_ U_ k e. ( 1 ... N ) ( Q ` k ) )
27	26 13	sseqtrrdi	\|- ( ph -> ( Q ` 1 ) C_ K )
28		0xr	\|- 0 e. RR*
29	28	a1i	\|- ( ph -> 0 e. RR* )
30	8	nnrecred	\|- ( ph -> ( 1 / N ) e. RR )
31	30	rexrd	\|- ( ph -> ( 1 / N ) e. RR* )
32		1red	\|- ( ph -> 1 e. RR )
33		0le1	\|- 0 <_ 1
34	33	a1i	\|- ( ph -> 0 <_ 1 )
35	8	nnred	\|- ( ph -> N e. RR )
36	8	nngt0d	\|- ( ph -> 0 < N )
37		divge0	\|- ( ( ( 1 e. RR /\ 0 <_ 1 ) /\ ( N e. RR /\ 0 < N ) ) -> 0 <_ ( 1 / N ) )
38	32 34 35 36 37	syl22anc	\|- ( ph -> 0 <_ ( 1 / N ) )
39		lbicc2	\|- ( ( 0 e. RR* /\ ( 1 / N ) e. RR* /\ 0 <_ ( 1 / N ) ) -> 0 e. ( 0 [,] ( 1 / N ) ) )
40	29 31 38 39	syl3anc	\|- ( ph -> 0 e. ( 0 [,] ( 1 / N ) ) )
41		1m1e0	\|- ( 1 - 1 ) = 0
42	41	oveq1i	\|- ( ( 1 - 1 ) / N ) = ( 0 / N )
43	8	nncnd	\|- ( ph -> N e. CC )
44	8	nnne0d	\|- ( ph -> N =/= 0 )
45	43 44	div0d	\|- ( ph -> ( 0 / N ) = 0 )
46	42 45	syl5eq	\|- ( ph -> ( ( 1 - 1 ) / N ) = 0 )
47	46	oveq1d	\|- ( ph -> ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( 0 [,] ( 1 / N ) ) )
48	40 47	eleqtrrd	\|- ( ph -> 0 e. ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) )
49		eqid	\|- ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) = ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) )
50		simpr	\|- ( ( ph /\ 1 e. ( 1 ... N ) ) -> 1 e. ( 1 ... N ) )
51	1 2 3 4 5 6 7 8 9 10 11 12 49	cvmliftlem7	\|- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) e. ( `' F " { ( G ` ( ( 1 - 1 ) / N ) ) } ) )
52	1 2 3 4 5 6 7 8 9 10 11 12 49 50 51	cvmliftlem6	\|- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G \|` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
53	23 52	mpdan	\|- ( ph -> ( ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B /\ ( F o. ( Q ` 1 ) ) = ( G \|` ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) ) ) )
54	53	simpld	\|- ( ph -> ( Q ` 1 ) : ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) --> B )
55	54	fdmd	\|- ( ph -> dom ( Q ` 1 ) = ( ( ( 1 - 1 ) / N ) [,] ( 1 / N ) ) )
56	48 55	eleqtrrd	\|- ( ph -> 0 e. dom ( Q ` 1 ) )
57		funssfv	\|- ( ( Fun K /\ ( Q ` 1 ) C_ K /\ 0 e. dom ( Q ` 1 ) ) -> ( K ` 0 ) = ( ( Q ` 1 ) ` 0 ) )
58	19 27 56 57	syl3anc	\|- ( ph -> ( K ` 0 ) = ( ( Q ` 1 ) ` 0 ) )
59	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem9	\|- ( ( ph /\ 1 e. ( 1 ... N ) ) -> ( ( Q ` 1 ) ` ( ( 1 - 1 ) / N ) ) = ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) )
60	23 59	mpdan	\|- ( ph -> ( ( Q ` 1 ) ` ( ( 1 - 1 ) / N ) ) = ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) )
61	46	fveq2d	\|- ( ph -> ( ( Q ` 1 ) ` ( ( 1 - 1 ) / N ) ) = ( ( Q ` 1 ) ` 0 ) )
62	41	fveq2i	\|- ( Q ` ( 1 - 1 ) ) = ( Q ` 0 )
63	1 2 3 4 5 6 7 8 9 10 11 12	cvmliftlem4	\|- ( Q ` 0 ) = { <. 0 , P >. }
64	62 63	eqtri	\|- ( Q ` ( 1 - 1 ) ) = { <. 0 , P >. }
65	64	a1i	\|- ( ph -> ( Q ` ( 1 - 1 ) ) = { <. 0 , P >. } )
66	65 46	fveq12d	\|- ( ph -> ( ( Q ` ( 1 - 1 ) ) ` ( ( 1 - 1 ) / N ) ) = ( { <. 0 , P >. } ` 0 ) )
67	60 61 66	3eqtr3d	\|- ( ph -> ( ( Q ` 1 ) ` 0 ) = ( { <. 0 , P >. } ` 0 ) )
68		0nn0	\|- 0 e. NN0
69		fvsng	\|- ( ( 0 e. NN0 /\ P e. B ) -> ( { <. 0 , P >. } ` 0 ) = P )
70	68 6 69	sylancr	\|- ( ph -> ( { <. 0 , P >. } ` 0 ) = P )
71	58 67 70	3eqtrd	\|- ( ph -> ( K ` 0 ) = P )

Metamath Proof Explorer

Theorem cvmliftlem13

Proof