Metamath Proof Explorer

Theorem cvxpconn

Description: A convex subset of the complex numbers is path-connected. (Contributed by Mario Carneiro, 12-Feb-2015) Avoid ax-mulf . (Revised by GG, 19-Apr-2025)

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 unitsscn 
 |-  ( 0 [,] 1 ) C_ CC
16 15 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 [,] 1 ) C_ CC )
17 13 a1i 
 |-  ( ( ph /\ x e. S ) -> J e. ( TopOn ` CC ) )
18 17 cnmptid 
 |-  ( ( ph /\ x e. S ) -> ( t e. CC |-> t ) e. ( J Cn J ) )
19 1 sselda 
 |-  ( ( ph /\ x e. S ) -> x e. CC )
20 17 17 19 cnmptc 
 |-  ( ( ph /\ x e. S ) -> ( t e. CC |-> x ) e. ( J Cn J ) )
21 3 mpomulcn 
 |-  ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J )
22 21 a1i 
 |-  ( ( ph /\ x e. S ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J ) )
23 oveq12 
 |-  ( ( u = t /\ v = x ) -> ( u x. v ) = ( t x. x ) )
24 17 18 20 17 17 22 23 cnmpt12 
 |-  ( ( ph /\ x e. S ) -> ( t e. CC |-> ( t x. x ) ) e. ( J Cn J ) )
25 24 adantrl 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( t x. x ) ) e. ( J Cn J ) )
26 13 a1i 
 |-  ( ph -> J e. ( TopOn ` CC ) )
27 1cnd 
 |-  ( ph -> 1 e. CC )
28 26 26 27 cnmptc 
 |-  ( ph -> ( t e. CC |-> 1 ) e. ( J Cn J ) )
29 3 cncfcn1 
 |-  ( CC -cn-> CC ) = ( J Cn J )
30 28 29 eleqtrrdi 
 |-  ( ph -> ( t e. CC |-> 1 ) e. ( CC -cn-> CC ) )
31 26 cnmptid 
 |-  ( ph -> ( t e. CC |-> t ) e. ( J Cn J ) )
32 31 29 eleqtrrdi 
 |-  ( ph -> ( t e. CC |-> t ) e. ( CC -cn-> CC ) )
33 30 32 subcncf 
 |-  ( ph -> ( t e. CC |-> ( 1 - t ) ) e. ( CC -cn-> CC ) )
34 33 29 eleqtrdi 
 |-  ( ph -> ( t e. CC |-> ( 1 - t ) ) e. ( J Cn J ) )
35 34 adantr 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( 1 - t ) ) e. ( J Cn J ) )
36 1 adantr 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> S C_ CC )
37 simprl 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> y e. S )
38 36 37 sseldd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> y e. CC )
39 14 14 38 cnmptc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> y ) e. ( J Cn J ) )
40 21 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( u e. CC , v e. CC |-> ( u x. v ) ) e. ( ( J tX J ) Cn J ) )
41 oveq12 
 |-  ( ( u = ( 1 - t ) /\ v = y ) -> ( u x. v ) = ( ( 1 - t ) x. y ) )
42 14 35 39 14 14 40 41 cnmpt12 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( ( 1 - t ) x. y ) ) e. ( J Cn J ) )
43 3 addcn 
 |-  + e. ( ( J tX J ) Cn J )
44 43 a1i 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> + e. ( ( J tX J ) Cn J ) )
45 14 25 42 44 cnmpt12f 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. CC |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( J Cn J ) )
46 12 14 16 45 cnmpt1res 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn J ) )
47 2 3exp2 
 |-  ( ph -> ( x e. S -> ( y e. S -> ( t e. ( 0 [,] 1 ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S ) ) ) )
48 47 com23 
 |-  ( ph -> ( y e. S -> ( x e. S -> ( t e. ( 0 [,] 1 ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S ) ) ) )
49 48 imp42 
 |-  ( ( ( ph /\ ( y e. S /\ x e. S ) ) /\ t e. ( 0 [,] 1 ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
50 49 fmpttd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) : ( 0 [,] 1 ) --> S )
51 50 frnd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ran ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) C_ S )
52 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 ) ) ) )
53 13 51 36 52 mp3an2i 
 |-  ( ( 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 ) ) ) )
