Metamath Proof Explorer

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