Metamath Proof Explorer

Theorem cvmlift3lem5

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 6-Jul-2015)

Ref Expression
Hypotheses cvmlift3.b 
|- B = U. C
cvmlift3.y 
|- Y = U. K
cvmlift3.f 
|- ( ph -> F e. ( C CovMap J ) )
cvmlift3.k 
|- ( ph -> K e. SConn )
cvmlift3.l 
|- ( ph -> K e. N-Locally PConn )
cvmlift3.o 
|- ( ph -> O e. Y )
cvmlift3.g 
|- ( ph -> G e. ( K Cn J ) )
cvmlift3.p 
|- ( ph -> P e. B )
cvmlift3.e 
|- ( ph -> ( F ` P ) = ( G ` O ) )
cvmlift3.h 
|- H = ( x e. Y |-> ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
Assertion cvmlift3lem5 
|- ( ph -> ( F o. H ) = G )

Proof

Step Hyp Ref Expression
1 cvmlift3.b 
 |-  B = U. C
2 cvmlift3.y 
 |-  Y = U. K
3 cvmlift3.f 
 |-  ( ph -> F e. ( C CovMap J ) )
4 cvmlift3.k 
 |-  ( ph -> K e. SConn )
5 cvmlift3.l 
 |-  ( ph -> K e. N-Locally PConn )
6 cvmlift3.o 
 |-  ( ph -> O e. Y )
7 cvmlift3.g 
 |-  ( ph -> G e. ( K Cn J ) )
8 cvmlift3.p 
 |-  ( ph -> P e. B )
9 cvmlift3.e 
 |-  ( ph -> ( F ` P ) = ( G ` O ) )
10 cvmlift3.h 
 |-  H = ( x e. Y |-> ( iota_ z e. B E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = x /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = z ) ) )
11 eqid 
 |-  ( H ` y ) = ( H ` y )
12 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 
 |-  ( ( ph /\ y e. Y ) -> ( ( H ` y ) = ( H ` y ) <-> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = y /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) ) )
13 11 12 mpbii 
 |-  ( ( ph /\ y e. Y ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = y /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) )
14 df-3an 
 |-  ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = y /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) <-> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) )
15 eqid 
 |-  ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) = ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) )
16 3 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> F e. ( C CovMap J ) )
17 simplr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> f e. ( II Cn K ) )
18 7 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> G e. ( K Cn J ) )
19 cnco 
 |-  ( ( f e. ( II Cn K ) /\ G e. ( K Cn J ) ) -> ( G o. f ) e. ( II Cn J ) )
20 17 18 19 syl2anc 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( G o. f ) e. ( II Cn J ) )
21 8 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> P e. B )
22 simprl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( f ` 0 ) = O )
23 22 fveq2d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( G ` ( f ` 0 ) ) = ( G ` O ) )
24 iiuni 
 |-  ( 0 [,] 1 ) = U. II
25 24 2 cnf 
 |-  ( f e. ( II Cn K ) -> f : ( 0 [,] 1 ) --> Y )
26 17 25 syl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> f : ( 0 [,] 1 ) --> Y )
27 0elunit 
 |-  0 e. ( 0 [,] 1 )
28 fvco3 
 |-  ( ( f : ( 0 [,] 1 ) --> Y /\ 0 e. ( 0 [,] 1 ) ) -> ( ( G o. f ) ` 0 ) = ( G ` ( f ` 0 ) ) )
29 26 27 28 sylancl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( G o. f ) ` 0 ) = ( G ` ( f ` 0 ) ) )
30 9 ad3antrrr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( F ` P ) = ( G ` O ) )
31 23 29 30 3eqtr4rd 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( F ` P ) = ( ( G o. f ) ` 0 ) )
32 1 15 16 20 21 31 cvmliftiota 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) /\ ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) = ( G o. f ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 0 ) = P ) )
33 32 simp2d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) = ( G o. f ) )
34 33 fveq1d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) ` 1 ) = ( ( G o. f ) ` 1 ) )
35 32 simp1d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) )
36 24 1 cnf 
 |-  ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) e. ( II Cn C ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
37 35 36 syl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B )
38 1elunit 
 |-  1 e. ( 0 [,] 1 )
