cvxsconn

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

Metamath Proof Explorer

Theorem cvxsconn

Proof