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 
|- J = ( ( topGen ` ran (,) ) |`t A )
Assertion resconn 
|- ( A C_ RR -> ( J e. SConn <-> J e. Conn ) )

Proof

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