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 JPConnYXJSConnBaseJπ1Y1𝑜

Proof

Step Hyp Ref Expression
1 sconnpi1.1 X=J
2 sconntop JSConnJTop
3 2 adantl YXJSConnJTop
4 simpl YXJSConnYX
5 eqid Jπ1Y=Jπ1Y
6 eqid BaseJπ1Y=BaseJπ1Y
7 simpl JTopYXJTop
8 1 toptopon JTopJTopOnX
9 7 8 sylib JTopYXJTopOnX
10 simpr JTopYXYX
11 5 6 9 10 elpi1 JTopYXxBaseJπ1YfIICnJf0=Yf1=Yx=fphJ
12 3 4 11 syl2anc YXJSConnxBaseJπ1YfIICnJf0=Yf1=Yx=fphJ
13 phtpcer phJErIICnJ
14 13 a1i YXJSConnfIICnJf0=Yf1=YphJErIICnJ
15 simpllr YXJSConnfIICnJf0=Yf1=YJSConn
16 simplr YXJSConnfIICnJf0=Yf1=YfIICnJ
17 simprl YXJSConnfIICnJf0=Yf1=Yf0=Y
18 simprr YXJSConnfIICnJf0=Yf1=Yf1=Y
19 17 18 eqtr4d YXJSConnfIICnJf0=Yf1=Yf0=f1
20 sconnpht JSConnfIICnJf0=f1fphJ01×f0
21 15 16 19 20 syl3anc YXJSConnfIICnJf0=Yf1=YfphJ01×f0
22 17 sneqd YXJSConnfIICnJf0=Yf1=Yf0=Y
23 22 xpeq2d YXJSConnfIICnJf0=Yf1=Y01×f0=01×Y
24 21 23 breqtrd YXJSConnfIICnJf0=Yf1=YfphJ01×Y
25 14 24 erthi YXJSConnfIICnJf0=Yf1=YfphJ=01×YphJ
26 3 8 sylib YXJSConnJTopOnX
27 eqid 01×Y=01×Y
28 5 27 pi1id JTopOnXYX01×YphJ=0Jπ1Y
29 26 4 28 syl2anc YXJSConn01×YphJ=0Jπ1Y
30 29 ad2antrr YXJSConnfIICnJf0=Yf1=Y01×YphJ=0Jπ1Y
31 25 30 eqtrd YXJSConnfIICnJf0=Yf1=YfphJ=0Jπ1Y
32 velsn x0Jπ1Yx=0Jπ1Y
33 eqeq1 x=fphJx=0Jπ1YfphJ=0Jπ1Y
34 32 33 syl5bb x=fphJx0Jπ1YfphJ=0Jπ1Y
35 31 34 syl5ibrcom YXJSConnfIICnJf0=Yf1=Yx=fphJx0Jπ1Y
36 35 expimpd YXJSConnfIICnJf0=Yf1=Yx=fphJx0Jπ1Y
37 36 rexlimdva YXJSConnfIICnJf0=Yf1=Yx=fphJx0Jπ1Y
38 12 37 sylbid YXJSConnxBaseJπ1Yx0Jπ1Y
39 38 ssrdv YXJSConnBaseJπ1Y0Jπ1Y
40 5 pi1grp JTopOnXYXJπ1YGrp
41 26 4 40 syl2anc YXJSConnJπ1YGrp
42 eqid 0Jπ1Y=0Jπ1Y
43 6 42 grpidcl Jπ1YGrp0Jπ1YBaseJπ1Y
44 41 43 syl YXJSConn0Jπ1YBaseJπ1Y
45 44 snssd YXJSConn0Jπ1YBaseJπ1Y
46 39 45 eqssd YXJSConnBaseJπ1Y=0Jπ1Y
47 fvex 0Jπ1YV
48 47 ensn1 0Jπ1Y1𝑜
49 46 48 eqbrtrdi YXJSConnBaseJπ1Y1𝑜
50 49 adantll JPConnYXJSConnBaseJπ1Y1𝑜
51 simpll JPConnYXBaseJπ1Y1𝑜JPConn
52 eqid Jπ1f0=Jπ1f0
53 eqid BaseJπ1f0=BaseJπ1f0
54 simplll JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1JPConn
55 pconntop JPConnJTop
56 54 55 syl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1JTop
57 56 8 sylib JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1JTopOnX
58 simprl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fIICnJ
59 iiuni 01=II
60 59 1 cnf fIICnJf:01X
61 58 60 syl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1f:01X
62 0elunit 001
63 ffvelrn f:01X001f0X
64 61 62 63 sylancl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1f0X
65 eqidd JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1f0=f0
66 simprr JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1f0=f1
67 66 eqcomd JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1f1=f0
68 52 53 57 64 58 65 67 elpi1i JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJBaseJπ1f0
69 eqid 01×f0=01×f0
70 69 pcoptcl JTopOnXf0X01×f0IICnJ01×f00=f001×f01=f0
71 57 64 70 syl2anc JPConnYXBaseJπ1Y1𝑜fIICnJf0=f101×f0IICnJ01×f00=f001×f01=f0
72 71 simp1d JPConnYXBaseJπ1Y1𝑜fIICnJf0=f101×f0IICnJ
73 71 simp2d JPConnYXBaseJπ1Y1𝑜fIICnJf0=f101×f00=f0
74 71 simp3d JPConnYXBaseJπ1Y1𝑜fIICnJf0=f101×f01=f0
75 52 53 57 64 72 73 74 elpi1i JPConnYXBaseJπ1Y1𝑜fIICnJf0=f101×f0phJBaseJπ1f0
76 simpllr JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1YX
77 1 52 5 53 6 pconnpi1 JPConnf0XYXJπ1f0𝑔Jπ1Y
78 54 64 76 77 syl3anc JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1Jπ1f0𝑔Jπ1Y
79 53 6 gicen Jπ1f0𝑔Jπ1YBaseJπ1f0BaseJπ1Y
80 78 79 syl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1BaseJπ1f0BaseJπ1Y
81 simplr JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1BaseJπ1Y1𝑜
82 entr BaseJπ1f0BaseJπ1YBaseJπ1Y1𝑜BaseJπ1f01𝑜
83 80 81 82 syl2anc JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1BaseJπ1f01𝑜
84 en1eqsn 01×f0phJBaseJπ1f0BaseJπ1f01𝑜BaseJπ1f0=01×f0phJ
85 75 83 84 syl2anc JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1BaseJπ1f0=01×f0phJ
86 68 85 eleqtrd JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ01×f0phJ
87 elsni fphJ01×f0phJfphJ=01×f0phJ
88 86 87 syl JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ=01×f0phJ
89 13 a1i JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1phJErIICnJ
90 89 58 erth JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ01×f0fphJ=01×f0phJ
91 88 90 mpbird JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ01×f0
92 91 expr JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ01×f0
93 92 ralrimiva JPConnYXBaseJπ1Y1𝑜fIICnJf0=f1fphJ01×f0
94 issconn JSConnJPConnfIICnJf0=f1fphJ01×f0
95 51 93 94 sylanbrc JPConnYXBaseJπ1Y1𝑜JSConn
96 50 95 impbida JPConnYXJSConnBaseJπ1Y1𝑜