Metamath Proof Explorer


Theorem cvmlift3lem9

Description: Lemma for cvmlift2 . (Contributed by Mario Carneiro, 7-May-2015)

Ref Expression
Hypotheses cvmlift3.b B = C
cvmlift3.y Y = K
cvmlift3.f φ F C CovMap J
cvmlift3.k φ K SConn
cvmlift3.l φ K N-Locally PConn
cvmlift3.o φ O Y
cvmlift3.g φ G K Cn J
cvmlift3.p φ P B
cvmlift3.e φ F P = G O
cvmlift3.h H = x Y ι z B | f II Cn K f 0 = O f 1 = x ι g II Cn C | F g = G f g 0 = P 1 = z
cvmlift3lem7.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
Assertion cvmlift3lem9 φ f K Cn C F f = G f O = P

Proof

Step Hyp Ref Expression
1 cvmlift3.b B = C
2 cvmlift3.y Y = K
3 cvmlift3.f φ F C CovMap J
4 cvmlift3.k φ K SConn
5 cvmlift3.l φ K N-Locally PConn
6 cvmlift3.o φ O Y
7 cvmlift3.g φ G K Cn J
8 cvmlift3.p φ P B
9 cvmlift3.e φ F P = G O
10 cvmlift3.h H = x Y ι z B | f II Cn K f 0 = O f 1 = x ι g II Cn C | F g = G f g 0 = P 1 = z
11 cvmlift3lem7.s S = k J s 𝒫 C | s = F -1 k c s d s c c d = F c C 𝑡 c Homeo J 𝑡 k
12 1 2 3 4 5 6 7 8 9 10 11 cvmlift3lem8 φ H K Cn C
13 1 2 3 4 5 6 7 8 9 10 cvmlift3lem5 φ F H = G
14 iitopon II TopOn 0 1
15 14 a1i φ II TopOn 0 1
16 sconntop K SConn K Top
17 4 16 syl φ K Top
18 2 toptopon K Top K TopOn Y
19 17 18 sylib φ K TopOn Y
20 cnconst2 II TopOn 0 1 K TopOn Y O Y 0 1 × O II Cn K
21 15 19 6 20 syl3anc φ 0 1 × O II Cn K
22 0elunit 0 0 1
23 fvconst2g O Y 0 0 1 0 1 × O 0 = O
24 6 22 23 sylancl φ 0 1 × O 0 = O
25 1elunit 1 0 1
26 fvconst2g O Y 1 0 1 0 1 × O 1 = O
27 6 25 26 sylancl φ 0 1 × O 1 = O
28 9 sneqd φ F P = G O
29 28 xpeq2d φ 0 1 × F P = 0 1 × G O
30 cvmcn F C CovMap J F C Cn J
31 eqid J = J
32 1 31 cnf F C Cn J F : B J
33 ffn F : B J F Fn B
34 3 30 32 33 4syl φ F Fn B
35 fcoconst F Fn B P B F 0 1 × P = 0 1 × F P
36 34 8 35 syl2anc φ F 0 1 × P = 0 1 × F P
37 2 31 cnf G K Cn J G : Y J
38 7 37 syl φ G : Y J
39 38 ffnd φ G Fn Y
40 fcoconst G Fn Y O Y G 0 1 × O = 0 1 × G O
41 39 6 40 syl2anc φ G 0 1 × O = 0 1 × G O
42 29 36 41 3eqtr4d φ F 0 1 × P = G 0 1 × O
43 fvconst2g P B 0 0 1 0 1 × P 0 = P
44 8 22 43 sylancl φ 0 1 × P 0 = P
45 cvmtop1 F C CovMap J C Top
46 3 45 syl φ C Top
47 1 toptopon C Top C TopOn B
48 46 47 sylib φ C TopOn B
49 cnconst2 II TopOn 0 1 C TopOn B P B 0 1 × P II Cn C
50 15 48 8 49 syl3anc φ 0 1 × P II Cn C
51 cvmtop2 F C CovMap J J Top
52 3 51 syl φ J Top
53 31 toptopon J Top J TopOn J
54 52 53 sylib φ J TopOn J
55 38 6 ffvelrnd φ G O J
56 cnconst2 II TopOn 0 1 J TopOn J G O J 0 1 × G O II Cn J
57 15 54 55 56 syl3anc φ 0 1 × G O II Cn J
58 41 57 eqeltrd φ G 0 1 × O II Cn J
59 fvconst2g G O J 0 0 1 0 1 × G O 0 = G O
60 55 22 59 sylancl φ 0 1 × G O 0 = G O
61 41 fveq1d φ G 0 1 × O 0 = 0 1 × G O 0
62 60 61 9 3eqtr4rd φ F P = G 0 1 × O 0
63 1 cvmlift F C CovMap J G 0 1 × O II Cn J P B F P = G 0 1 × O 0 ∃! g II Cn C F g = G 0 1 × O g 0 = P
64 3 58 8 62 63 syl22anc φ ∃! g II Cn C F g = G 0 1 × O g 0 = P
65 coeq2 g = 0 1 × P F g = F 0 1 × P
66 65 eqeq1d g = 0 1 × P F g = G 0 1 × O F 0 1 × P = G 0 1 × O
67 fveq1 g = 0 1 × P g 0 = 0 1 × P 0
68 67 eqeq1d g = 0 1 × P g 0 = P 0 1 × P 0 = P
69 66 68 anbi12d g = 0 1 × P F g = G 0 1 × O g 0 = P F 0 1 × P = G 0 1 × O 0 1 × P 0 = P
70 69 riota2 0 1 × P II Cn C ∃! g II Cn C F g = G 0 1 × O g 0 = P F 0 1 × P = G 0 1 × O 0 1 × P 0 = P ι g II Cn C | F g = G 0 1 × O g 0 = P = 0 1 × P
71 50 64 70 syl2anc φ F 0 1 × P = G 0 1 × O 0 1 × P 0 = P ι g II Cn C | F g = G 0 1 × O g 0 = P = 0 1 × P
72 42 44 71 mpbi2and φ ι g II Cn C | F g = G 0 1 × O g 0 = P = 0 1 × P
73 72 fveq1d φ ι g II Cn C | F g = G 0 1 × O g 0 = P 1 = 0 1 × P 1
74 fvconst2g P B 1 0 1 0 1 × P 1 = P
75 8 25 74 sylancl φ 0 1 × P 1 = P
76 73 75 eqtrd φ ι g II Cn C | F g = G 0 1 × O g 0 = P 1 = P
77 fveq1 f = 0 1 × O f 0 = 0 1 × O 0
78 77 eqeq1d f = 0 1 × O f 0 = O 0 1 × O 0 = O
79 fveq1 f = 0 1 × O f 1 = 0 1 × O 1
80 79 eqeq1d f = 0 1 × O f 1 = O 0 1 × O 1 = O
81 coeq2 f = 0 1 × O G f = G 0 1 × O
82 81 eqeq2d f = 0 1 × O F g = G f F g = G 0 1 × O
83 82 anbi1d f = 0 1 × O F g = G f g 0 = P F g = G 0 1 × O g 0 = P
84 83 riotabidv f = 0 1 × O ι g II Cn C | F g = G f g 0 = P = ι g II Cn C | F g = G 0 1 × O g 0 = P
85 84 fveq1d f = 0 1 × O ι g II Cn C | F g = G f g 0 = P 1 = ι g II Cn C | F g = G 0 1 × O g 0 = P 1
86 85 eqeq1d f = 0 1 × O ι g II Cn C | F g = G f g 0 = P 1 = P ι g II Cn C | F g = G 0 1 × O g 0 = P 1 = P
87 78 80 86 3anbi123d f = 0 1 × O f 0 = O f 1 = O ι g II Cn C | F g = G f g 0 = P 1 = P 0 1 × O 0 = O 0 1 × O 1 = O ι g II Cn C | F g = G 0 1 × O g 0 = P 1 = P
88 87 rspcev 0 1 × O II Cn K 0 1 × O 0 = O 0 1 × O 1 = O ι g II Cn C | F g = G 0 1 × O g 0 = P 1 = P f II Cn K f 0 = O f 1 = O ι g II Cn C | F g = G f g 0 = P 1 = P
89 21 24 27 76 88 syl13anc φ f II Cn K f 0 = O f 1 = O ι g II Cn C | F g = G f g 0 = P 1 = P
90 1 2 3 4 5 6 7 8 9 10 cvmlift3lem4 φ O Y H O = P f II Cn K f 0 = O f 1 = O ι g II Cn C | F g = G f g 0 = P 1 = P
91 6 90 mpdan φ H O = P f II Cn K f 0 = O f 1 = O ι g II Cn C | F g = G f g 0 = P 1 = P
92 89 91 mpbird φ H O = P
93 coeq2 f = H F f = F H
94 93 eqeq1d f = H F f = G F H = G
95 fveq1 f = H f O = H O
96 95 eqeq1d f = H f O = P H O = P
97 94 96 anbi12d f = H F f = G f O = P F H = G H O = P
98 97 rspcev H K Cn C F H = G H O = P f K Cn C F f = G f O = P
99 12 13 92 98 syl12anc φ f K Cn C F f = G f O = P