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	$⊢ φ \to S \subseteq ℂ$
	cvxpconn.2	$⊢ (φ \land (x \in S \land y \in S \land t \in [0, 1])) \to t x + (1 - t) y \in S$
	cvxpconn.3	$⊢ J = TopOpen (ℂ_{fld})$
	cvxpconn.4	$⊢ K = J ↾_{𝑡} S$
Assertion	cvxpconn	$⊢ φ \to K \in PConn$

Proof

Step	Hyp	Ref	Expression
1		cvxpconn.1	$⊢ φ \to S \subseteq ℂ$
2		cvxpconn.2	$⊢ (φ \land (x \in S \land y \in S \land t \in [0, 1])) \to t x + (1 - t) y \in S$
3		cvxpconn.3	$⊢ J = TopOpen (ℂ_{fld})$
4		cvxpconn.4	$⊢ K = J ↾_{𝑡} S$
5	3	cnfldtop	$⊢ J \in Top$
6		cnex	$⊢ ℂ \in V$
7		ssexg	$⊢ (S \subseteq ℂ \land ℂ \in V) \to S \in V$
8	1 6 7	sylancl	$⊢ φ \to S \in V$
9		resttop	$⊢ (J \in Top \land S \in V) \to J ↾_{𝑡} S \in Top$
10	5 8 9	sylancr	$⊢ φ \to J ↾_{𝑡} S \in Top$
11	4 10	eqeltrid	$⊢ φ \to K \in Top$
12	3	dfii3	$⊢ II = J ↾_{𝑡} [0, 1]$
13	3	cnfldtopon	$⊢ J \in TopOn (ℂ)$
14	13	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to J \in TopOn (ℂ)$
15		unitsscn	$⊢ [0, 1] \subseteq ℂ$
16	15	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to [0, 1] \subseteq ℂ$
17	13	a1i	$⊢ (φ \land x \in S) \to J \in TopOn (ℂ)$
18	17	cnmptid	$⊢ (φ \land x \in S) \to (t \in ℂ ⟼ t) \in (J Cn J)$
19	1	sselda	$⊢ (φ \land x \in S) \to x \in ℂ$
20	17 17 19	cnmptc	$⊢ (φ \land x \in S) \to (t \in ℂ ⟼ x) \in (J Cn J)$
21	3	mpomulcn	$⊢ (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
22	21	a1i	$⊢ (φ \land x \in S) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
23		oveq12	$⊢ (u = t \land v = x) \to u v = t x$
24	17 18 20 17 17 22 23	cnmpt12	$⊢ (φ \land x \in S) \to (t \in ℂ ⟼ t x) \in (J Cn J)$
25	24	adantrl	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ t x) \in (J Cn J)$
26	13	a1i	$⊢ φ \to J \in TopOn (ℂ)$
27		1cnd	$⊢ φ \to 1 \in ℂ$
28	26 26 27	cnmptc	$⊢ φ \to (t \in ℂ ⟼ 1) \in (J Cn J)$
29	3	cncfcn1	$⊢ ℂ \underset{cn}{⟶} ℂ = J Cn J$
30	28 29	eleqtrrdi	$⊢ φ \to (t \in ℂ ⟼ 1) : ℂ \underset{cn}{⟶} ℂ$
31	26	cnmptid	$⊢ φ \to (t \in ℂ ⟼ t) \in (J Cn J)$
32	31 29	eleqtrrdi	$⊢ φ \to (t \in ℂ ⟼ t) : ℂ \underset{cn}{⟶} ℂ$
33	30 32	subcncf	$⊢ φ \to (t \in ℂ ⟼ 1 - t) : ℂ \underset{cn}{⟶} ℂ$
34	33 29	eleqtrdi	$⊢ φ \to (t \in ℂ ⟼ 1 - t) \in (J Cn J)$
35	34	adantr	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ 1 - t) \in (J Cn J)$
36	1	adantr	$⊢ (φ \land (y \in S \land x \in S)) \to S \subseteq ℂ$
37		simprl	$⊢ (φ \land (y \in S \land x \in S)) \to y \in S$
38	36 37	sseldd	$⊢ (φ \land (y \in S \land x \in S)) \to y \in ℂ$
39	14 14 38	cnmptc	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ y) \in (J Cn J)$
40	21	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to (u \in ℂ, v \in ℂ ⟼ u v) \in ((J \times_{t} J) Cn J)$
41		oveq12	$⊢ (u = 1 - t \land v = y) \to u v = (1 - t) y$
42	14 35 39 14 14 40 41	cnmpt12	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ (1 - t) y) \in (J Cn J)$
43	3	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
44	43	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to + \in ((J \times_{t} J) Cn J)$
45	14 25 42 44	cnmpt12f	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ t x + (1 - t) y) \in (J Cn J)$
46	12 14 16 45	cnmpt1res	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn J)$
47	2	3exp2	$⊢ φ \to (x \in S \to (y \in S \to (t \in [0, 1] \to t x + (1 - t) y \in S)))$
48	47	com23	$⊢ φ \to (y \in S \to (x \in S \to (t \in [0, 1] \to t x + (1 - t) y \in S)))$
49	48	imp42	$⊢ ((φ \land (y \in S \land x \in S)) \land t \in [0, 1]) \to t x + (1 - t) y \in S$
50	49	fmpttd	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) : [0, 1] ⟶ S$
51	50	frnd	$⊢ (φ \land (y \in S \land x \in S)) \to ran (t \in [0, 1] ⟼ t x + (1 - t) y) \subseteq S$
52		cnrest2	$⊢ (J \in TopOn (ℂ) \land ran (t \in [0, 1] ⟼ t x + (1 - t) y) \subseteq S \land S \subseteq ℂ) \to ((t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn J) \leftrightarrow (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn (J ↾_{𝑡} S)))$
53	13 51 36 52	mp3an2i	$⊢ (φ \land (y \in S \land x \in S)) \to ((t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn J) \leftrightarrow (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn (J ↾_{𝑡} S)))$
54	46 53	mpbid	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn (J ↾_{𝑡} S))$
55	4	oveq2i	$⊢ II Cn K = II Cn (J ↾_{𝑡} S)$
56	54 55	eleqtrrdi	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn K)$
57		0elunit	$⊢ 0 \in [0, 1]$
58		oveq1	$⊢ t = 0 \to t x = 0 \cdot x$
59		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
60		1m0e1	$⊢ 1 - 0 = 1$
61	59 60	eqtrdi	$⊢ t = 0 \to 1 - t = 1$
62	61	oveq1d	$⊢ t = 0 \to (1 - t) y = 1 y$
63	58 62	oveq12d	$⊢ t = 0 \to t x + (1 - t) y = 0 \cdot x + 1 y$
64		eqid	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) = (t \in [0, 1] ⟼ t x + (1 - t) y)$
65		ovex	$⊢ 0 \cdot x + 1 y \in V$
66	63 64 65	fvmpt	$⊢ 0 \in [0, 1] \to (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = 0 \cdot x + 1 y$
67	57 66	ax-mp	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = 0 \cdot x + 1 y$
68	19	adantrl	$⊢ (φ \land (y \in S \land x \in S)) \to x \in ℂ$
69	68	mul02d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x = 0$
70	38	mullidd	$⊢ (φ \land (y \in S \land x \in S)) \to 1 y = y$
71	69 70	oveq12d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x + 1 y = 0 + y$
72	38	addlidd	$⊢ (φ \land (y \in S \land x \in S)) \to 0 + y = y$
73	71 72	eqtrd	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x + 1 y = y$
74	67 73	eqtrid	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = y$
75		1elunit	$⊢ 1 \in [0, 1]$
76		oveq1	$⊢ t = 1 \to t x = 1 x$
77		oveq2	$⊢ t = 1 \to 1 - t = 1 - 1$
78		1m1e0	$⊢ 1 - 1 = 0$
79	77 78	eqtrdi	$⊢ t = 1 \to 1 - t = 0$
80	79	oveq1d	$⊢ t = 1 \to (1 - t) y = 0 \cdot y$
81	76 80	oveq12d	$⊢ t = 1 \to t x + (1 - t) y = 1 x + 0 \cdot y$
82		ovex	$⊢ 1 x + 0 \cdot y \in V$
83	81 64 82	fvmpt	$⊢ 1 \in [0, 1] \to (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = 1 x + 0 \cdot y$
84	75 83	ax-mp	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = 1 x + 0 \cdot y$
85	68	mullidd	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x = x$
86	38	mul02d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot y = 0$
87	85 86	oveq12d	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x + 0 \cdot y = x + 0$
88	68	addridd	$⊢ (φ \land (y \in S \land x \in S)) \to x + 0 = x$
89	87 88	eqtrd	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x + 0 \cdot y = x$
90	84 89	eqtrid	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = x$
91		fveq1	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to f (0) = (t \in [0, 1] ⟼ t x + (1 - t) y) (0)$
92	91	eqeq1d	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to (f (0) = y \leftrightarrow (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = y)$
93		fveq1	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to f (1) = (t \in [0, 1] ⟼ t x + (1 - t) y) (1)$
94	93	eqeq1d	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to (f (1) = x \leftrightarrow (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = x)$
95	92 94	anbi12d	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to ((f (0) = y \land f (1) = x) \leftrightarrow ((t \in [0, 1] ⟼ t x + (1 - t) y) (0) = y \land (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = x))$
96	95	rspcev	$⊢ ((t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn K) \land ((t \in [0, 1] ⟼ t x + (1 - t) y) (0) = y \land (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = x)) \to \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
97	56 74 90 96	syl12anc	$⊢ (φ \land (y \in S \land x \in S)) \to \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
98	97	ralrimivva	$⊢ φ \to \forall y \in S \forall x \in S \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
99		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
100	13 1 99	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
101	4 100	eqeltrid	$⊢ φ \to K \in TopOn (S)$
102		toponuni	$⊢ K \in TopOn (S) \to S = ⋃ K$
103	101 102	syl	$⊢ φ \to S = ⋃ K$
104	103	raleqdv	$⊢ φ \to (\forall x \in S \exists f \in (II Cn K) (f (0) = y \land f (1) = x) \leftrightarrow \forall x \in ⋃ K \exists f \in (II Cn K) (f (0) = y \land f (1) = x))$
105	103 104	raleqbidv	$⊢ φ \to (\forall y \in S \forall x \in S \exists f \in (II Cn K) (f (0) = y \land f (1) = x) \leftrightarrow \forall y \in ⋃ K \forall x \in ⋃ K \exists f \in (II Cn K) (f (0) = y \land f (1) = x))$
106	98 105	mpbid	$⊢ φ \to \forall y \in ⋃ K \forall x \in ⋃ K \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
107		eqid	$⊢ ⋃ K = ⋃ K$
108	107	ispconn	$⊢ K \in PConn \leftrightarrow (K \in Top \land \forall y \in ⋃ K \forall x \in ⋃ K \exists f \in (II Cn K) (f (0) = y \land f (1) = x))$
109	11 106 108	sylanbrc	$⊢ φ \to K \in PConn$

Metamath Proof Explorer

Theorem cvxpconn

Proof