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 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
cvxpconn.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
cvxpconn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
cvxpconn.4 ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
Assertion cvxsconn ( 𝜑 → 𝐾 ∈ SConn )

Proof

Step Hyp Ref Expression
1 cvxpconn.1 ⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2 cvxpconn.2 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
3 cvxpconn.3 ⊢ 𝐽 = ( TopOpen ‘ ℂfld )
4 cvxpconn.4 ⊢ 𝐾 = ( 𝐽 ↾t 𝑆 )
5 1 2 3 4 cvxpconn ⊢ ( 𝜑 → 𝐾 ∈ PConn )
6 simprl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ∈ ( II Cn 𝐾 ) )
7 pconntop ⊢ ( 𝐾 ∈ PConn → 𝐾 ∈ Top )
8 5 7 syl ⊢ ( 𝜑 → 𝐾 ∈ Top )
9 8 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐾 ∈ Top )
10 toptopon2 ⊢ ( 𝐾 ∈ Top ↔ 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
11 9 10 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) )
12 iiuni ⊢ ( 0 [,] 1 ) = ∪ II
13 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
14 12 13 cnf ⊢ ( 𝑓 ∈ ( II Cn 𝐾 ) → 𝑓 : ( 0 [,] 1 ) ⟶ ∪ 𝐾 )
15 6 14 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ ∪ 𝐾 )
16 0elunit ⊢ 0 ∈ ( 0 [,] 1 )
17 ffvelcdm ⊢ ( ( 𝑓 : ( 0 [,] 1 ) ⟶ ∪ 𝐾 ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 0 ) ∈ ∪ 𝐾 )
18 15 16 17 sylancl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) ∈ ∪ 𝐾 )
19 eqid ⊢ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) = ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } )
20 19 pcoptcl ⊢ ( ( 𝐾 ∈ ( TopOn ‘ ∪ 𝐾 ) ∧ ( 𝑓 ‘ 0 ) ∈ ∪ 𝐾 ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 0 ) = ( 𝑓 ‘ 0 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 1 ) = ( 𝑓 ‘ 0 ) ) )
21 11 18 20 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐾 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 0 ) = ( 𝑓 ‘ 0 ) ∧ ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 1 ) = ( 𝑓 ‘ 0 ) ) )
22 21 simp1d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐾 ) )
23 iitopon ⊢ II ∈ ( TopOn ‘ ( 0 [,] 1 ) )
24 23 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → II ∈ ( TopOn ‘ ( 0 [,] 1 ) ) )
25 3 dfii3 ⊢ II = ( 𝐽 ↾t ( 0 [,] 1 ) )
26 3 cnfldtopon ⊢ 𝐽 ∈ ( TopOn ‘ ℂ )
27 26 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝐽 ∈ ( TopOn ‘ ℂ ) )
28 unitsscn ⊢ ( 0 [,] 1 ) ⊆ ℂ
29 28 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 0 [,] 1 ) ⊆ ℂ )
30 27 27 cnmpt2nd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ℂ , 𝑡 ∈ ℂ ↦ 𝑡 ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
31 25 27 29 25 27 29 30 cnmpt2res ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ 𝑡 ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
32 1 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑆 ⊆ ℂ )
33 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ 𝑆 ⊆ ℂ ) → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
34 26 1 33 sylancr ⊢ ( 𝜑 → ( 𝐽 ↾t 𝑆 ) ∈ ( TopOn ‘ 𝑆 ) )
35 4 34 eqeltrid ⊢ ( 𝜑 → 𝐾 ∈ ( TopOn ‘ 𝑆 ) )
36 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑆 ) → 𝑆 = ∪ 𝐾 )
37 35 36 syl ⊢ ( 𝜑 → 𝑆 = ∪ 𝐾 )
38 37 adantr ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑆 = ∪ 𝐾 )
39 18 38 eleqtrrd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) ∈ 𝑆 )
40 32 39 sseldd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ‘ 0 ) ∈ ℂ )
41 24 24 27 40 cnmpt2c ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ 0 ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
42 3 mpomulcn ⊢ ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
43 42 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑢 ∈ ℂ , 𝑣 ∈ ℂ ↦ ( 𝑢 · 𝑣 ) ) ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
44 oveq12 ⊢ ( ( 𝑢 = 𝑡 ∧ 𝑣 = ( 𝑓 ‘ 0 ) ) → ( 𝑢 · 𝑣 ) = ( 𝑡 · ( 𝑓 ‘ 0 ) ) )
45 24 24 31 41 27 27 43 44 cnmpt22 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝑡 · ( 𝑓 ‘ 0 ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
46 ax-1cn ⊢ 1 ∈ ℂ
47 46 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 1 ∈ ℂ )
48 24 24 27 47 cnmpt2c ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ 1 ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
49 3 subcn ⊢ − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
50 49 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → − ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
51 24 24 48 31 50 cnmpt22f ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 1 − 𝑡 ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
52 24 24 cnmpt1st ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ 𝑧 ) ∈ ( ( II ×t II ) Cn II ) )
53 3 cnfldtop ⊢ 𝐽 ∈ Top
54 cnrest2r ⊢ ( 𝐽 ∈ Top → ( II Cn ( 𝐽 ↾t 𝑆 ) ) ⊆ ( II Cn 𝐽 ) )
55 53 54 ax-mp ⊢ ( II Cn ( 𝐽 ↾t 𝑆 ) ) ⊆ ( II Cn 𝐽 )
56 4 oveq2i ⊢ ( II Cn 𝐾 ) = ( II Cn ( 𝐽 ↾t 𝑆 ) )
57 6 56 eleqtrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ∈ ( II Cn ( 𝐽 ↾t 𝑆 ) ) )
58 55 57 sselid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ∈ ( II Cn 𝐽 ) )
59 24 24 52 58 cnmpt21f ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( 𝑓 ‘ 𝑧 ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
60 oveq12 ⊢ ( ( 𝑢 = ( 1 − 𝑡 ) ∧ 𝑣 = ( 𝑓 ‘ 𝑧 ) ) → ( 𝑢 · 𝑣 ) = ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) )
61 24 24 51 59 27 27 43 60 cnmpt22 ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
62 3 addcn ⊢ + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 )
63 62 a1i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → + ∈ ( ( 𝐽 ×t 𝐽 ) Cn 𝐽 ) )
64 24 24 45 61 63 cnmpt22f ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) )
65 oveq2 ⊢ ( 𝑥 = ( 𝑓 ‘ 0 ) → ( 𝑡 · 𝑥 ) = ( 𝑡 · ( 𝑓 ‘ 0 ) ) )
66 65 oveq1d ⊢ ( 𝑥 = ( 𝑓 ‘ 0 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) )
67 66 eleq1d ⊢ ( 𝑥 = ( 𝑓 ‘ 0 ) → ( ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ↔ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) )
68 oveq2 ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( ( 1 − 𝑡 ) · 𝑦 ) = ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) )
69 68 oveq2d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) = ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) )
70 69 eleq1d ⊢ ( 𝑦 = ( 𝑓 ‘ 𝑧 ) → ( ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ↔ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ∈ 𝑆 ) )
71 2 3exp2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 → ( 𝑦 ∈ 𝑆 → ( 𝑡 ∈ ( 0 [,] 1 ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 ) ) ) )
72 71 imp42 ⊢ ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
73 72 an32s ⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
74 73 ralrimivva ⊢ ( ( 𝜑 ∧ 𝑡 ∈ ( 0 [,] 1 ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
75 74 ad2ant2rl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( ( 𝑡 · 𝑥 ) + ( ( 1 − 𝑡 ) · 𝑦 ) ) ∈ 𝑆 )
76 39 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ‘ 0 ) ∈ 𝑆 )
77 15 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ ∪ 𝐾 )
78 simprl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑧 ∈ ( 0 [,] 1 ) )
79 77 78 ffvelcdmd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ‘ 𝑧 ) ∈ ∪ 𝐾 )
80 38 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → 𝑆 = ∪ 𝐾 )
81 79 80 eleqtrrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( 𝑓 ‘ 𝑧 ) ∈ 𝑆 )
82 67 70 75 76 81 rspc2dv ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ ( 𝑧 ∈ ( 0 [,] 1 ) ∧ 𝑡 ∈ ( 0 [,] 1 ) ) ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ∈ 𝑆 )
83 82 ralrimivva ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ∀ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ∈ 𝑆 )
84 eqid ⊢ ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) = ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) )
85 84 fmpo ⊢ ( ∀ 𝑧 ∈ ( 0 [,] 1 ) ∀ 𝑡 ∈ ( 0 [,] 1 ) ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ∈ 𝑆 ↔ ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝑆 )
86 83 85 sylib ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) : ( ( 0 [,] 1 ) × ( 0 [,] 1 ) ) ⟶ 𝑆 )
87 86 frnd ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ran ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ⊆ 𝑆 )
88 cnrest2 ⊢ ( ( 𝐽 ∈ ( TopOn ‘ ℂ ) ∧ ran ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ⊆ 𝑆 ∧ 𝑆 ⊆ ℂ ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) ↔ ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn ( 𝐽 ↾t 𝑆 ) ) ) )
89 26 87 32 88 mp3an2i ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐽 ) ↔ ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn ( 𝐽 ↾t 𝑆 ) ) ) )
90 64 89 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn ( 𝐽 ↾t 𝑆 ) ) )
91 4 oveq2i ⊢ ( ( II ×t II ) Cn 𝐾 ) = ( ( II ×t II ) Cn ( 𝐽 ↾t 𝑆 ) )
92 90 91 eleqtrrdi ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( ( II ×t II ) Cn 𝐾 ) )
93 simpr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ( 0 [,] 1 ) )
94 simpr ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → 𝑡 = 0 )
95 94 oveq1d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( 𝑡 · ( 𝑓 ‘ 0 ) ) = ( 0 · ( 𝑓 ‘ 0 ) ) )
96 94 oveq2d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( 1 − 𝑡 ) = ( 1 − 0 ) )
97 1m0e1 ⊢ ( 1 − 0 ) = 1
98 96 97 eqtrdi ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( 1 − 𝑡 ) = 1 )
99 simpl ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → 𝑧 = 𝑠 )
100 99 fveq2d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑠 ) )
101 98 100 oveq12d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) = ( 1 · ( 𝑓 ‘ 𝑠 ) ) )
102 95 101 oveq12d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 0 ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) = ( ( 0 · ( 𝑓 ‘ 0 ) ) + ( 1 · ( 𝑓 ‘ 𝑠 ) ) ) )
103 ovex ⊢ ( ( 0 · ( 𝑓 ‘ 0 ) ) + ( 1 · ( 𝑓 ‘ 𝑠 ) ) ) ∈ V
104 102 84 103 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 0 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 0 ) = ( ( 0 · ( 𝑓 ‘ 0 ) ) + ( 1 · ( 𝑓 ‘ 𝑠 ) ) ) )
105 93 16 104 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 0 ) = ( ( 0 · ( 𝑓 ‘ 0 ) ) + ( 1 · ( 𝑓 ‘ 𝑠 ) ) ) )
106 40 adantr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 0 ) ∈ ℂ )
107 106 mul02d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 · ( 𝑓 ‘ 0 ) ) = 0 )
108 26 toponunii ⊢ ℂ = ∪ 𝐽
109 12 108 cnf ⊢ ( 𝑓 ∈ ( II Cn 𝐽 ) → 𝑓 : ( 0 [,] 1 ) ⟶ ℂ )
110 58 109 syl ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 : ( 0 [,] 1 ) ⟶ ℂ )
111 110 ffvelcdmda ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 𝑠 ) ∈ ℂ )
112 111 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 𝑓 ‘ 𝑠 ) ) = ( 𝑓 ‘ 𝑠 ) )
113 107 112 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 0 · ( 𝑓 ‘ 0 ) ) + ( 1 · ( 𝑓 ‘ 𝑠 ) ) ) = ( 0 + ( 𝑓 ‘ 𝑠 ) ) )
114 111 addlidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 + ( 𝑓 ‘ 𝑠 ) ) = ( 𝑓 ‘ 𝑠 ) )
115 105 113 114 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 0 ) = ( 𝑓 ‘ 𝑠 ) )
116 1elunit ⊢ 1 ∈ ( 0 [,] 1 )
117 simpr ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → 𝑡 = 1 )
118 117 oveq1d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( 𝑡 · ( 𝑓 ‘ 0 ) ) = ( 1 · ( 𝑓 ‘ 0 ) ) )
119 117 oveq2d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( 1 − 𝑡 ) = ( 1 − 1 ) )
120 1m1e0 ⊢ ( 1 − 1 ) = 0
121 119 120 eqtrdi ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( 1 − 𝑡 ) = 0 )
122 simpl ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → 𝑧 = 𝑠 )
123 122 fveq2d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 𝑠 ) )
124 121 123 oveq12d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) = ( 0 · ( 𝑓 ‘ 𝑠 ) ) )
125 118 124 oveq12d ⊢ ( ( 𝑧 = 𝑠 ∧ 𝑡 = 1 ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) = ( ( 1 · ( 𝑓 ‘ 0 ) ) + ( 0 · ( 𝑓 ‘ 𝑠 ) ) ) )
126 ovex ⊢ ( ( 1 · ( 𝑓 ‘ 0 ) ) + ( 0 · ( 𝑓 ‘ 𝑠 ) ) ) ∈ V
127 125 84 126 ovmpoa ⊢ ( ( 𝑠 ∈ ( 0 [,] 1 ) ∧ 1 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 1 ) = ( ( 1 · ( 𝑓 ‘ 0 ) ) + ( 0 · ( 𝑓 ‘ 𝑠 ) ) ) )
128 93 116 127 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 1 ) = ( ( 1 · ( 𝑓 ‘ 0 ) ) + ( 0 · ( 𝑓 ‘ 𝑠 ) ) ) )
129 106 mullidd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 · ( 𝑓 ‘ 0 ) ) = ( 𝑓 ‘ 0 ) )
130 111 mul02d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 · ( 𝑓 ‘ 𝑠 ) ) = 0 )
131 129 130 oveq12d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 1 · ( 𝑓 ‘ 0 ) ) + ( 0 · ( 𝑓 ‘ 𝑠 ) ) ) = ( ( 𝑓 ‘ 0 ) + 0 ) )
132 106 addridd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑓 ‘ 0 ) + 0 ) = ( 𝑓 ‘ 0 ) )
133 fvex ⊢ ( 𝑓 ‘ 0 ) ∈ V
134 133 fvconst2 ⊢ ( 𝑠 ∈ ( 0 [,] 1 ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝑓 ‘ 0 ) )
135 134 adantl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑠 ) = ( 𝑓 ‘ 0 ) )
136 132 135 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑓 ‘ 0 ) + 0 ) = ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑠 ) )
137 128 131 136 3eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 1 ) = ( ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ‘ 𝑠 ) )
138 simpr ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → 𝑡 = 𝑠 )
139 138 oveq1d ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → ( 𝑡 · ( 𝑓 ‘ 0 ) ) = ( 𝑠 · ( 𝑓 ‘ 0 ) ) )
140 138 oveq2d ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → ( 1 − 𝑡 ) = ( 1 − 𝑠 ) )
141 simpl ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → 𝑧 = 0 )
142 141 fveq2d ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 0 ) )
143 140 142 oveq12d ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) = ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) )
144 139 143 oveq12d ⊢ ( ( 𝑧 = 0 ∧ 𝑡 = 𝑠 ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) )
145 ovex ⊢ ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) ∈ V
146 144 84 145 ovmpoa ⊢ ( ( 0 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) )
147 16 93 146 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) )
148 28 93 sselid ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → 𝑠 ∈ ℂ )
149 pncan3 ⊢ ( ( 𝑠 ∈ ℂ ∧ 1 ∈ ℂ ) → ( 𝑠 + ( 1 − 𝑠 ) ) = 1 )
150 148 46 149 sylancl ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑠 + ( 1 − 𝑠 ) ) = 1 )
151 150 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 + ( 1 − 𝑠 ) ) · ( 𝑓 ‘ 0 ) ) = ( 1 · ( 𝑓 ‘ 0 ) ) )
152 subcl ⊢ ( ( 1 ∈ ℂ ∧ 𝑠 ∈ ℂ ) → ( 1 − 𝑠 ) ∈ ℂ )
153 46 148 152 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 − 𝑠 ) ∈ ℂ )
154 148 153 106 adddird ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 + ( 1 − 𝑠 ) ) · ( 𝑓 ‘ 0 ) ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) )
155 151 154 129 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) = ( 𝑓 ‘ 0 ) )
156 147 155 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 0 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( 𝑓 ‘ 0 ) )
157 simpr ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → 𝑡 = 𝑠 )
158 157 oveq1d ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → ( 𝑡 · ( 𝑓 ‘ 0 ) ) = ( 𝑠 · ( 𝑓 ‘ 0 ) ) )
159 157 oveq2d ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → ( 1 − 𝑡 ) = ( 1 − 𝑠 ) )
160 simpl ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → 𝑧 = 1 )
161 160 fveq2d ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → ( 𝑓 ‘ 𝑧 ) = ( 𝑓 ‘ 1 ) )
162 159 161 oveq12d ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) = ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) )
163 158 162 oveq12d ⊢ ( ( 𝑧 = 1 ∧ 𝑡 = 𝑠 ) → ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) )
164 ovex ⊢ ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) ∈ V
165 163 84 164 ovmpoa ⊢ ( ( 1 ∈ ( 0 [,] 1 ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) )
166 116 93 165 sylancr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) )
167 simplrr ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) )
168 167 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) = ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) )
169 168 oveq2d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 0 ) ) ) = ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) )
170 155 169 167 3eqtr3d ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( ( 𝑠 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑠 ) · ( 𝑓 ‘ 1 ) ) ) = ( 𝑓 ‘ 1 ) )
171 166 170 eqtrd ⊢ ( ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) ∧ 𝑠 ∈ ( 0 [,] 1 ) ) → ( 1 ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) 𝑠 ) = ( 𝑓 ‘ 1 ) )
172 6 22 92 115 137 156 171 isphtpy2d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑧 ∈ ( 0 [,] 1 ) , 𝑡 ∈ ( 0 [,] 1 ) ↦ ( ( 𝑡 · ( 𝑓 ‘ 0 ) ) + ( ( 1 − 𝑡 ) · ( 𝑓 ‘ 𝑧 ) ) ) ) ∈ ( 𝑓 ( PHtpy ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
173 172 ne0d ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → ( 𝑓 ( PHtpy ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ≠ ∅ )
174 isphtpc ⊢ ( 𝑓 ( ≃ph ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ↔ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ( PHtpy ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ≠ ∅ ) )
175 6 22 173 174 syl3anbrc ⊢ ( ( 𝜑 ∧ ( 𝑓 ∈ ( II Cn 𝐾 ) ∧ ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) ) ) → 𝑓 ( ≃ph ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) )
176 175 expr ⊢ ( ( 𝜑 ∧ 𝑓 ∈ ( II Cn 𝐾 ) ) → ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
177 176 ralrimiva ⊢ ( 𝜑 → ∀ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) )
178 issconn ⊢ ( 𝐾 ∈ SConn ↔ ( 𝐾 ∈ PConn ∧ ∀ 𝑓 ∈ ( II Cn 𝐾 ) ( ( 𝑓 ‘ 0 ) = ( 𝑓 ‘ 1 ) → 𝑓 ( ≃ph ‘ 𝐾 ) ( ( 0 [,] 1 ) × { ( 𝑓 ‘ 0 ) } ) ) ) )
179 5 177 178 sylanbrc ⊢ ( 𝜑 → 𝐾 ∈ SConn )