Theorem resconn

Description: A subset of RR is simply connected iff it is connected. (Contributed by Mario Carneiro, 9-Mar-2015)

	Ref	Expression
Hypothesis	resconn.1	⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
Assertion	resconn	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ∈ SConn ↔ 𝐽 ∈ Conn ) )

Proof

Step	Hyp	Ref	Expression
1		resconn.1	⊢ 𝐽 = ( ( topGen ‘ ran (,) ) ↾t 𝐴 )
2		sconnpconn	⊢ ( 𝐽 ∈ SConn → 𝐽 ∈ PConn )
3		pconnconn	⊢ ( 𝐽 ∈ PConn → 𝐽 ∈ Conn )
4	2 3	syl	⊢ ( 𝐽 ∈ SConn → 𝐽 ∈ Conn )
5		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
6		eqid	⊢ ( topGen ‘ ran (,) ) = ( topGen ‘ ran (,) )
7	5 6	rerest	⊢ ( 𝐴 ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) )
8	7 1	eqtr4di	⊢ ( 𝐴 ⊆ ℝ → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = 𝐽 )
9	8	adantr	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = 𝐽 )
10		simpl	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → 𝐴 ⊆ ℝ )
11		ax-resscn	⊢ ℝ ⊆ ℂ
12	10 11	sstrdi	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → 𝐴 ⊆ ℂ )
13		df-3an	⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ↔ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) )
14		oveq2	⊢ ( 𝑧 = 𝑥 → ( 𝑡 · 𝑧 ) = ( 𝑡 · 𝑥 ) )
15		oveq2	⊢ ( 𝑤 = 𝑦 → ( ( 1 − 𝑡 ) · 𝑤 ) = ( ( 1 − 𝑡 ) · 𝑦 ) )
16	14 15	oveqan12d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
17	16	eleq1d	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) ∈ 𝐴 ↔ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 ) )
18	17	ralbidv	⊢ ( ( 𝑧 = 𝑥 ∧ 𝑤 = 𝑦 ) → ( ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) ∈ 𝐴 ↔ ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 ) )
19		oveq2	⊢ ( 𝑧 = 𝑦 → ( 𝑡 · 𝑧 ) = ( 𝑡 · 𝑦 ) )
20		oveq2	⊢ ( 𝑤 = 𝑥 → ( ( 1 − 𝑡 ) · 𝑤 ) = ( ( 1 − 𝑡 ) · 𝑥 ) )
21	19 20	oveqan12d	⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) = ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) )
22	21	eleq1d	⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) ∈ 𝐴 ↔ ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ∈ 𝐴 ) )
23	22	ralbidv	⊢ ( ( 𝑧 = 𝑦 ∧ 𝑤 = 𝑥 ) → ( ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑧 ) + ( ( 1 − 𝑡 ) · 𝑤 ) ) ∈ 𝐴 ↔ ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ∈ 𝐴 ) )
24		unitssre	⊢ ( 0 [,] 1 ) ⊆ ℝ
25	24 11	sstri	⊢ ( 0 [,] 1 ) ⊆ ℂ
26		simpr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
27	25 26	sselid	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ℂ )
28	12	adantr	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → 𝐴 ⊆ ℂ )
29		simpr2	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → 𝑦 ∈ 𝐴 )
30	28 29	sseldd	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → 𝑦 ∈ ℂ )
31	30	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑦 ∈ ℂ )
32	27 31	mulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 · 𝑦 ) ∈ ℂ )
33		ax-1cn	⊢ 1 ∈ ℂ
34		subcl	⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑠 ) ∈ ℂ )
35	33 27 34	sylancr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑠 ) ∈ ℂ )
36		simpr1	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → 𝑥 ∈ 𝐴 )
37	28 36	sseldd	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → 𝑥 ∈ ℂ )
38	37	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℂ )
39	35 38	mulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑠 ) · 𝑥 ) ∈ ℂ )
40	32 39	addcomd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) = ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( 𝑠 · 𝑦 ) ) )
41		nncan	⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − ( 1 − 𝑠 ) ) = 𝑠 )
42	33 27 41	sylancr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 − ( 1 − 𝑠 ) ) = 𝑠 )
43	42	oveq1d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) = ( 𝑠 · 𝑦 ) )
44	43	oveq2d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) = ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( 𝑠 · 𝑦 ) ) )
45	40 44	eqtr4d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) = ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) )
46		iirev	⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( 1 − 𝑠 ) ∈ ( 0 [,] 1 ) )
47	46	adantl	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑠 ) ∈ ( 0 [,] 1 ) )
48	1	eleq1i	⊢ ( 𝐽 ∈ Conn ↔ ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn )
49		reconn	⊢ ( 𝐴 ⊆ ℝ → ( ( ( topGen ‘ ran (,) ) ↾t 𝐴 ) ∈ Conn ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )
50	48 49	bitrid	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ∈ Conn ↔ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 ) )
51	50	biimpa	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
52	51	r19.21bi	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ 𝑥 ∈ 𝐴 ) → ∀ 𝑦 ∈ 𝐴 ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
53	52	r19.21bi	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ 𝑥 ∈ 𝐴 ) ∧ 𝑦 ∈ 𝐴 ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
54	53	anasss	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
55	54	3adantr3	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
56	55	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑥 [,] 𝑦 ) ⊆ 𝐴 )
57		simpr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ( 0 [,] 1 ) )
58	24 57	sselid	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ℝ )
59		simplll	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝐴 ⊆ ℝ )
60	36	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ 𝐴 )
61	59 60	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℝ )
62	58 61	remulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 · 𝑥 ) ∈ ℝ )
63		1re	⊢ 1 ∈ ℝ
64		resubcl	⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 1 − 𝑡 ) ∈ ℝ )
65	63 58 64	sylancr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑡 ) ∈ ℝ )
66	29	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑦 ∈ 𝐴 )
67	59 66	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑦 ∈ ℝ )
68	65 67	remulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑡 ) · 𝑦 ) ∈ ℝ )
69	62 68	readdcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ )
70	58	recnd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ∈ ℂ )
71		pncan3	⊢ ( ( 𝑡 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑡 + ( 1 − 𝑡 ) ) = 1 )
72	70 33 71	sylancl	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 + ( 1 − 𝑡 ) ) = 1 )
73	72	oveq1d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 + ( 1 − 𝑡 ) ) · 𝑥 ) = ( 1 · 𝑥 ) )
74	65	recnd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑡 ) ∈ ℂ )
75	37	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑥 ∈ ℂ )
76	70 74 75	adddird	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 + ( 1 − 𝑡 ) ) · 𝑥 ) = ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) )
77	75	mullidd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 · 𝑥 ) = 𝑥 )
78	73 76 77	3eqtr3d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) = 𝑥 )
79	65 61	remulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑡 ) · 𝑥 ) ∈ ℝ )
80		elicc01	⊢ ( 𝑡 ∈ ( 0 [,] 1 ) ↔ ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
81	57 80	sylib	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 ∈ ℝ ∧ 0 ≤ 𝑡 ∧ 𝑡 ≤ 1 ) )
82	81	simp3d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑡 ≤ 1 )
83		subge0	⊢ ( ( 1 ∈ ℝ ∧ 𝑡 ∈ ℝ ) → ( 0 ≤ ( 1 − 𝑡 ) ↔ 𝑡 ≤ 1 ) )
84	63 58 83	sylancr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 0 ≤ ( 1 − 𝑡 ) ↔ 𝑡 ≤ 1 ) )
85	82 84	mpbird	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 ≤ ( 1 − 𝑡 ) )
86		simplr3	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑥 ≤ 𝑦 )
87	61 67 65 85 86	lemul2ad	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑡 ) · 𝑥 ) ≤ ( ( 1 − 𝑡 ) · 𝑦 ) )
88	79 68 62 87	leadd2dd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ≤ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
89	78 88	eqbrtrrd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑥 ≤ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
90	58 67	remulcld	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 · 𝑦 ) ∈ ℝ )
91	81	simp2d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 0 ≤ 𝑡 )
92	61 67 58 91 86	lemul2ad	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 𝑡 · 𝑥 ) ≤ ( 𝑡 · 𝑦 ) )
93	62 90 68 92	leadd1dd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ≤ ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
94	72	oveq1d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 + ( 1 − 𝑡 ) ) · 𝑦 ) = ( 1 · 𝑦 ) )
95	30	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → 𝑦 ∈ ℂ )
96	70 74 95	adddird	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 + ( 1 − 𝑡 ) ) · 𝑦 ) = ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
97	95	mullidd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( 1 · 𝑦 ) = 𝑦 )
98	94 96 97	3eqtr3d	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = 𝑦 )
99	93 98	breqtrd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ≤ 𝑦 )
100		elicc2	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ ∧ 𝑥 ≤ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∧ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ≤ 𝑦 ) ) )
101	61 67 100	syl2anc	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ( 𝑥 [,] 𝑦 ) ↔ ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ℝ ∧ 𝑥 ≤ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∧ ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ≤ 𝑦 ) ) )
102	69 89 99 101	mpbir3and	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ ( 𝑥 [,] 𝑦 ) )
103	56 102	sseldd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
104	103	ralrimiva	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
105	104	adantr	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
106		oveq1	⊢ ( 𝑡 = ( 1 − 𝑠 ) → ( 𝑡 · 𝑥 ) = ( ( 1 − 𝑠 ) · 𝑥 ) )
107		oveq2	⊢ ( 𝑡 = ( 1 − 𝑠 ) → ( 1 − 𝑡 ) = ( 1 − ( 1 − 𝑠 ) ) )
108	107	oveq1d	⊢ ( 𝑡 = ( 1 − 𝑠 ) → ( ( 1 − 𝑡 ) · 𝑦 ) = ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) )
109	106 108	oveq12d	⊢ ( 𝑡 = ( 1 − 𝑠 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) )
110	109	eleq1d	⊢ ( 𝑡 = ( 1 − 𝑠 ) → ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 ↔ ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) ∈ 𝐴 ) )
111	110	rspcv	⊢ ( ( 1 − 𝑠 ) ∈ ( 0 [,] 1 ) → ( ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 → ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) ∈ 𝐴 ) )
112	47 105 111	sylc	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 1 − 𝑠 ) · 𝑥 ) + ( ( 1 − ( 1 − 𝑠 ) ) · 𝑦 ) ) ∈ 𝐴 )
113	45 112	eqeltrd	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) ∈ 𝐴 )
114	113	ralrimiva	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) ∈ 𝐴 )
115		oveq1	⊢ ( 𝑠 = 𝑡 → ( 𝑠 · 𝑦 ) = ( 𝑡 · 𝑦 ) )
116		oveq2	⊢ ( 𝑠 = 𝑡 → ( 1 − 𝑠 ) = ( 1 − 𝑡 ) )
117	116	oveq1d	⊢ ( 𝑠 = 𝑡 → ( ( 1 − 𝑠 ) · 𝑥 ) = ( ( 1 − 𝑡 ) · 𝑥 ) )
118	115 117	oveq12d	⊢ ( 𝑠 = 𝑡 → ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) = ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) )
119	118	eleq1d	⊢ ( 𝑠 = 𝑡 → ( ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) ∈ 𝐴 ↔ ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ∈ 𝐴 ) )
120	119	cbvralvw	⊢ ( ∀ 𝑠 ∈ ( 0 [,] 1 ) ( ( 𝑠 · 𝑦 ) + ( ( 1 − 𝑠 ) · 𝑥 ) ) ∈ 𝐴 ↔ ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ∈ 𝐴 )
121	114 120	sylib	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ≤ 𝑦 ) ) → ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑦 ) + ( ( 1 − 𝑡 ) · 𝑥 ) ) ∈ 𝐴 )
122	18 23 10 121 104	wloglei	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
123	122	r19.21bi	⊢ ( ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
124	123	anasss	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
125	13 124	sylan2b	⊢ ( ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝐴 )
126		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 )
127	12 125 5 126	cvxsconn	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → ( ( TopOpen ‘ ℂfld ) ↾t 𝐴 ) ∈ SConn )
128	9 127	eqeltrrd	⊢ ( ( 𝐴 ⊆ ℝ ∧ 𝐽 ∈ Conn ) → 𝐽 ∈ SConn )
129	128	ex	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ∈ Conn → 𝐽 ∈ SConn ) )
130	4 129	impbid2	⊢ ( 𝐴 ⊆ ℝ → ( 𝐽 ∈ SConn ↔ 𝐽 ∈ Conn ) )