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