Users' Mathboxes Mathbox for Mario Carneiro < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  cvxsconn Structured version   Visualization version   GIF version

Theorem cvxsconn 31557
Description: A convex subset of the complex numbers is simply connected. (Contributed by Mario Carneiro, 12-Feb-2015.)
Hypotheses
Ref Expression
cvxpconn.1 (𝜑𝑆 ⊆ ℂ)
cvxpconn.2 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
cvxpconn.3 𝐽 = (TopOpen‘ℂfld)
cvxpconn.4 𝐾 = (𝐽t 𝑆)
Assertion
Ref Expression
cvxsconn (𝜑𝐾 ∈ SConn)
Distinct variable groups:   𝑡,𝐽   𝑥,𝑡,𝑦,𝐾   𝜑,𝑡,𝑥,𝑦   𝑡,𝑆,𝑥,𝑦
Allowed substitution hints:   𝐽(𝑥,𝑦)

Proof of Theorem cvxsconn
Dummy variables 𝑧 𝑓 𝑠 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 cvxpconn.1 . . 3 (𝜑𝑆 ⊆ ℂ)
2 cvxpconn.2 . . 3 ((𝜑 ∧ (𝑥𝑆𝑦𝑆𝑡 ∈ (0[,]1))) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
3 cvxpconn.3 . . 3 𝐽 = (TopOpen‘ℂfld)
4 cvxpconn.4 . . 3 𝐾 = (𝐽t 𝑆)
51, 2, 3, 4cvxpconn 31556 . 2 (𝜑𝐾 ∈ PConn)
6 simprl 746 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓 ∈ (II Cn 𝐾))
7 pconntop 31539 . . . . . . . . . 10 (𝐾 ∈ PConn → 𝐾 ∈ Top)
85, 7syl 17 . . . . . . . . 9 (𝜑𝐾 ∈ Top)
98adantr 466 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝐾 ∈ Top)
10 eqid 2770 . . . . . . . . 9 𝐾 = 𝐾
1110toptopon 20941 . . . . . . . 8 (𝐾 ∈ Top ↔ 𝐾 ∈ (TopOn‘ 𝐾))
129, 11sylib 208 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝐾 ∈ (TopOn‘ 𝐾))
13 iiuni 22903 . . . . . . . . . 10 (0[,]1) = II
1413, 10cnf 21270 . . . . . . . . 9 (𝑓 ∈ (II Cn 𝐾) → 𝑓:(0[,]1)⟶ 𝐾)
156, 14syl 17 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓:(0[,]1)⟶ 𝐾)
16 0elunit 12496 . . . . . . . 8 0 ∈ (0[,]1)
17 ffvelrn 6500 . . . . . . . 8 ((𝑓:(0[,]1)⟶ 𝐾 ∧ 0 ∈ (0[,]1)) → (𝑓‘0) ∈ 𝐾)
1815, 16, 17sylancl 566 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓‘0) ∈ 𝐾)
19 eqid 2770 . . . . . . . 8 ((0[,]1) × {(𝑓‘0)}) = ((0[,]1) × {(𝑓‘0)})
2019pcoptcl 23039 . . . . . . 7 ((𝐾 ∈ (TopOn‘ 𝐾) ∧ (𝑓‘0) ∈ 𝐾) → (((0[,]1) × {(𝑓‘0)}) ∈ (II Cn 𝐾) ∧ (((0[,]1) × {(𝑓‘0)})‘0) = (𝑓‘0) ∧ (((0[,]1) × {(𝑓‘0)})‘1) = (𝑓‘0)))
2112, 18, 20syl2anc 565 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (((0[,]1) × {(𝑓‘0)}) ∈ (II Cn 𝐾) ∧ (((0[,]1) × {(𝑓‘0)})‘0) = (𝑓‘0) ∧ (((0[,]1) × {(𝑓‘0)})‘1) = (𝑓‘0)))
2221simp1d 1135 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → ((0[,]1) × {(𝑓‘0)}) ∈ (II Cn 𝐾))
23 iitopon 22901 . . . . . . . . . . 11 II ∈ (TopOn‘(0[,]1))
2423a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → II ∈ (TopOn‘(0[,]1)))
253dfii3 22905 . . . . . . . . . . . 12 II = (𝐽t (0[,]1))
263cnfldtopon 22805 . . . . . . . . . . . . 13 𝐽 ∈ (TopOn‘ℂ)
2726a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝐽 ∈ (TopOn‘ℂ))
28 unitssre 12525 . . . . . . . . . . . . . 14 (0[,]1) ⊆ ℝ
29 ax-resscn 10194 . . . . . . . . . . . . . 14 ℝ ⊆ ℂ
3028, 29sstri 3759 . . . . . . . . . . . . 13 (0[,]1) ⊆ ℂ
3130a1i 11 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (0[,]1) ⊆ ℂ)
3227, 27cnmpt2nd 21692 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ ℂ, 𝑡 ∈ ℂ ↦ 𝑡) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
3325, 27, 31, 25, 27, 31, 32cnmpt2res 21700 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑡) ∈ ((II ×t II) Cn 𝐽))
341adantr 466 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 ⊆ ℂ)
35 resttopon 21185 . . . . . . . . . . . . . . . . . 18 ((𝐽 ∈ (TopOn‘ℂ) ∧ 𝑆 ⊆ ℂ) → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
3626, 1, 35sylancr 567 . . . . . . . . . . . . . . . . 17 (𝜑 → (𝐽t 𝑆) ∈ (TopOn‘𝑆))
374, 36syl5eqel 2853 . . . . . . . . . . . . . . . 16 (𝜑𝐾 ∈ (TopOn‘𝑆))
38 toponuni 20938 . . . . . . . . . . . . . . . 16 (𝐾 ∈ (TopOn‘𝑆) → 𝑆 = 𝐾)
3937, 38syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 = 𝐾)
4039adantr 466 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑆 = 𝐾)
4118, 40eleqtrrd 2852 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓‘0) ∈ 𝑆)
4234, 41sseldd 3751 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓‘0) ∈ ℂ)
4324, 24, 27, 42cnmpt2c 21693 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝑓‘0)) ∈ ((II ×t II) Cn 𝐽))
443mulcn 22889 . . . . . . . . . . . 12 · ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
4544a1i 11 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → · ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
4624, 24, 33, 43, 45cnmpt22f 21698 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝑡 · (𝑓‘0))) ∈ ((II ×t II) Cn 𝐽))
47 ax-1cn 10195 . . . . . . . . . . . . . . 15 1 ∈ ℂ
4847a1i 11 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 1 ∈ ℂ)
4927, 27, 27, 48cnmpt2c 21693 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ ℂ, 𝑡 ∈ ℂ ↦ 1) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
503subcn 22888 . . . . . . . . . . . . . 14 − ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
5150a1i 11 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → − ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
5227, 27, 49, 32, 51cnmpt22f 21698 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ ℂ, 𝑡 ∈ ℂ ↦ (1 − 𝑡)) ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
5325, 27, 31, 25, 27, 31, 52cnmpt2res 21700 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (1 − 𝑡)) ∈ ((II ×t II) Cn 𝐽))
5424, 24cnmpt1st 21691 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ 𝑧) ∈ ((II ×t II) Cn II))
553cnfldtop 22806 . . . . . . . . . . . . . 14 𝐽 ∈ Top
56 cnrest2r 21311 . . . . . . . . . . . . . 14 (𝐽 ∈ Top → (II Cn (𝐽t 𝑆)) ⊆ (II Cn 𝐽))
5755, 56ax-mp 5 . . . . . . . . . . . . 13 (II Cn (𝐽t 𝑆)) ⊆ (II Cn 𝐽)
584oveq2i 6803 . . . . . . . . . . . . . 14 (II Cn 𝐾) = (II Cn (𝐽t 𝑆))
596, 58syl6eleq 2859 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓 ∈ (II Cn (𝐽t 𝑆)))
6057, 59sseldi 3748 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓 ∈ (II Cn 𝐽))
6124, 24, 54, 60cnmpt21f 21695 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ (𝑓𝑧)) ∈ ((II ×t II) Cn 𝐽))
6224, 24, 53, 61, 45cnmpt22f 21698 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((1 − 𝑡) · (𝑓𝑧))) ∈ ((II ×t II) Cn 𝐽))
633addcn 22887 . . . . . . . . . . 11 + ∈ ((𝐽 ×t 𝐽) Cn 𝐽)
6463a1i 11 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → + ∈ ((𝐽 ×t 𝐽) Cn 𝐽))
6524, 24, 46, 62, 64cnmpt22f 21698 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ∈ ((II ×t II) Cn 𝐽))
6641adantr 466 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → (𝑓‘0) ∈ 𝑆)
6715adantr 466 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → 𝑓:(0[,]1)⟶ 𝐾)
68 simprl 746 . . . . . . . . . . . . . . . 16 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → 𝑧 ∈ (0[,]1))
6967, 68ffvelrnd 6503 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → (𝑓𝑧) ∈ 𝐾)
7040adantr 466 . . . . . . . . . . . . . . 15 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → 𝑆 = 𝐾)
7169, 70eleqtrrd 2852 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → (𝑓𝑧) ∈ 𝑆)
7223exp2 1446 . . . . . . . . . . . . . . . . . 18 (𝜑 → (𝑥𝑆 → (𝑦𝑆 → (𝑡 ∈ (0[,]1) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆))))
7372imp42 413 . . . . . . . . . . . . . . . . 17 (((𝜑 ∧ (𝑥𝑆𝑦𝑆)) ∧ 𝑡 ∈ (0[,]1)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
7473an32s 623 . . . . . . . . . . . . . . . 16 (((𝜑𝑡 ∈ (0[,]1)) ∧ (𝑥𝑆𝑦𝑆)) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
7574ralrimivva 3119 . . . . . . . . . . . . . . 15 ((𝜑𝑡 ∈ (0[,]1)) → ∀𝑥𝑆𝑦𝑆 ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
7675ad2ant2rl 735 . . . . . . . . . . . . . 14 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → ∀𝑥𝑆𝑦𝑆 ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆)
77 oveq2 6800 . . . . . . . . . . . . . . . . 17 (𝑥 = (𝑓‘0) → (𝑡 · 𝑥) = (𝑡 · (𝑓‘0)))
7877oveq1d 6807 . . . . . . . . . . . . . . . 16 (𝑥 = (𝑓‘0) → ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · 𝑦)))
7978eleq1d 2834 . . . . . . . . . . . . . . 15 (𝑥 = (𝑓‘0) → (((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆 ↔ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆))
80 oveq2 6800 . . . . . . . . . . . . . . . . 17 (𝑦 = (𝑓𝑧) → ((1 − 𝑡) · 𝑦) = ((1 − 𝑡) · (𝑓𝑧)))
8180oveq2d 6808 . . . . . . . . . . . . . . . 16 (𝑦 = (𝑓𝑧) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · 𝑦)) = ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))
8281eleq1d 2834 . . . . . . . . . . . . . . 15 (𝑦 = (𝑓𝑧) → (((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆 ↔ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) ∈ 𝑆))
8379, 82rspc2va 3471 . . . . . . . . . . . . . 14 ((((𝑓‘0) ∈ 𝑆 ∧ (𝑓𝑧) ∈ 𝑆) ∧ ∀𝑥𝑆𝑦𝑆 ((𝑡 · 𝑥) + ((1 − 𝑡) · 𝑦)) ∈ 𝑆) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) ∈ 𝑆)
8466, 71, 76, 83syl21anc 1474 . . . . . . . . . . . . 13 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ (𝑧 ∈ (0[,]1) ∧ 𝑡 ∈ (0[,]1))) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) ∈ 𝑆)
8584ralrimivva 3119 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → ∀𝑧 ∈ (0[,]1)∀𝑡 ∈ (0[,]1)((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) ∈ 𝑆)
86 eqid 2770 . . . . . . . . . . . . 13 (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) = (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))
8786fmpt2 7386 . . . . . . . . . . . 12 (∀𝑧 ∈ (0[,]1)∀𝑡 ∈ (0[,]1)((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) ∈ 𝑆 ↔ (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))):((0[,]1) × (0[,]1))⟶𝑆)
8885, 87sylib 208 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))):((0[,]1) × (0[,]1))⟶𝑆)
89 frn 6193 . . . . . . . . . . 11 ((𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))):((0[,]1) × (0[,]1))⟶𝑆 → ran (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ⊆ 𝑆)
9088, 89syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → ran (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ⊆ 𝑆)
91 cnrest2 21310 . . . . . . . . . 10 ((𝐽 ∈ (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 𝑆))))
9227, 90, 34, 91syl3anc 1475 . . . . . . . . 9 ((𝜑 ∧ (𝑓 ∈ (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 𝑆))))
9365, 92mpbid 222 . . . . . . . 8 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ∈ ((II ×t II) Cn (𝐽t 𝑆)))
944oveq2i 6803 . . . . . . . 8 ((II ×t II) Cn 𝐾) = ((II ×t II) Cn (𝐽t 𝑆))
9593, 94syl6eleqr 2860 . . . . . . 7 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ∈ ((II ×t II) Cn 𝐾))
96 simpr 471 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ (0[,]1))
97 simpr 471 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 0) → 𝑡 = 0)
9897oveq1d 6807 . . . . . . . . . . 11 ((𝑧 = 𝑠𝑡 = 0) → (𝑡 · (𝑓‘0)) = (0 · (𝑓‘0)))
9997oveq2d 6808 . . . . . . . . . . . . 13 ((𝑧 = 𝑠𝑡 = 0) → (1 − 𝑡) = (1 − 0))
100 1m0e1 11332 . . . . . . . . . . . . 13 (1 − 0) = 1
10199, 100syl6eq 2820 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 0) → (1 − 𝑡) = 1)
102 simpl 468 . . . . . . . . . . . . 13 ((𝑧 = 𝑠𝑡 = 0) → 𝑧 = 𝑠)
103102fveq2d 6336 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 0) → (𝑓𝑧) = (𝑓𝑠))
104101, 103oveq12d 6810 . . . . . . . . . . 11 ((𝑧 = 𝑠𝑡 = 0) → ((1 − 𝑡) · (𝑓𝑧)) = (1 · (𝑓𝑠)))
10598, 104oveq12d 6810 . . . . . . . . . 10 ((𝑧 = 𝑠𝑡 = 0) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) = ((0 · (𝑓‘0)) + (1 · (𝑓𝑠))))
106 ovex 6822 . . . . . . . . . 10 ((0 · (𝑓‘0)) + (1 · (𝑓𝑠))) ∈ V
107105, 86, 106ovmpt2a 6937 . . . . . . . . 9 ((𝑠 ∈ (0[,]1) ∧ 0 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))0) = ((0 · (𝑓‘0)) + (1 · (𝑓𝑠))))
10896, 16, 107sylancl 566 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))0) = ((0 · (𝑓‘0)) + (1 · (𝑓𝑠))))
10942adantr 466 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑓‘0) ∈ ℂ)
110109mul02d 10435 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (0 · (𝑓‘0)) = 0)
11126toponunii 20940 . . . . . . . . . . . . 13 ℂ = 𝐽
11213, 111cnf 21270 . . . . . . . . . . . 12 (𝑓 ∈ (II Cn 𝐽) → 𝑓:(0[,]1)⟶ℂ)
11360, 112syl 17 . . . . . . . . . . 11 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓:(0[,]1)⟶ℂ)
114113ffvelrnda 6502 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑓𝑠) ∈ ℂ)
115114mulid2d 10259 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (1 · (𝑓𝑠)) = (𝑓𝑠))
116110, 115oveq12d 6810 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((0 · (𝑓‘0)) + (1 · (𝑓𝑠))) = (0 + (𝑓𝑠)))
117114addid2d 10438 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (0 + (𝑓𝑠)) = (𝑓𝑠))
118108, 116, 1173eqtrd 2808 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))0) = (𝑓𝑠))
119 1elunit 12497 . . . . . . . . 9 1 ∈ (0[,]1)
120 simpr 471 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 1) → 𝑡 = 1)
121120oveq1d 6807 . . . . . . . . . . 11 ((𝑧 = 𝑠𝑡 = 1) → (𝑡 · (𝑓‘0)) = (1 · (𝑓‘0)))
122120oveq2d 6808 . . . . . . . . . . . . 13 ((𝑧 = 𝑠𝑡 = 1) → (1 − 𝑡) = (1 − 1))
123 1m1e0 11290 . . . . . . . . . . . . 13 (1 − 1) = 0
124122, 123syl6eq 2820 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 1) → (1 − 𝑡) = 0)
125 simpl 468 . . . . . . . . . . . . 13 ((𝑧 = 𝑠𝑡 = 1) → 𝑧 = 𝑠)
126125fveq2d 6336 . . . . . . . . . . . 12 ((𝑧 = 𝑠𝑡 = 1) → (𝑓𝑧) = (𝑓𝑠))
127124, 126oveq12d 6810 . . . . . . . . . . 11 ((𝑧 = 𝑠𝑡 = 1) → ((1 − 𝑡) · (𝑓𝑧)) = (0 · (𝑓𝑠)))
128121, 127oveq12d 6810 . . . . . . . . . 10 ((𝑧 = 𝑠𝑡 = 1) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) = ((1 · (𝑓‘0)) + (0 · (𝑓𝑠))))
129 ovex 6822 . . . . . . . . . 10 ((1 · (𝑓‘0)) + (0 · (𝑓𝑠))) ∈ V
130128, 86, 129ovmpt2a 6937 . . . . . . . . 9 ((𝑠 ∈ (0[,]1) ∧ 1 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))1) = ((1 · (𝑓‘0)) + (0 · (𝑓𝑠))))
13196, 119, 130sylancl 566 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))1) = ((1 · (𝑓‘0)) + (0 · (𝑓𝑠))))
132109mulid2d 10259 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (1 · (𝑓‘0)) = (𝑓‘0))
133114mul02d 10435 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (0 · (𝑓𝑠)) = 0)
134132, 133oveq12d 6810 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((1 · (𝑓‘0)) + (0 · (𝑓𝑠))) = ((𝑓‘0) + 0))
135109addid1d 10437 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑓‘0) + 0) = (𝑓‘0))
136 fvex 6342 . . . . . . . . . . 11 (𝑓‘0) ∈ V
137136fvconst2 6612 . . . . . . . . . 10 (𝑠 ∈ (0[,]1) → (((0[,]1) × {(𝑓‘0)})‘𝑠) = (𝑓‘0))
138137adantl 467 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (((0[,]1) × {(𝑓‘0)})‘𝑠) = (𝑓‘0))
139135, 138eqtr4d 2807 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑓‘0) + 0) = (((0[,]1) × {(𝑓‘0)})‘𝑠))
140131, 134, 1393eqtrd 2808 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑠(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))1) = (((0[,]1) × {(𝑓‘0)})‘𝑠))
141 simpr 471 . . . . . . . . . . . 12 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → 𝑡 = 𝑠)
142141oveq1d 6807 . . . . . . . . . . 11 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → (𝑡 · (𝑓‘0)) = (𝑠 · (𝑓‘0)))
143141oveq2d 6808 . . . . . . . . . . . 12 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → (1 − 𝑡) = (1 − 𝑠))
144 simpl 468 . . . . . . . . . . . . 13 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → 𝑧 = 0)
145144fveq2d 6336 . . . . . . . . . . . 12 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → (𝑓𝑧) = (𝑓‘0))
146143, 145oveq12d 6810 . . . . . . . . . . 11 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → ((1 − 𝑡) · (𝑓𝑧)) = ((1 − 𝑠) · (𝑓‘0)))
147142, 146oveq12d 6810 . . . . . . . . . 10 ((𝑧 = 0 ∧ 𝑡 = 𝑠) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))))
148 ovex 6822 . . . . . . . . . 10 ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))) ∈ V
149147, 86, 148ovmpt2a 6937 . . . . . . . . 9 ((0 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (0(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))))
15016, 96, 149sylancr 567 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (0(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))))
15130, 96sseldi 3748 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → 𝑠 ∈ ℂ)
152 pncan3 10490 . . . . . . . . . . 11 ((𝑠 ∈ ℂ ∧ 1 ∈ ℂ) → (𝑠 + (1 − 𝑠)) = 1)
153151, 47, 152sylancl 566 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑠 + (1 − 𝑠)) = 1)
154153oveq1d 6807 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 + (1 − 𝑠)) · (𝑓‘0)) = (1 · (𝑓‘0)))
155 subcl 10481 . . . . . . . . . . 11 ((1 ∈ ℂ ∧ 𝑠 ∈ ℂ) → (1 − 𝑠) ∈ ℂ)
15647, 151, 155sylancr 567 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (1 − 𝑠) ∈ ℂ)
157151, 156, 109adddird 10266 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 + (1 − 𝑠)) · (𝑓‘0)) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))))
158154, 157, 1323eqtr3d 2812 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))) = (𝑓‘0))
159150, 158eqtrd 2804 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (0(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = (𝑓‘0))
160 simpr 471 . . . . . . . . . . . 12 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → 𝑡 = 𝑠)
161160oveq1d 6807 . . . . . . . . . . 11 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → (𝑡 · (𝑓‘0)) = (𝑠 · (𝑓‘0)))
162160oveq2d 6808 . . . . . . . . . . . 12 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → (1 − 𝑡) = (1 − 𝑠))
163 simpl 468 . . . . . . . . . . . . 13 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → 𝑧 = 1)
164163fveq2d 6336 . . . . . . . . . . . 12 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → (𝑓𝑧) = (𝑓‘1))
165162, 164oveq12d 6810 . . . . . . . . . . 11 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → ((1 − 𝑡) · (𝑓𝑧)) = ((1 − 𝑠) · (𝑓‘1)))
166161, 165oveq12d 6810 . . . . . . . . . 10 ((𝑧 = 1 ∧ 𝑡 = 𝑠) → ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))))
167 ovex 6822 . . . . . . . . . 10 ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))) ∈ V
168166, 86, 167ovmpt2a 6937 . . . . . . . . 9 ((1 ∈ (0[,]1) ∧ 𝑠 ∈ (0[,]1)) → (1(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))))
169119, 96, 168sylancr 567 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (1(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))))
170 simplrr 755 . . . . . . . . . . 11 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (𝑓‘0) = (𝑓‘1))
171170oveq2d 6808 . . . . . . . . . 10 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((1 − 𝑠) · (𝑓‘0)) = ((1 − 𝑠) · (𝑓‘1)))
172171oveq2d 6808 . . . . . . . . 9 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘0))) = ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))))
173158, 172, 1703eqtr3d 2812 . . . . . . . 8 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → ((𝑠 · (𝑓‘0)) + ((1 − 𝑠) · (𝑓‘1))) = (𝑓‘1))
174169, 173eqtrd 2804 . . . . . . 7 (((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) ∧ 𝑠 ∈ (0[,]1)) → (1(𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧))))𝑠) = (𝑓‘1))
1756, 22, 95, 118, 140, 159, 174isphtpy2d 23005 . . . . . 6 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ∈ (𝑓(PHtpy‘𝐾)((0[,]1) × {(𝑓‘0)})))
176 ne0i 4067 . . . . . 6 ((𝑧 ∈ (0[,]1), 𝑡 ∈ (0[,]1) ↦ ((𝑡 · (𝑓‘0)) + ((1 − 𝑡) · (𝑓𝑧)))) ∈ (𝑓(PHtpy‘𝐾)((0[,]1) × {(𝑓‘0)})) → (𝑓(PHtpy‘𝐾)((0[,]1) × {(𝑓‘0)})) ≠ ∅)
177175, 176syl 17 . . . . 5 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → (𝑓(PHtpy‘𝐾)((0[,]1) × {(𝑓‘0)})) ≠ ∅)
178 isphtpc 23012 . . . . 5 (𝑓( ≃ph𝐾)((0[,]1) × {(𝑓‘0)}) ↔ (𝑓 ∈ (II Cn 𝐾) ∧ ((0[,]1) × {(𝑓‘0)}) ∈ (II Cn 𝐾) ∧ (𝑓(PHtpy‘𝐾)((0[,]1) × {(𝑓‘0)})) ≠ ∅))
1796, 22, 177, 178syl3anbrc 1427 . . . 4 ((𝜑 ∧ (𝑓 ∈ (II Cn 𝐾) ∧ (𝑓‘0) = (𝑓‘1))) → 𝑓( ≃ph𝐾)((0[,]1) × {(𝑓‘0)}))
180179expr 444 . . 3 ((𝜑𝑓 ∈ (II Cn 𝐾)) → ((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝐾)((0[,]1) × {(𝑓‘0)})))
181180ralrimiva 3114 . 2 (𝜑 → ∀𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝐾)((0[,]1) × {(𝑓‘0)})))
182 issconn 31540 . 2 (𝐾 ∈ SConn ↔ (𝐾 ∈ PConn ∧ ∀𝑓 ∈ (II Cn 𝐾)((𝑓‘0) = (𝑓‘1) → 𝑓( ≃ph𝐾)((0[,]1) × {(𝑓‘0)}))))
1835, 181, 182sylanbrc 564 1 (𝜑𝐾 ∈ SConn)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 382  w3a 1070   = wceq 1630  wcel 2144  wne 2942  wral 3060  wss 3721  c0 4061  {csn 4314   cuni 4572   class class class wbr 4784   × cxp 5247  ran crn 5250  wf 6027  cfv 6031  (class class class)co 6792  cmpt2 6794  cc 10135  cr 10136  0cc0 10137  1c1 10138   + caddc 10140   · cmul 10142  cmin 10467  [,]cicc 12382  t crest 16288  TopOpenctopn 16289  fldccnfld 19960  Topctop 20917  TopOnctopon 20934   Cn ccn 21248   ×t ctx 21583  IIcii 22897  PHtpycphtpy 22986  phcphtpc 22987  PConncpconn 31533  SConncsconn 31534
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-8 2146  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750  ax-rep 4902  ax-sep 4912  ax-nul 4920  ax-pow 4971  ax-pr 5034  ax-un 7095  ax-inf2 8701  ax-cnex 10193  ax-resscn 10194  ax-1cn 10195  ax-icn 10196  ax-addcl 10197  ax-addrcl 10198  ax-mulcl 10199  ax-mulrcl 10200  ax-mulcom 10201  ax-addass 10202  ax-mulass 10203  ax-distr 10204  ax-i2m1 10205  ax-1ne0 10206  ax-1rid 10207  ax-rnegex 10208  ax-rrecex 10209  ax-cnre 10210  ax-pre-lttri 10211  ax-pre-lttrn 10212  ax-pre-ltadd 10213  ax-pre-mulgt0 10214  ax-pre-sup 10215  ax-addf 10216  ax-mulf 10217
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-3or 1071  df-3an 1072  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-eu 2621  df-mo 2622  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-ne 2943  df-nel 3046  df-ral 3065  df-rex 3066  df-reu 3067  df-rmo 3068  df-rab 3069  df-v 3351  df-sbc 3586  df-csb 3681  df-dif 3724  df-un 3726  df-in 3728  df-ss 3735  df-pss 3737  df-nul 4062  df-if 4224  df-pw 4297  df-sn 4315  df-pr 4317  df-tp 4319  df-op 4321  df-uni 4573  df-int 4610  df-iun 4654  df-iin 4655  df-br 4785  df-opab 4845  df-mpt 4862  df-tr 4885  df-id 5157  df-eprel 5162  df-po 5170  df-so 5171  df-fr 5208  df-se 5209  df-we 5210  df-xp 5255  df-rel 5256  df-cnv 5257  df-co 5258  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262  df-pred 5823  df-ord 5869  df-on 5870  df-lim 5871  df-suc 5872  df-iota 5994  df-fun 6033  df-fn 6034  df-f 6035  df-f1 6036  df-fo 6037  df-f1o 6038  df-fv 6039  df-isom 6040  df-riota 6753  df-ov 6795  df-oprab 6796  df-mpt2 6797  df-of 7043  df-om 7212  df-1st 7314  df-2nd 7315  df-supp 7446  df-wrecs 7558  df-recs 7620  df-rdg 7658  df-1o 7712  df-2o 7713  df-oadd 7716  df-er 7895  df-map 8010  df-ixp 8062  df-en 8109  df-dom 8110  df-sdom 8111  df-fin 8112  df-fsupp 8431  df-fi 8472  df-sup 8503  df-inf 8504  df-oi 8570  df-card 8964  df-cda 9191  df-pnf 10277  df-mnf 10278  df-xr 10279  df-ltxr 10280  df-le 10281  df-sub 10469  df-neg 10470  df-div 10886  df-nn 11222  df-2 11280  df-3 11281  df-4 11282  df-5 11283  df-6 11284  df-7 11285  df-8 11286  df-9 11287  df-n0 11494  df-z 11579  df-dec 11695  df-uz 11888  df-q 11991  df-rp 12035  df-xneg 12150  df-xadd 12151  df-xmul 12152  df-icc 12386  df-fz 12533  df-fzo 12673  df-seq 13008  df-exp 13067  df-hash 13321  df-cj 14046  df-re 14047  df-im 14048  df-sqrt 14182  df-abs 14183  df-struct 16065  df-ndx 16066  df-slot 16067  df-base 16069  df-sets 16070  df-ress 16071  df-plusg 16161  df-mulr 16162  df-starv 16163  df-sca 16164  df-vsca 16165  df-ip 16166  df-tset 16167  df-ple 16168  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16290  df-topn 16291  df-0g 16309  df-gsum 16310  df-topgen 16311  df-pt 16312  df-prds 16315  df-xrs 16369  df-qtop 16374  df-imas 16375  df-xps 16377  df-mre 16453  df-mrc 16454  df-acs 16456  df-mgm 17449  df-sgrp 17491  df-mnd 17502  df-submnd 17543  df-mulg 17748  df-cntz 17956  df-cmn 18401  df-psmet 19952  df-xmet 19953  df-met 19954  df-bl 19955  df-mopn 19956  df-cnfld 19961  df-top 20918  df-topon 20935  df-topsp 20957  df-bases 20970  df-cn 21251  df-cnp 21252  df-tx 21585  df-hmeo 21778  df-xms 22344  df-ms 22345  df-tms 22346  df-ii 22899  df-htpy 22988  df-phtpy 22989  df-phtpc 23010  df-pconn 31535  df-sconn 31536
This theorem is referenced by:  blsconn  31558  resconn  31560
  Copyright terms: Public domain W3C validator