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 
|- ( ph -> S C_ CC )
cvxpconn.2 
|- ( ( ph /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
cvxpconn.3 
|- J = ( TopOpen ` CCfld )
cvxpconn.4 
|- K = ( J |`t S )
Assertion cvxpconn 
|- ( ph -> K e. PConn )

Proof

Step Hyp Ref Expression
1 cvxpconn.1 
 |-  ( ph -> S C_ CC )
2 cvxpconn.2 
 |-  ( ( ph /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
3 cvxpconn.3 
 |-  J = ( TopOpen ` CCfld )
4 cvxpconn.4 
 |-  K = ( J |`t S )
5 3 cnfldtop 
 |-  J e. Top
6 cnex 
 |-  CC e. _V
7 ssexg 
 |-  ( ( S C_ CC /\ CC e. _V ) -> S e. _V )
8 1 6 7 sylancl 
 |-  ( ph -> S e. _V )
9 resttop 
 |-  ( ( J e. Top /\ S e. _V ) -> ( J |`t S ) e. Top )
10 5 8 9 sylancr 
 |-  ( ph -> ( J |`t S ) e. Top )
11 4 10 eqeltrid 
 |-  ( ph -> K e. Top )
12 3 dfii3 
 |-  II = ( J |`t ( 0 [,] 1 ) )
13 3 cnfldtopon 
 |-  J e. ( TopOn ` CC )
14 13 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> J e. ( TopOn ` CC ) )
15 unitssre 
 |-  ( 0 [,] 1 ) C_ RR
16 ax-resscn 
 |-  RR C_ CC
17 15 16 sstri 
 |-  ( 0 [,] 1 ) C_ CC
18 17 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 [,] 1 ) C_ CC )
19 14 cnmptid 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> t ) e. ( J Cn J ) )
20 1 adantr 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> S C_ CC )
21 simprr 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> x e. S )
22 20 21 sseldd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> x e. CC )
23 14 14 22 cnmptc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> x ) e. ( J Cn J ) )
24 3 mulcn 
 |-  x. e. ( ( J tX J ) Cn J )
25 24 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> x. e. ( ( J tX J ) Cn J ) )
26 14 19 23 25 cnmpt12f 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( t x. x ) ) e. ( J Cn J ) )
27 1cnd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> 1 e. CC )
28 14 14 27 cnmptc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> 1 ) e. ( J Cn J ) )
29 3 subcn 
 |-  - e. ( ( J tX J ) Cn J )
30 29 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> - e. ( ( J tX J ) Cn J ) )
31 14 28 19 30 cnmpt12f 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( 1 - t ) ) e. ( J Cn J ) )
32 simprl 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> y e. S )
33 20 32 sseldd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> y e. CC )
34 14 14 33 cnmptc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> y ) e. ( J Cn J ) )
35 14 31 34 25 cnmpt12f 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( ( 1 - t ) x. y ) ) e. ( J Cn J ) )
36 3 addcn 
 |-  + e. ( ( J tX J ) Cn J )
37 36 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> + e. ( ( J tX J ) Cn J ) )
38 14 26 35 37 cnmpt12f 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( J Cn J ) )
39 12 14 18 38 cnmpt1res 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn J ) )
40 2 3exp2 
 |-  ( ph -> ( x e. S -> ( y e. S -> ( t e. ( 0 [,] 1 ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S ) ) ) )
41 40 com23 
 |-  ( ph -> ( y e. S -> ( x e. S -> ( t e. ( 0 [,] 1 ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S ) ) ) )
42 41 imp42 
 |-  ( ( ( ph /\ ( y e. S /\ x e. S ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
43 42 fmpttd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) : ( 0 [,] 1 ) --> S )
44 43 frnd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ran ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) C_ S )
45 cnrest2 
 |-  ( ( J e. ( TopOn ` CC ) /\ ran ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) C_ S /\ S C_ CC ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn J ) <-> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn ( J |`t S ) ) ) )
46 14 44 20 45 syl3anc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn J ) <-> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn ( J |`t S ) ) ) )
47 39 46 mpbid 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn ( J |`t S ) ) )
48 4 oveq2i 
 |-  ( II Cn K ) = ( II Cn ( J |`t S ) )
49 47 48 eleqtrrdi 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn K ) )
50 0elunit 
 |-  0 e. ( 0 [,] 1 )