39 fvco3 
 |-  ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) : ( 0 [,] 1 ) --> B /\ 1 e. ( 0 [,] 1 ) ) -> ( ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) ` 1 ) = ( F ` ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
40 37 38 39 sylancl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( F o. ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ) ` 1 ) = ( F ` ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) )
41 fvco3 
 |-  ( ( f : ( 0 [,] 1 ) --> Y /\ 1 e. ( 0 [,] 1 ) ) -> ( ( G o. f ) ` 1 ) = ( G ` ( f ` 1 ) ) )
42 26 38 41 sylancl 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( G o. f ) ` 1 ) = ( G ` ( f ` 1 ) ) )
43 simprr 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( f ` 1 ) = y )
44 43 fveq2d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( G ` ( f ` 1 ) ) = ( G ` y ) )
45 42 44 eqtrd 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( G o. f ) ` 1 ) = ( G ` y ) )
46 34 40 45 3eqtr3d 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( F ` ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) = ( G ` y ) )
47 fveqeq2 
 |-  ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) -> ( ( F ` ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) ) = ( G ` y ) <-> ( F ` ( H ` y ) ) = ( G ` y ) ) )
48 46 47 syl5ibcom 
 |-  ( ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) /\ ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) ) -> ( ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) -> ( F ` ( H ` y ) ) = ( G ` y ) ) )
49 48 expimpd 
 |-  ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) -> ( ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = y ) /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) -> ( F ` ( H ` y ) ) = ( G ` y ) ) )
50 14 49 syl5bi 
 |-  ( ( ( ph /\ y e. Y ) /\ f e. ( II Cn K ) ) -> ( ( ( f ` 0 ) = O /\ ( f ` 1 ) = y /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) -> ( F ` ( H ` y ) ) = ( G ` y ) ) )
51 50 rexlimdva 
 |-  ( ( ph /\ y e. Y ) -> ( E. f e. ( II Cn K ) ( ( f ` 0 ) = O /\ ( f ` 1 ) = y /\ ( ( iota_ g e. ( II Cn C ) ( ( F o. g ) = ( G o. f ) /\ ( g ` 0 ) = P ) ) ` 1 ) = ( H ` y ) ) -> ( F ` ( H ` y ) ) = ( G ` y ) ) )
52 13 51 mpd 
 |-  ( ( ph /\ y e. Y ) -> ( F ` ( H ` y ) ) = ( G ` y ) )
53 52 mpteq2dva 
 |-  ( ph -> ( y e. Y |-> ( F ` ( H ` y ) ) ) = ( y e. Y |-> ( G ` y ) ) )
54 1 2 3 4 5 6 7 8 9 10 cvmlift3lem3 
 |-  ( ph -> H : Y --> B )
55 54 ffvelrnda 
 |-  ( ( ph /\ y e. Y ) -> ( H ` y ) e. B )
56 54 feqmptd 
 |-  ( ph -> H = ( y e. Y |-> ( H ` y ) ) )
57 cvmcn 
 |-  ( F e. ( C CovMap J ) -> F e. ( C Cn J ) )
58 eqid 
 |-  U. J = U. J
59 1 58 cnf 
 |-  ( F e. ( C Cn J ) -> F : B --> U. J )
60 3 57 59 3syl 
 |-  ( ph -> F : B --> U. J )
61 60 feqmptd 
 |-  ( ph -> F = ( w e. B |-> ( F ` w ) ) )
62 fveq2 
 |-  ( w = ( H ` y ) -> ( F ` w ) = ( F ` ( H ` y ) ) )
63 55 56 61 62 fmptco 
 |-  ( ph -> ( F o. H ) = ( y e. Y |-> ( F ` ( H ` y ) ) ) )
64 2 58 cnf 
 |-  ( G e. ( K Cn J ) -> G : Y --> U. J )
65 7 64 syl 
 |-  ( ph -> G : Y --> U. J )
66 65 feqmptd 
 |-  ( ph -> G = ( y e. Y |-> ( G ` y ) ) )
67 53 63 66 3eqtr4d 
 |-  ( ph -> ( F o. H ) = G )