54 46 53 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 ) ) )
55 4 oveq2i 
 |-  ( II Cn K ) = ( II Cn ( J |`t S ) )
56 54 55 eleqtrrdi 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) e. ( II Cn K ) )
57 0elunit 
 |-  0 e. ( 0 [,] 1 )
58 oveq1 
 |-  ( t = 0 -> ( t x. x ) = ( 0 x. x ) )
59 oveq2 
 |-  ( t = 0 -> ( 1 - t ) = ( 1 - 0 ) )
60 1m0e1 
 |-  ( 1 - 0 ) = 1
61 59 60 eqtrdi 
 |-  ( t = 0 -> ( 1 - t ) = 1 )
62 61 oveq1d 
 |-  ( t = 0 -> ( ( 1 - t ) x. y ) = ( 1 x. y ) )
63 58 62 oveq12d 
 |-  ( t = 0 -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) = ( ( 0 x. x ) + ( 1 x. y ) ) )
64 eqid 
 |-  ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) = ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) )
65 ovex 
 |-  ( ( 0 x. x ) + ( 1 x. y ) ) e. _V
66 63 64 65 fvmpt 
 |-  ( 0 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = ( ( 0 x. x ) + ( 1 x. y ) ) )
67 57 66 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = ( ( 0 x. x ) + ( 1 x. y ) )
68 19 adantrl 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> x e. CC )
69 68 mul02d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 x. x ) = 0 )
70 38 mullidd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 1 x. y ) = y )
71 69 70 oveq12d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 0 x. x ) + ( 1 x. y ) ) = ( 0 + y ) )
72 38 addlidd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 + y ) = y )
73 71 72 eqtrd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 0 x. x ) + ( 1 x. y ) ) = y )
74 67 73 eqtrid 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 0 ) = y )
75 1elunit 
 |-  1 e. ( 0 [,] 1 )
76 oveq1 
 |-  ( t = 1 -> ( t x. x ) = ( 1 x. x ) )
77 oveq2 
 |-  ( t = 1 -> ( 1 - t ) = ( 1 - 1 ) )
78 1m1e0 
 |-  ( 1 - 1 ) = 0
79 77 78 eqtrdi 
 |-  ( t = 1 -> ( 1 - t ) = 0 )
80 79 oveq1d 
 |-  ( t = 1 -> ( ( 1 - t ) x. y ) = ( 0 x. y ) )
81 76 80 oveq12d 
 |-  ( t = 1 -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) = ( ( 1 x. x ) + ( 0 x. y ) ) )
82 ovex 
 |-  ( ( 1 x. x ) + ( 0 x. y ) ) e. _V
83 81 64 82 fvmpt 
 |-  ( 1 e. ( 0 [,] 1 ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = ( ( 1 x. x ) + ( 0 x. y ) ) )
84 75 83 ax-mp 
 |-  ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = ( ( 1 x. x ) + ( 0 x. y ) )
85 68 mullidd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 1 x. x ) = x )
86 38 mul02d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( 0 x. y ) = 0 )
87 85 86 oveq12d 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 1 x. x ) + ( 0 x. y ) ) = ( x + 0 ) )
88 68 addridd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( x + 0 ) = x )
89 87 88 eqtrd 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( 1 x. x ) + ( 0 x. y ) ) = x )
90 84 89 eqtrid 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> ( ( t e. ( 0 [,] 1 ) |-> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) ) ` 1 ) = x )
91 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 ) )
92 91 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 ) )
93 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 ) )
94 93 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 ) )
95 92 94 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 ) ) )
96 95 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 ) )
97 56 74 90 96 syl12anc 
 |-  ( ( ph /\ ( y e. S /\ x e. S ) ) -> E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
98 97 ralrimivva 
 |-  ( ph -> A. y e. S A. x e. S E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
99 resttopon 
 |-  ( ( J e. ( TopOn ` CC ) /\ S C_ CC ) -> ( J |`t S ) e. ( TopOn ` S ) )
100 13 1 99 sylancr 
 |-  ( ph -> ( J |`t S ) e. ( TopOn ` S ) )
101 4 100 eqeltrid 
 |-  ( ph -> K e. ( TopOn ` S ) )
102 toponuni 
 |-  ( K e. ( TopOn ` S ) -> S = U. K )
103 101 102 syl 
 |-  ( ph -> S = U. K )
104 103 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 ) ) )
105 103 104 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 ) ) )
106 98 105 mpbid 
 |-  ( ph -> A. y e. U. K A. x e. U. K E. f e. ( II Cn K ) ( ( f ` 0 ) = y /\ ( f ` 1 ) = x ) )
107 eqid 
 |-  U. K = U. K
108 107 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 ) ) )
109 11 106 108 sylanbrc 
 |-  ( ph -> K e. PConn )