Metamath Proof Explorer

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 ) )