Metamath Proof Explorer


Theorem resconn

Description: A subset of RR is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015)

Ref Expression
Hypothesis resconn.1 J = topGen ran . 𝑡 A
Assertion resconn A J SConn J Conn

Proof

Step Hyp Ref Expression
1 resconn.1 J = topGen ran . 𝑡 A
2 sconnpconn J SConn J PConn
3 pconnconn J PConn J Conn
4 2 3 syl J SConn J Conn
5 eqid TopOpen fld = TopOpen fld
6 eqid topGen ran . = topGen ran .
7 5 6 rerest A TopOpen fld 𝑡 A = topGen ran . 𝑡 A
8 7 1 eqtr4di A TopOpen fld 𝑡 A = J
9 8 adantr A J Conn TopOpen fld 𝑡 A = J
10 simpl A J Conn A
11 ax-resscn
12 10 11 sstrdi A J Conn A
13 df-3an x A y A t 0 1 x A y A t 0 1
14 oveq2 z = x t z = t x
15 oveq2 w = y 1 t w = 1 t y
16 14 15 oveqan12d z = x w = y t z + 1 t w = t x + 1 t y
17 16 eleq1d z = x w = y t z + 1 t w A t x + 1 t y A
18 17 ralbidv z = x w = y t 0 1 t z + 1 t w A t 0 1 t x + 1 t y A
19 oveq2 z = y t z = t y
20 oveq2 w = x 1 t w = 1 t x
21 19 20 oveqan12d z = y w = x t z + 1 t w = t y + 1 t x
22 21 eleq1d z = y w = x t z + 1 t w A t y + 1 t x A
23 22 ralbidv z = y w = x t 0 1 t z + 1 t w A t 0 1 t y + 1 t x A
24 unitssre 0 1
25 24 11 sstri 0 1
26 simpr A J Conn x A y A x y s 0 1 s 0 1
27 25 26 sseldi A J Conn x A y A x y s 0 1 s
28 12 adantr A J Conn x A y A x y A
29 simpr2 A J Conn x A y A x y y A
30 28 29 sseldd A J Conn x A y A x y y
31 30 adantr A J Conn x A y A x y s 0 1 y
32 27 31 mulcld A J Conn x A y A x y s 0 1 s y
33 ax-1cn 1
34 subcl 1 s 1 s
35 33 27 34 sylancr A J Conn x A y A x y s 0 1 1 s
36 simpr1 A J Conn x A y A x y x A
37 28 36 sseldd A J Conn x A y A x y x
38 37 adantr A J Conn x A y A x y s 0 1 x
39 35 38 mulcld A J Conn x A y A x y s 0 1 1 s x
40 32 39 addcomd A J Conn x A y A x y s 0 1 s y + 1 s x = 1 s x + s y
41 nncan 1 s 1 1 s = s
42 33 27 41 sylancr A J Conn x A y A x y s 0 1 1 1 s = s
43 42 oveq1d A J Conn x A y A x y s 0 1 1 1 s y = s y
44 43 oveq2d A J Conn x A y A x y s 0 1 1 s x + 1 1 s y = 1 s x + s y
45 40 44 eqtr4d A J Conn x A y A x y s 0 1 s y + 1 s x = 1 s x + 1 1 s y
46 iirev s 0 1 1 s 0 1
47 46 adantl A J Conn x A y A x y s 0 1 1 s 0 1
48 1 eleq1i J Conn topGen ran . 𝑡 A Conn
49 reconn A topGen ran . 𝑡 A Conn x A y A x y A
50 48 49 syl5bb A J Conn x A y A x y A
51 50 biimpa A J Conn x A y A x y A
52 51 r19.21bi A J Conn x A y A x y A
53 52 r19.21bi A J Conn x A y A x y A
54 53 anasss A J Conn x A y A x y A
55 54 3adantr3 A J Conn x A y A x y x y A
56 55 adantr A J Conn x A y A x y t 0 1 x y A
57 simpr A J Conn x A y A x y t 0 1 t 0 1
58 24 57 sseldi A J Conn x A y A x y t 0 1 t
59 simplll A J Conn x A y A x y t 0 1 A
60 36 adantr A J Conn x A y A x y t 0 1 x A
61 59 60 sseldd A J Conn x A y A x y t 0 1 x
62 58 61 remulcld A J Conn x A y A x y t 0 1 t x
63 1re 1
64 resubcl 1 t 1 t
65 63 58 64 sylancr A J Conn x A y A x y t 0 1 1 t
66 29 adantr A J Conn x A y A x y t 0 1 y A
67 59 66 sseldd A J Conn x A y A x y t 0 1 y
68 65 67 remulcld A J Conn x A y A x y t 0 1 1 t y
69 62 68 readdcld A J Conn x A y A x y t 0 1 t x + 1 t y
70 58 recnd A J Conn x A y A x y t 0 1 t
71 pncan3 t 1 t + 1 - t = 1
72 70 33 71 sylancl A J Conn x A y A x y t 0 1 t + 1 - t = 1
73 72 oveq1d A J Conn x A y A x y t 0 1 t + 1 - t x = 1 x
74 65 recnd A J Conn x A y A x y t 0 1 1 t
75 37 adantr A J Conn x A y A x y t 0 1 x
76 70 74 75 adddird A J Conn x A y A x y t 0 1 t + 1 - t x = t x + 1 t x
77 75 mulid2d A J Conn x A y A x y t 0 1 1 x = x
78 73 76 77 3eqtr3d A J Conn x A y A x y t 0 1 t x + 1 t x = x
79 65 61 remulcld A J Conn x A y A x y t 0 1 1 t x
80 elicc01 t 0 1 t 0 t t 1
81 57 80 sylib A J Conn x A y A x y t 0 1 t 0 t t 1
82 81 simp3d A J Conn x A y A x y t 0 1 t 1
83 subge0 1 t 0 1 t t 1
84 63 58 83 sylancr A J Conn x A y A x y t 0 1 0 1 t t 1
85 82 84 mpbird A J Conn x A y A x y t 0 1 0 1 t
86 simplr3 A J Conn x A y A x y t 0 1 x y
87 61 67 65 85 86 lemul2ad A J Conn x A y A x y t 0 1 1 t x 1 t y
88 79 68 62 87 leadd2dd A J Conn x A y A x y t 0 1 t x + 1 t x t x + 1 t y
89 78 88 eqbrtrrd A J Conn x A y A x y t 0 1 x t x + 1 t y
90 58 67 remulcld A J Conn x A y A x y t 0 1 t y
91 81 simp2d A J Conn x A y A x y t 0 1 0 t
92 61 67 58 91 86 lemul2ad A J Conn x A y A x y t 0 1 t x t y
93 62 90 68 92 leadd1dd A J Conn x A y A x y t 0 1 t x + 1 t y t y + 1 t y
94 72 oveq1d A J Conn x A y A x y t 0 1 t + 1 - t y = 1 y
95 30 adantr A J Conn x A y A x y t 0 1 y
96 70 74 95 adddird A J Conn x A y A x y t 0 1 t + 1 - t y = t y + 1 t y
97 95 mulid2d A J Conn x A y A x y t 0 1 1 y = y
98 94 96 97 3eqtr3d A J Conn x A y A x y t 0 1 t y + 1 t y = y
99 93 98 breqtrd A J Conn x A y A x y t 0 1 t x + 1 t y y
100 elicc2 x y t x + 1 t y x y t x + 1 t y x t x + 1 t y t x + 1 t y y
101 61 67 100 syl2anc A J Conn x A y A x y t 0 1 t x + 1 t y x y t x + 1 t y x t x + 1 t y t x + 1 t y y
102 69 89 99 101 mpbir3and A J Conn x A y A x y t 0 1 t x + 1 t y x y
103 56 102 sseldd A J Conn x A y A x y t 0 1 t x + 1 t y A
104 103 ralrimiva A J Conn x A y A x y t 0 1 t x + 1 t y A
105 104 adantr A J Conn x A y A x y s 0 1 t 0 1 t x + 1 t y A
106 oveq1 t = 1 s t x = 1 s x
107 oveq2 t = 1 s 1 t = 1 1 s
108 107 oveq1d t = 1 s 1 t y = 1 1 s y
109 106 108 oveq12d t = 1 s t x + 1 t y = 1 s x + 1 1 s y
110 109 eleq1d t = 1 s t x + 1 t y A 1 s x + 1 1 s y A
111 110 rspcv 1 s 0 1 t 0 1 t x + 1 t y A 1 s x + 1 1 s y A
112 47 105 111 sylc A J Conn x A y A x y s 0 1 1 s x + 1 1 s y A
113 45 112 eqeltrd A J Conn x A y A x y s 0 1 s y + 1 s x A
114 113 ralrimiva A J Conn x A y A x y s 0 1 s y + 1 s x A
115 oveq1 s = t s y = t y
116 oveq2 s = t 1 s = 1 t
117 116 oveq1d s = t 1 s x = 1 t x
118 115 117 oveq12d s = t s y + 1 s x = t y + 1 t x
119 118 eleq1d s = t s y + 1 s x A t y + 1 t x A
120 119 cbvralvw s 0 1 s y + 1 s x A t 0 1 t y + 1 t x A
121 114 120 sylib A J Conn x A y A x y t 0 1 t y + 1 t x A
122 18 23 10 121 104 wloglei A J Conn x A y A t 0 1 t x + 1 t y A
123 122 r19.21bi A J Conn x A y A t 0 1 t x + 1 t y A
124 123 anasss A J Conn x A y A t 0 1 t x + 1 t y A
125 13 124 sylan2b A J Conn x A y A t 0 1 t x + 1 t y A
126 eqid TopOpen fld 𝑡 A = TopOpen fld 𝑡 A
127 12 125 5 126 cvxsconn A J Conn TopOpen fld 𝑡 A SConn
128 9 127 eqeltrrd A J Conn J SConn
129 128 ex A J Conn J SConn
130 4 129 impbid2 A J SConn J Conn