cvxpconn

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

	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		unitssre	$⊢ [0, 1] \subseteq ℝ$
16		ax-resscn	$⊢ ℝ \subseteq ℂ$
17	15 16	sstri	$⊢ [0, 1] \subseteq ℂ$
18	17	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to [0, 1] \subseteq ℂ$
19	14	cnmptid	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ t) \in (J Cn J)$
20	1	adantr	$⊢ (φ \land (y \in S \land x \in S)) \to S \subseteq ℂ$
21		simprr	$⊢ (φ \land (y \in S \land x \in S)) \to x \in S$
22	20 21	sseldd	$⊢ (φ \land (y \in S \land x \in S)) \to x \in ℂ$
23	14 14 22	cnmptc	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ x) \in (J Cn J)$
24	3	mulcn	$⊢ \times \in ((J \times_{t} J) Cn J)$
25	24	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to \times \in ((J \times_{t} J) Cn J)$
26	14 19 23 25	cnmpt12f	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ t x) \in (J Cn J)$
27		1cnd	$⊢ (φ \land (y \in S \land x \in S)) \to 1 \in ℂ$
28	14 14 27	cnmptc	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ 1) \in (J Cn J)$
29	3	subcn	$⊢ - \in ((J \times_{t} J) Cn J)$
30	29	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to - \in ((J \times_{t} J) Cn J)$
31	14 28 19 30	cnmpt12f	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ 1 - t) \in (J Cn J)$
32		simprl	$⊢ (φ \land (y \in S \land x \in S)) \to y \in S$
33	20 32	sseldd	$⊢ (φ \land (y \in S \land x \in S)) \to y \in ℂ$
34	14 14 33	cnmptc	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ y) \in (J Cn J)$
35	14 31 34 25	cnmpt12f	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ (1 - t) y) \in (J Cn J)$
36	3	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
37	36	a1i	$⊢ (φ \land (y \in S \land x \in S)) \to + \in ((J \times_{t} J) Cn J)$
38	14 26 35 37	cnmpt12f	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in ℂ ⟼ t x + (1 - t) y) \in (J Cn J)$
39	12 14 18 38	cnmpt1res	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn J)$
40	2	3exp2	$⊢ φ \to (x \in S \to (y \in S \to (t \in [0, 1] \to t x + (1 - t) y \in S)))$
41	40	com23	$⊢ φ \to (y \in S \to (x \in S \to (t \in [0, 1] \to t x + (1 - t) y \in S)))$
42	41	imp42	$⊢ ((φ \land (y \in S \land x \in S)) \land t \in [0, 1]) \to t x + (1 - t) y \in S$
43	42	fmpttd	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) : [0, 1] ⟶ S$
44	43	frnd	$⊢ (φ \land (y \in S \land x \in S)) \to ran (t \in [0, 1] ⟼ t x + (1 - t) y) \subseteq S$
45		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)))$
46	14 44 20 45	syl3anc	$⊢ (φ \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)))$
47	39 46	mpbid	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn (J ↾_{𝑡} S))$
48	4	oveq2i	$⊢ II Cn K = II Cn (J ↾_{𝑡} S)$
49	47 48	eleqtrrdi	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) \in (II Cn K)$
50		0elunit	$⊢ 0 \in [0, 1]$
51		oveq1	$⊢ t = 0 \to t x = 0 \cdot x$
52		oveq2	$⊢ t = 0 \to 1 - t = 1 - 0$
53		1m0e1	$⊢ 1 - 0 = 1$
54	52 53	eqtrdi	$⊢ t = 0 \to 1 - t = 1$
55	54	oveq1d	$⊢ t = 0 \to (1 - t) y = 1 y$
56	51 55	oveq12d	$⊢ t = 0 \to t x + (1 - t) y = 0 \cdot x + 1 y$
57		eqid	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) = (t \in [0, 1] ⟼ t x + (1 - t) y)$
58		ovex	$⊢ 0 \cdot x + 1 y \in V$
59	56 57 58	fvmpt	$⊢ 0 \in [0, 1] \to (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = 0 \cdot x + 1 y$
60	50 59	ax-mp	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = 0 \cdot x + 1 y$
61	22	mul02d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x = 0$
62	33	mulid2d	$⊢ (φ \land (y \in S \land x \in S)) \to 1 y = y$
63	61 62	oveq12d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x + 1 y = 0 + y$
64	33	addid2d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 + y = y$
65	63 64	eqtrd	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot x + 1 y = y$
66	60 65	syl5eq	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) (0) = y$
67		1elunit	$⊢ 1 \in [0, 1]$
68		oveq1	$⊢ t = 1 \to t x = 1 x$
69		oveq2	$⊢ t = 1 \to 1 - t = 1 - 1$
70		1m1e0	$⊢ 1 - 1 = 0$
71	69 70	eqtrdi	$⊢ t = 1 \to 1 - t = 0$
72	71	oveq1d	$⊢ t = 1 \to (1 - t) y = 0 \cdot y$
73	68 72	oveq12d	$⊢ t = 1 \to t x + (1 - t) y = 1 x + 0 \cdot y$
74		ovex	$⊢ 1 x + 0 \cdot y \in V$
75	73 57 74	fvmpt	$⊢ 1 \in [0, 1] \to (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = 1 x + 0 \cdot y$
76	67 75	ax-mp	$⊢ (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = 1 x + 0 \cdot y$
77	22	mulid2d	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x = x$
78	33	mul02d	$⊢ (φ \land (y \in S \land x \in S)) \to 0 \cdot y = 0$
79	77 78	oveq12d	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x + 0 \cdot y = x + 0$
80	22	addid1d	$⊢ (φ \land (y \in S \land x \in S)) \to x + 0 = x$
81	79 80	eqtrd	$⊢ (φ \land (y \in S \land x \in S)) \to 1 x + 0 \cdot y = x$
82	76 81	syl5eq	$⊢ (φ \land (y \in S \land x \in S)) \to (t \in [0, 1] ⟼ t x + (1 - t) y) (1) = x$
83		fveq1	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to f (0) = (t \in [0, 1] ⟼ t x + (1 - t) y) (0)$
84	83	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)$
85		fveq1	$⊢ f = (t \in [0, 1] ⟼ t x + (1 - t) y) \to f (1) = (t \in [0, 1] ⟼ t x + (1 - t) y) (1)$
86	85	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)$
87	84 86	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))$
88	87	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)$
89	49 66 82 88	syl12anc	$⊢ (φ \land (y \in S \land x \in S)) \to \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
90	89	ralrimivva	$⊢ φ \to \forall y \in S \forall x \in S \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
91		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
92	13 1 91	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
93	4 92	eqeltrid	$⊢ φ \to K \in TopOn (S)$
94		toponuni	$⊢ K \in TopOn (S) \to S = ⋃ K$
95	93 94	syl	$⊢ φ \to S = ⋃ K$
96	95	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))$
97	95 96	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))$
98	90 97	mpbid	$⊢ φ \to \forall y \in ⋃ K \forall x \in ⋃ K \exists f \in (II Cn K) (f (0) = y \land f (1) = x)$
99		eqid	$⊢ ⋃ K = ⋃ K$
100	99	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))$
101	11 98 100	sylanbrc	$⊢ φ \to K \in PConn$

Metamath Proof Explorer

Theorem cvxpconn

Proof