Metamath Proof Explorer


Theorem sconnpi1

Description: A path-connected topological space is simply connected iff its fundamental group is trivial. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypothesis sconnpi1.1 X = J
Assertion sconnpi1 J PConn Y X J SConn Base J π 1 Y 1 𝑜

Proof

Step Hyp Ref Expression
1 sconnpi1.1 X = J
2 sconntop J SConn J Top
3 2 adantl Y X J SConn J Top
4 simpl Y X J SConn Y X
5 eqid J π 1 Y = J π 1 Y
6 eqid Base J π 1 Y = Base J π 1 Y
7 simpl J Top Y X J Top
8 1 toptopon J Top J TopOn X
9 7 8 sylib J Top Y X J TopOn X
10 simpr J Top Y X Y X
11 5 6 9 10 elpi1 J Top Y X x Base J π 1 Y f II Cn J f 0 = Y f 1 = Y x = f ph J
12 3 4 11 syl2anc Y X J SConn x Base J π 1 Y f II Cn J f 0 = Y f 1 = Y x = f ph J
13 phtpcer ph J Er II Cn J
14 13 a1i Y X J SConn f II Cn J f 0 = Y f 1 = Y ph J Er II Cn J
15 simpllr Y X J SConn f II Cn J f 0 = Y f 1 = Y J SConn
16 simplr Y X J SConn f II Cn J f 0 = Y f 1 = Y f II Cn J
17 simprl Y X J SConn f II Cn J f 0 = Y f 1 = Y f 0 = Y
18 simprr Y X J SConn f II Cn J f 0 = Y f 1 = Y f 1 = Y
19 17 18 eqtr4d Y X J SConn f II Cn J f 0 = Y f 1 = Y f 0 = f 1
20 sconnpht J SConn f II Cn J f 0 = f 1 f ph J 0 1 × f 0
21 15 16 19 20 syl3anc Y X J SConn f II Cn J f 0 = Y f 1 = Y f ph J 0 1 × f 0
22 17 sneqd Y X J SConn f II Cn J f 0 = Y f 1 = Y f 0 = Y
23 22 xpeq2d Y X J SConn f II Cn J f 0 = Y f 1 = Y 0 1 × f 0 = 0 1 × Y
24 21 23 breqtrd Y X J SConn f II Cn J f 0 = Y f 1 = Y f ph J 0 1 × Y
25 14 24 erthi Y X J SConn f II Cn J f 0 = Y f 1 = Y f ph J = 0 1 × Y ph J
26 3 8 sylib Y X J SConn J TopOn X
27 eqid 0 1 × Y = 0 1 × Y
28 5 27 pi1id J TopOn X Y X 0 1 × Y ph J = 0 J π 1 Y
29 26 4 28 syl2anc Y X J SConn 0 1 × Y ph J = 0 J π 1 Y
30 29 ad2antrr Y X J SConn f II Cn J f 0 = Y f 1 = Y 0 1 × Y ph J = 0 J π 1 Y
31 25 30 eqtrd Y X J SConn f II Cn J f 0 = Y f 1 = Y f ph J = 0 J π 1 Y
32 velsn x 0 J π 1 Y x = 0 J π 1 Y
33 eqeq1 x = f ph J x = 0 J π 1 Y f ph J = 0 J π 1 Y
34 32 33 syl5bb x = f ph J x 0 J π 1 Y f ph J = 0 J π 1 Y
35 31 34 syl5ibrcom Y X J SConn f II Cn J f 0 = Y f 1 = Y x = f ph J x 0 J π 1 Y
36 35 expimpd Y X J SConn f II Cn J f 0 = Y f 1 = Y x = f ph J x 0 J π 1 Y
37 36 rexlimdva Y X J SConn f II Cn J f 0 = Y f 1 = Y x = f ph J x 0 J π 1 Y
38 12 37 sylbid Y X J SConn x Base J π 1 Y x 0 J π 1 Y
39 38 ssrdv Y X J SConn Base J π 1 Y 0 J π 1 Y
40 5 pi1grp J TopOn X Y X J π 1 Y Grp
41 26 4 40 syl2anc Y X J SConn J π 1 Y Grp
42 eqid 0 J π 1 Y = 0 J π 1 Y
43 6 42 grpidcl J π 1 Y Grp 0 J π 1 Y Base J π 1 Y
44 41 43 syl Y X J SConn 0 J π 1 Y Base J π 1 Y
45 44 snssd Y X J SConn 0 J π 1 Y Base J π 1 Y
46 39 45 eqssd Y X J SConn Base J π 1 Y = 0 J π 1 Y
47 fvex 0 J π 1 Y V
48 47 ensn1 0 J π 1 Y 1 𝑜
49 46 48 eqbrtrdi Y X J SConn Base J π 1 Y 1 𝑜
50 49 adantll J PConn Y X J SConn Base J π 1 Y 1 𝑜
51 simpll J PConn Y X Base J π 1 Y 1 𝑜 J PConn
52 eqid J π 1 f 0 = J π 1 f 0
53 eqid Base J π 1 f 0 = Base J π 1 f 0
54 simplll J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 J PConn
55 pconntop J PConn J Top
56 54 55 syl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 J Top
57 56 8 sylib J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 J TopOn X
58 simprl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f II Cn J
59 iiuni 0 1 = II
60 59 1 cnf f II Cn J f : 0 1 X
61 58 60 syl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f : 0 1 X
62 0elunit 0 0 1
63 ffvelrn f : 0 1 X 0 0 1 f 0 X
64 61 62 63 sylancl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f 0 X
65 eqidd J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f 0 = f 0
66 simprr J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f 0 = f 1
67 66 eqcomd J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f 1 = f 0
68 52 53 57 64 58 65 67 elpi1i J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J Base J π 1 f 0
69 eqid 0 1 × f 0 = 0 1 × f 0
70 69 pcoptcl J TopOn X f 0 X 0 1 × f 0 II Cn J 0 1 × f 0 0 = f 0 0 1 × f 0 1 = f 0
71 57 64 70 syl2anc J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 0 1 × f 0 II Cn J 0 1 × f 0 0 = f 0 0 1 × f 0 1 = f 0
72 71 simp1d J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 0 1 × f 0 II Cn J
73 71 simp2d J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 0 1 × f 0 0 = f 0
74 71 simp3d J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 0 1 × f 0 1 = f 0
75 52 53 57 64 72 73 74 elpi1i J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 0 1 × f 0 ph J Base J π 1 f 0
76 simpllr J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 Y X
77 1 52 5 53 6 pconnpi1 J PConn f 0 X Y X J π 1 f 0 𝑔 J π 1 Y
78 54 64 76 77 syl3anc J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 J π 1 f 0 𝑔 J π 1 Y
79 53 6 gicen J π 1 f 0 𝑔 J π 1 Y Base J π 1 f 0 Base J π 1 Y
80 78 79 syl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 Base J π 1 f 0 Base J π 1 Y
81 simplr J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 Base J π 1 Y 1 𝑜
82 entr Base J π 1 f 0 Base J π 1 Y Base J π 1 Y 1 𝑜 Base J π 1 f 0 1 𝑜
83 80 81 82 syl2anc J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 Base J π 1 f 0 1 𝑜
84 en1eqsn 0 1 × f 0 ph J Base J π 1 f 0 Base J π 1 f 0 1 𝑜 Base J π 1 f 0 = 0 1 × f 0 ph J
85 75 83 84 syl2anc J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 Base J π 1 f 0 = 0 1 × f 0 ph J
86 68 85 eleqtrd J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J 0 1 × f 0 ph J
87 elsni f ph J 0 1 × f 0 ph J f ph J = 0 1 × f 0 ph J
88 86 87 syl J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J = 0 1 × f 0 ph J
89 13 a1i J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 ph J Er II Cn J
90 89 58 erth J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J 0 1 × f 0 f ph J = 0 1 × f 0 ph J
91 88 90 mpbird J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J 0 1 × f 0
92 91 expr J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J 0 1 × f 0
93 92 ralrimiva J PConn Y X Base J π 1 Y 1 𝑜 f II Cn J f 0 = f 1 f ph J 0 1 × f 0
94 issconn J SConn J PConn f II Cn J f 0 = f 1 f ph J 0 1 × f 0
95 51 93 94 sylanbrc J PConn Y X Base J π 1 Y 1 𝑜 J SConn
96 50 95 impbida J PConn Y X J SConn Base J π 1 Y 1 𝑜