Metamath Proof Explorer

Theorem cvxsconn

Description: A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015)

Ref Expression
Hypotheses cvxpconn.1 
|- ( ph -> S C_ CC )
cvxpconn.2 
|- ( ( ph /\ ( x e. S /\ y e. S /\ t e. ( 0 [,] 1 ) ) ) -> ( ( t x. x ) + ( ( 1 - t ) x. y ) ) e. S )
cvxpconn.3 
|- J = ( TopOpen ` CCfld )
cvxpconn.4 
|- K = ( J |`t S )
Assertion cvxsconn 
|- ( ph -> K e. SConn )

Proof

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