cvxsconn

Description: A convex subset of the complex numbers is simply 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	cvxsconn	$⊢ φ \to K \in SConn$

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	1 2 3 4	cvxpconn	$⊢ φ \to K \in PConn$
6		simprl	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f \in (II Cn K)$
7		pconntop	$⊢ K \in PConn \to K \in Top$
8	5 7	syl	$⊢ φ \to K \in Top$
9	8	adantr	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to K \in Top$
10		eqid	$⊢ ⋃ K = ⋃ K$
11	10	toptopon	$⊢ K \in Top \leftrightarrow K \in TopOn (⋃ K)$
12	9 11	sylib	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to K \in TopOn (⋃ K)$
13		iiuni	$⊢ [0, 1] = ⋃ II$
14	13 10	cnf	$⊢ f \in (II Cn K) \to f : [0, 1] ⟶ ⋃ K$
15	6 14	syl	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f : [0, 1] ⟶ ⋃ K$
16		0elunit	$⊢ 0 \in [0, 1]$
17		ffvelcdm	$⊢ (f : [0, 1] ⟶ ⋃ K \land 0 \in [0, 1]) \to f (0) \in ⋃ K$
18	15 16 17	sylancl	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f (0) \in ⋃ K$
19		eqid	$⊢ [0, 1] \times \{f (0)\} = [0, 1] \times \{f (0)\}$
20	19	pcoptcl	$⊢ (K \in TopOn (⋃ K) \land f (0) \in ⋃ K) \to ([0, 1] \times \{f (0)\} \in (II Cn K) \land ([0, 1] \times \{f (0)\}) (0) = f (0) \land ([0, 1] \times \{f (0)\}) (1) = f (0))$
21	12 18 20	syl2anc	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to ([0, 1] \times \{f (0)\} \in (II Cn K) \land ([0, 1] \times \{f (0)\}) (0) = f (0) \land ([0, 1] \times \{f (0)\}) (1) = f (0))$
22	21	simp1d	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to [0, 1] \times \{f (0)\} \in (II Cn K)$
23		iitopon	$⊢ II \in TopOn ([0, 1])$
24	23	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to II \in TopOn ([0, 1])$
25	3	dfii3	$⊢ II = J ↾_{𝑡} [0, 1]$
26	3	cnfldtopon	$⊢ J \in TopOn (ℂ)$
27	26	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to J \in TopOn (ℂ)$
28		unitssre	$⊢ [0, 1] \subseteq ℝ$
29		ax-resscn	$⊢ ℝ \subseteq ℂ$
30	28 29	sstri	$⊢ [0, 1] \subseteq ℂ$
31	30	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to [0, 1] \subseteq ℂ$
32	27 27	cnmpt2nd	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in ℂ, t \in ℂ ⟼ t) \in ((J \times_{t} J) Cn J)$
33	25 27 31 25 27 31 32	cnmpt2res	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t) \in ((II \times_{t} II) Cn J)$
34	1	adantr	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to S \subseteq ℂ$
35		resttopon	$⊢ (J \in TopOn (ℂ) \land S \subseteq ℂ) \to J ↾_{𝑡} S \in TopOn (S)$
36	26 1 35	sylancr	$⊢ φ \to J ↾_{𝑡} S \in TopOn (S)$
37	4 36	eqeltrid	$⊢ φ \to K \in TopOn (S)$
38		toponuni	$⊢ K \in TopOn (S) \to S = ⋃ K$
39	37 38	syl	$⊢ φ \to S = ⋃ K$
40	39	adantr	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to S = ⋃ K$
41	18 40	eleqtrrd	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f (0) \in S$
42	34 41	sseldd	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f (0) \in ℂ$
43	24 24 27 42	cnmpt2c	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ f (0)) \in ((II \times_{t} II) Cn J)$
44	3	mulcn	$⊢ \times \in ((J \times_{t} J) Cn J)$
45	44	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to \times \in ((J \times_{t} J) Cn J)$
46	24 24 33 43 45	cnmpt22f	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0)) \in ((II \times_{t} II) Cn J)$
47		ax-1cn	$⊢ 1 \in ℂ$
48	47	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to 1 \in ℂ$
49	27 27 27 48	cnmpt2c	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in ℂ, t \in ℂ ⟼ 1) \in ((J \times_{t} J) Cn J)$
50	3	subcn	$⊢ - \in ((J \times_{t} J) Cn J)$
51	50	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to - \in ((J \times_{t} J) Cn J)$
52	27 27 49 32 51	cnmpt22f	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in ℂ, t \in ℂ ⟼ 1 - t) \in ((J \times_{t} J) Cn J)$
53	25 27 31 25 27 31 52	cnmpt2res	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ 1 - t) \in ((II \times_{t} II) Cn J)$
54	24 24	cnmpt1st	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ z) \in ((II \times_{t} II) Cn II)$
55	3	cnfldtop	$⊢ J \in Top$
56		cnrest2r	$⊢ J \in Top \to II Cn (J ↾_{𝑡} S) \subseteq II Cn J$
57	55 56	ax-mp	$⊢ II Cn (J ↾_{𝑡} S) \subseteq II Cn J$
58	4	oveq2i	$⊢ II Cn K = II Cn (J ↾_{𝑡} S)$
59	6 58	eleqtrdi	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f \in (II Cn (J ↾_{𝑡} S))$
60	57 59	sselid	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f \in (II Cn J)$
61	24 24 54 60	cnmpt21f	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ f (z)) \in ((II \times_{t} II) Cn J)$
62	24 24 53 61 45	cnmpt22f	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ (1 - t) f (z)) \in ((II \times_{t} II) Cn J)$
63	3	addcn	$⊢ + \in ((J \times_{t} J) Cn J)$
64	63	a1i	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to + \in ((J \times_{t} J) Cn J)$
65	24 24 46 62 64	cnmpt22f	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn J)$
66	41	adantr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to f (0) \in S$
67	15	adantr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to f : [0, 1] ⟶ ⋃ K$
68		simprl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to z \in [0, 1]$
69	67 68	ffvelcdmd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to f (z) \in ⋃ K$
70	40	adantr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to S = ⋃ K$
71	69 70	eleqtrrd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to f (z) \in S$
72	2	3exp2	$⊢ φ \to (x \in S \to (y \in S \to (t \in [0, 1] \to t x + (1 - t) y \in S)))$
73	72	imp42	$⊢ ((φ \land (x \in S \land y \in S)) \land t \in [0, 1]) \to t x + (1 - t) y \in S$
74	73	an32s	$⊢ ((φ \land t \in [0, 1]) \land (x \in S \land y \in S)) \to t x + (1 - t) y \in S$
75	74	ralrimivva	$⊢ (φ \land t \in [0, 1]) \to \forall x \in S \forall y \in S t x + (1 - t) y \in S$
76	75	ad2ant2rl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to \forall x \in S \forall y \in S t x + (1 - t) y \in S$
77		oveq2	$⊢ x = f (0) \to t x = t f (0)$
78	77	oveq1d	$⊢ x = f (0) \to t x + (1 - t) y = t f (0) + (1 - t) y$
79	78	eleq1d	$⊢ x = f (0) \to (t x + (1 - t) y \in S \leftrightarrow t f (0) + (1 - t) y \in S)$
80		oveq2	$⊢ y = f (z) \to (1 - t) y = (1 - t) f (z)$
81	80	oveq2d	$⊢ y = f (z) \to t f (0) + (1 - t) y = t f (0) + (1 - t) f (z)$
82	81	eleq1d	$⊢ y = f (z) \to (t f (0) + (1 - t) y \in S \leftrightarrow t f (0) + (1 - t) f (z) \in S)$
83	79 82	rspc2va	$⊢ ((f (0) \in S \land f (z) \in S) \land \forall x \in S \forall y \in S t x + (1 - t) y \in S) \to t f (0) + (1 - t) f (z) \in S$
84	66 71 76 83	syl21anc	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land (z \in [0, 1] \land t \in [0, 1])) \to t f (0) + (1 - t) f (z) \in S$
85	84	ralrimivva	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to \forall z \in [0, 1] \forall t \in [0, 1] t f (0) + (1 - t) f (z) \in S$
86		eqid	$⊢ (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) = (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z))$
87	86	fmpo	$⊢ \forall z \in [0, 1] \forall t \in [0, 1] t f (0) + (1 - t) f (z) \in S \leftrightarrow (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) : [0, 1] \times [0, 1] ⟶ S$
88	85 87	sylib	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) : [0, 1] \times [0, 1] ⟶ S$
89	88	frnd	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to ran (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \subseteq S$
90		cnrest2	$⊢ (J \in TopOn (ℂ) \land ran (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \subseteq S \land S \subseteq ℂ) \to ((z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn J) \leftrightarrow (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn (J ↾_{𝑡} S)))$
91	27 89 34 90	syl3anc	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to ((z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn J) \leftrightarrow (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn (J ↾_{𝑡} S)))$
92	65 91	mpbid	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn (J ↾_{𝑡} S))$
93	4	oveq2i	$⊢ (II \times_{t} II) Cn K = (II \times_{t} II) Cn (J ↾_{𝑡} S)$
94	92 93	eleqtrrdi	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in ((II \times_{t} II) Cn K)$
95		simpr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s \in [0, 1]$
96		simpr	$⊢ (z = s \land t = 0) \to t = 0$
97	96	oveq1d	$⊢ (z = s \land t = 0) \to t f (0) = 0 \cdot f (0)$
98	96	oveq2d	$⊢ (z = s \land t = 0) \to 1 - t = 1 - 0$
99		1m0e1	$⊢ 1 - 0 = 1$
100	98 99	eqtrdi	$⊢ (z = s \land t = 0) \to 1 - t = 1$
101		simpl	$⊢ (z = s \land t = 0) \to z = s$
102	101	fveq2d	$⊢ (z = s \land t = 0) \to f (z) = f (s)$
103	100 102	oveq12d	$⊢ (z = s \land t = 0) \to (1 - t) f (z) = 1 f (s)$
104	97 103	oveq12d	$⊢ (z = s \land t = 0) \to t f (0) + (1 - t) f (z) = 0 \cdot f (0) + 1 f (s)$
105		ovex	$⊢ 0 \cdot f (0) + 1 f (s) \in V$
106	104 86 105	ovmpoa	$⊢ (s \in [0, 1] \land 0 \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 0 = 0 \cdot f (0) + 1 f (s)$
107	95 16 106	sylancl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 0 = 0 \cdot f (0) + 1 f (s)$
108	42	adantr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to f (0) \in ℂ$
109	108	mul02d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 \cdot f (0) = 0$
110	26	toponunii	$⊢ ℂ = ⋃ J$
111	13 110	cnf	$⊢ f \in (II Cn J) \to f : [0, 1] ⟶ ℂ$
112	60 111	syl	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f : [0, 1] ⟶ ℂ$
113	112	ffvelcdmda	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to f (s) \in ℂ$
114	113	mullidd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 f (s) = f (s)$
115	109 114	oveq12d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 \cdot f (0) + 1 f (s) = 0 + f (s)$
116	113	addlidd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 + f (s) = f (s)$
117	107 115 116	3eqtrd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 0 = f (s)$
118		1elunit	$⊢ 1 \in [0, 1]$
119		simpr	$⊢ (z = s \land t = 1) \to t = 1$
120	119	oveq1d	$⊢ (z = s \land t = 1) \to t f (0) = 1 f (0)$
121	119	oveq2d	$⊢ (z = s \land t = 1) \to 1 - t = 1 - 1$
122		1m1e0	$⊢ 1 - 1 = 0$
123	121 122	eqtrdi	$⊢ (z = s \land t = 1) \to 1 - t = 0$
124		simpl	$⊢ (z = s \land t = 1) \to z = s$
125	124	fveq2d	$⊢ (z = s \land t = 1) \to f (z) = f (s)$
126	123 125	oveq12d	$⊢ (z = s \land t = 1) \to (1 - t) f (z) = 0 \cdot f (s)$
127	120 126	oveq12d	$⊢ (z = s \land t = 1) \to t f (0) + (1 - t) f (z) = 1 f (0) + 0 \cdot f (s)$
128		ovex	$⊢ 1 f (0) + 0 \cdot f (s) \in V$
129	127 86 128	ovmpoa	$⊢ (s \in [0, 1] \land 1 \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 1 = 1 f (0) + 0 \cdot f (s)$
130	95 118 129	sylancl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 1 = 1 f (0) + 0 \cdot f (s)$
131	108	mullidd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 f (0) = f (0)$
132	113	mul02d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 \cdot f (s) = 0$
133	131 132	oveq12d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 f (0) + 0 \cdot f (s) = f (0) + 0$
134	108	addridd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to f (0) + 0 = f (0)$
135		fvex	$⊢ f (0) \in V$
136	135	fvconst2	$⊢ s \in [0, 1] \to ([0, 1] \times \{f (0)\}) (s) = f (0)$
137	136	adantl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to ([0, 1] \times \{f (0)\}) (s) = f (0)$
138	134 137	eqtr4d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to f (0) + 0 = ([0, 1] \times \{f (0)\}) (s)$
139	130 133 138	3eqtrd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) 1 = ([0, 1] \times \{f (0)\}) (s)$
140		simpr	$⊢ (z = 0 \land t = s) \to t = s$
141	140	oveq1d	$⊢ (z = 0 \land t = s) \to t f (0) = s f (0)$
142	140	oveq2d	$⊢ (z = 0 \land t = s) \to 1 - t = 1 - s$
143		simpl	$⊢ (z = 0 \land t = s) \to z = 0$
144	143	fveq2d	$⊢ (z = 0 \land t = s) \to f (z) = f (0)$
145	142 144	oveq12d	$⊢ (z = 0 \land t = s) \to (1 - t) f (z) = (1 - s) f (0)$
146	141 145	oveq12d	$⊢ (z = 0 \land t = s) \to t f (0) + (1 - t) f (z) = s f (0) + (1 - s) f (0)$
147		ovex	$⊢ s f (0) + (1 - s) f (0) \in V$
148	146 86 147	ovmpoa	$⊢ (0 \in [0, 1] \land s \in [0, 1]) \to 0 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = s f (0) + (1 - s) f (0)$
149	16 95 148	sylancr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = s f (0) + (1 - s) f (0)$
150	30 95	sselid	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s \in ℂ$
151		pncan3	$⊢ (s \in ℂ \land 1 \in ℂ) \to s + 1 - s = 1$
152	150 47 151	sylancl	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s + 1 - s = 1$
153	152	oveq1d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to (s + 1 - s) f (0) = 1 f (0)$
154		subcl	$⊢ (1 \in ℂ \land s \in ℂ) \to 1 - s \in ℂ$
155	47 150 154	sylancr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 - s \in ℂ$
156	150 155 108	adddird	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to (s + 1 - s) f (0) = s f (0) + (1 - s) f (0)$
157	153 156 131	3eqtr3d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s f (0) + (1 - s) f (0) = f (0)$
158	149 157	eqtrd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 0 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = f (0)$
159		simpr	$⊢ (z = 1 \land t = s) \to t = s$
160	159	oveq1d	$⊢ (z = 1 \land t = s) \to t f (0) = s f (0)$
161	159	oveq2d	$⊢ (z = 1 \land t = s) \to 1 - t = 1 - s$
162		simpl	$⊢ (z = 1 \land t = s) \to z = 1$
163	162	fveq2d	$⊢ (z = 1 \land t = s) \to f (z) = f (1)$
164	161 163	oveq12d	$⊢ (z = 1 \land t = s) \to (1 - t) f (z) = (1 - s) f (1)$
165	160 164	oveq12d	$⊢ (z = 1 \land t = s) \to t f (0) + (1 - t) f (z) = s f (0) + (1 - s) f (1)$
166		ovex	$⊢ s f (0) + (1 - s) f (1) \in V$
167	165 86 166	ovmpoa	$⊢ (1 \in [0, 1] \land s \in [0, 1]) \to 1 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = s f (0) + (1 - s) f (1)$
168	118 95 167	sylancr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = s f (0) + (1 - s) f (1)$
169		simplrr	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to f (0) = f (1)$
170	169	oveq2d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to (1 - s) f (0) = (1 - s) f (1)$
171	170	oveq2d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s f (0) + (1 - s) f (0) = s f (0) + (1 - s) f (1)$
172	157 171 169	3eqtr3d	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to s f (0) + (1 - s) f (1) = f (1)$
173	168 172	eqtrd	$⊢ ((φ \land (f \in (II Cn K) \land f (0) = f (1))) \land s \in [0, 1]) \to 1 (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) s = f (1)$
174	6 22 94 117 139 158 173	isphtpy2d	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to (z \in [0, 1], t \in [0, 1] ⟼ t f (0) + (1 - t) f (z)) \in (f PHtpy (K) ([0, 1] \times \{f (0)\}))$
175	174	ne0d	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f PHtpy (K) ([0, 1] \times \{f (0)\}) \neq \emptyset$
176		isphtpc	$⊢ f ≃_{ph} (K) ([0, 1] \times \{f (0)\}) \leftrightarrow (f \in (II Cn K) \land [0, 1] \times \{f (0)\} \in (II Cn K) \land f PHtpy (K) ([0, 1] \times \{f (0)\}) \neq \emptyset)$
177	6 22 175 176	syl3anbrc	$⊢ (φ \land (f \in (II Cn K) \land f (0) = f (1))) \to f ≃_{ph} (K) ([0, 1] \times \{f (0)\})$
178	177	expr	$⊢ (φ \land f \in (II Cn K)) \to (f (0) = f (1) \to f ≃_{ph} (K) ([0, 1] \times \{f (0)\}))$
179	178	ralrimiva	$⊢ φ \to \forall f \in (II Cn K) (f (0) = f (1) \to f ≃_{ph} (K) ([0, 1] \times \{f (0)\}))$
180		issconn	$⊢ K \in SConn \leftrightarrow (K \in PConn \land \forall f \in (II Cn K) (f (0) = f (1) \to f ≃_{ph} (K) ([0, 1] \times \{f (0)\})))$
181	5 179 180	sylanbrc	$⊢ φ \to K \in SConn$

Metamath Proof Explorer

Theorem cvxsconn

Proof