51 oveq1 
 |-  ( t = 0 -> ( t x. x ) = ( 0 x. x ) )
52 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
53 1m0e1 
 |-  ( 1 - 0 ) = 1
54 52 53 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
55 54 oveq1d 
 |-  ( t = 0 -> ( ( 1 - t ) x. y ) = ( 1 x. y ) )
56 51 55 oveq12d 
 |-  ( t = 0 -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) = ( ( 0 x. x ) + ( 1 x. y ) ) )
57 eqid 
 |-  ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) )
58 ovex 
 |-  ( ( 0 x. x ) + ( 1 x. y ) ) e. _V
59 56 57 58 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = ( ( 0 x. x ) + ( 1 x. y ) ) )
60 50 59 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = ( ( 0 x. x ) + ( 1 x. y ) )
61 22 mul02d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 x. x ) = 0 )
62 33 mulid2d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 1 x. y ) = y )
63 61 62 oveq12d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 0 x. x ) + ( 1 x. y ) ) = ( 0 + y ) )
64 33 addid2d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 + y ) = y )
65 63 64 eqtrd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 0 x. x ) + ( 1 x. y ) ) = y )
66 60 65 syl5eq 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = y )
67 1elunit 
 |-  1 e. ( 0 [,] 1 )
68 oveq1 
 |-  ( t = 1 -> ( t x. x ) = ( 1 x. x ) )
69 oveq2 
 |-  ( t = 1 -> ( 1 - t ) = ( 1 - 1 ) )
70 1m1e0 
 |-  ( 1 - 1 ) = 0
71 69 70 eqtrdi 
 |-  ( t = 1 -> ( 1 - t ) = 0 )
72 71 oveq1d 
 |-  ( t = 1 -> ( ( 1 - t ) x. y ) = ( 0 x. y ) )
73 68 72 oveq12d 
 |-  ( t = 1 -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) = ( ( 1 x. x ) + ( 0 x. y ) ) )
74 ovex 
 |-  ( ( 1 x. x ) + ( 0 x. y ) ) e. _V
75 73 57 74 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = ( ( 1 x. x ) + ( 0 x. y ) ) )
76 67 75 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = ( ( 1 x. x ) + ( 0 x. y ) )
77 22 mulid2d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 1 x. x ) = x )
78 33 mul02d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 x. y ) = 0 )
79 77 78 oveq12d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 1 x. x ) + ( 0 x. y ) ) = ( x + 0 ) )
80 22 addid1d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( x + 0 ) = x )
81 79 80 eqtrd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 1 x. x ) + ( 0 x. y ) ) = x )
82 76 81 syl5eq 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = x )
83 fveq1 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) -> ( f ` 0 ) = ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) )
84 83 eqeq1d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) -> ( ( f ` 0 ) = y <-> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = y ) )
85 fveq1 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) -> ( f ` 1 ) = ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) )
86 85 eqeq1d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) -> ( ( f ` 1 ) = x <-> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = x ) )
87 84 86 anbi12d 
 |-  ( f = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) -> ( ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) <-> ( ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = y /\ ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = x ) ) )
88 87 rspcev 
 |-  ( ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn K ) /\ ( ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = y /\ ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = x ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
89 49 66 82 88 syl12anc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
90 89 ralrimivva 
 |-  ( ph -> A. y e. S A. x e. S E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
91 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ S C_ CC ) -> ( J |`t S ) e. ( TopOn ` S ) )
92 13 1 91 sylancr 
 |-  ( ph -> ( J |`t S ) e. ( TopOn ` S ) )
93 4 92 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` S ) )
94 toponuni 
 |-  ( K e. ( TopOn ` S ) -> S = U. K )
95 93 94 syl 
 |-  ( ph -> S = U. K )
96 95 raleqdv 
 |-  ( ph -> ( A. x e. S E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) <-> A. x e. U. K E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) ) )
97 95 96 raleqbidv 
 |-  ( ph -> ( A. y e. S A. x e. S E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) <-> A. y e. U. K A. x e. U. K E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) ) )
98 90 97 mpbid 
 |-  ( ph -> A. y e. U. K A. x e. U. K E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
99 eqid 
 |-  U. K = U. K
100 99 ispconn 
 |-  ( K e. PConn <-> ( K e. Top /\ A. y e. U. K A. x e. U. K E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) ) )
101 11 98 100 sylanbrc 
 |-  ( ph -> K e. PConn )