Metamath Proof Explorer


Theorem cvxpconn

Description: A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses cvxpconn.1 φS
cvxpconn.2 φxSySt01tx+1tyS
cvxpconn.3 J=TopOpenfld
cvxpconn.4 K=J𝑡S
Assertion cvxpconn φKPConn

Proof

Step Hyp Ref Expression
1 cvxpconn.1 φS
2 cvxpconn.2 φxSySt01tx+1tyS
3 cvxpconn.3 J=TopOpenfld
4 cvxpconn.4 K=J𝑡S
5 3 cnfldtop JTop
6 cnex V
7 ssexg SVSV
8 1 6 7 sylancl φSV
9 resttop JTopSVJ𝑡STop
10 5 8 9 sylancr φJ𝑡STop
11 4 10 eqeltrid φKTop
12 3 dfii3 II=J𝑡01
13 3 cnfldtopon JTopOn
14 13 a1i φySxSJTopOn
15 unitssre 01
16 ax-resscn
17 15 16 sstri 01
18 17 a1i φySxS01
19 14 cnmptid φySxSttJCnJ
20 1 adantr φySxSS
21 simprr φySxSxS
22 20 21 sseldd φySxSx
23 14 14 22 cnmptc φySxStxJCnJ
24 3 mulcn ×J×tJCnJ
25 24 a1i φySxS×J×tJCnJ
26 14 19 23 25 cnmpt12f φySxSttxJCnJ
27 1cnd φySxS1
28 14 14 27 cnmptc φySxSt1JCnJ
29 3 subcn J×tJCnJ
30 29 a1i φySxSJ×tJCnJ
31 14 28 19 30 cnmpt12f φySxSt1tJCnJ
32 simprl φySxSyS
33 20 32 sseldd φySxSy
34 14 14 33 cnmptc φySxStyJCnJ
35 14 31 34 25 cnmpt12f φySxSt1tyJCnJ
36 3 addcn +J×tJCnJ
37 36 a1i φySxS+J×tJCnJ
38 14 26 35 37 cnmpt12f φySxSttx+1tyJCnJ
39 12 14 18 38 cnmpt1res φySxSt01tx+1tyIICnJ
40 2 3exp2 φxSySt01tx+1tyS
41 40 com23 φySxSt01tx+1tyS
42 41 imp42 φySxSt01tx+1tyS
43 42 fmpttd φySxSt01tx+1ty:01S
44 43 frnd φySxSrant01tx+1tyS
45 cnrest2 JTopOnrant01tx+1tySSt01tx+1tyIICnJt01tx+1tyIICnJ𝑡S
46 14 44 20 45 syl3anc φySxSt01tx+1tyIICnJt01tx+1tyIICnJ𝑡S
47 39 46 mpbid φySxSt01tx+1tyIICnJ𝑡S
48 4 oveq2i IICnK=IICnJ𝑡S
49 47 48 eleqtrrdi φySxSt01tx+1tyIICnK
50 0elunit 001
51 oveq1 t=0tx=0x
52 oveq2 t=01t=10
53 1m0e1 10=1
54 52 53 eqtrdi t=01t=1
55 54 oveq1d t=01ty=1y
56 51 55 oveq12d t=0tx+1ty=0x+1y
57 eqid t01tx+1ty=t01tx+1ty
58 ovex 0x+1yV
59 56 57 58 fvmpt 001t01tx+1ty0=0x+1y
60 50 59 ax-mp t01tx+1ty0=0x+1y
61 22 mul02d φySxS0x=0
62 33 mulid2d φySxS1y=y
63 61 62 oveq12d φySxS0x+1y=0+y
64 33 addid2d φySxS0+y=y
65 63 64 eqtrd φySxS0x+1y=y
66 60 65 eqtrid φySxSt01tx+1ty0=y
67 1elunit 101
68 oveq1 t=1tx=1x
69 oveq2 t=11t=11
70 1m1e0 11=0
71 69 70 eqtrdi t=11t=0
72 71 oveq1d t=11ty=0y
73 68 72 oveq12d t=1tx+1ty=1x+0y
74 ovex 1x+0yV
75 73 57 74 fvmpt 101t01tx+1ty1=1x+0y
76 67 75 ax-mp t01tx+1ty1=1x+0y
77 22 mulid2d φySxS1x=x
78 33 mul02d φySxS0y=0
79 77 78 oveq12d φySxS1x+0y=x+0
80 22 addid1d φySxSx+0=x
81 79 80 eqtrd φySxS1x+0y=x
82 76 81 eqtrid φySxSt01tx+1ty1=x
83 fveq1 f=t01tx+1tyf0=t01tx+1ty0
84 83 eqeq1d f=t01tx+1tyf0=yt01tx+1ty0=y
85 fveq1 f=t01tx+1tyf1=t01tx+1ty1
86 85 eqeq1d f=t01tx+1tyf1=xt01tx+1ty1=x
87 84 86 anbi12d f=t01tx+1tyf0=yf1=xt01tx+1ty0=yt01tx+1ty1=x
88 87 rspcev t01tx+1tyIICnKt01tx+1ty0=yt01tx+1ty1=xfIICnKf0=yf1=x
89 49 66 82 88 syl12anc φySxSfIICnKf0=yf1=x
90 89 ralrimivva φySxSfIICnKf0=yf1=x
91 resttopon JTopOnSJ𝑡STopOnS
92 13 1 91 sylancr φJ𝑡STopOnS
93 4 92 eqeltrid φKTopOnS
94 toponuni KTopOnSS=K
95 93 94 syl φS=K
96 95 raleqdv φxSfIICnKf0=yf1=xxKfIICnKf0=yf1=x
97 95 96 raleqbidv φySxSfIICnKf0=yf1=xyKxKfIICnKf0=yf1=x
98 90 97 mpbid φyKxKfIICnKf0=yf1=x
99 eqid K=K
100 99 ispconn KPConnKTopyKxKfIICnKf0=yf1=x
101 11 98 100 sylanbrc φKPConn