MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  blocni Structured version   Visualization version   GIF version

Theorem blocni 28349
Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.)
Hypotheses
Ref Expression
blocni.8 𝐶 = (IndMet‘𝑈)
blocni.d 𝐷 = (IndMet‘𝑊)
blocni.j 𝐽 = (MetOpen‘𝐶)
blocni.k 𝐾 = (MetOpen‘𝐷)
blocni.4 𝐿 = (𝑈 LnOp 𝑊)
blocni.5 𝐵 = (𝑈 BLnOp 𝑊)
blocni.u 𝑈 ∈ NrmCVec
blocni.w 𝑊 ∈ NrmCVec
blocni.l 𝑇𝐿
Assertion
Ref Expression
blocni (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇𝐵)

Proof of Theorem blocni
Dummy variables 𝑥 𝑤 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 blocni.u . . . 4 𝑈 ∈ NrmCVec
2 eqid 2772 . . . . 5 (BaseSet‘𝑈) = (BaseSet‘𝑈)
3 eqid 2772 . . . . 5 (0vec𝑈) = (0vec𝑈)
42, 3nvzcl 28178 . . . 4 (𝑈 ∈ NrmCVec → (0vec𝑈) ∈ (BaseSet‘𝑈))
51, 4ax-mp 5 . . 3 (0vec𝑈) ∈ (BaseSet‘𝑈)
6 blocni.8 . . . . . . . . . 10 𝐶 = (IndMet‘𝑈)
72, 6imsmet 28235 . . . . . . . . 9 (𝑈 ∈ NrmCVec → 𝐶 ∈ (Met‘(BaseSet‘𝑈)))
81, 7ax-mp 5 . . . . . . . 8 𝐶 ∈ (Met‘(BaseSet‘𝑈))
9 metxmet 22637 . . . . . . . 8 (𝐶 ∈ (Met‘(BaseSet‘𝑈)) → 𝐶 ∈ (∞Met‘(BaseSet‘𝑈)))
108, 9ax-mp 5 . . . . . . 7 𝐶 ∈ (∞Met‘(BaseSet‘𝑈))
11 blocni.j . . . . . . . 8 𝐽 = (MetOpen‘𝐶)
1211mopntopon 22742 . . . . . . 7 (𝐶 ∈ (∞Met‘(BaseSet‘𝑈)) → 𝐽 ∈ (TopOn‘(BaseSet‘𝑈)))
1310, 12ax-mp 5 . . . . . 6 𝐽 ∈ (TopOn‘(BaseSet‘𝑈))
1413toponunii 21218 . . . . 5 (BaseSet‘𝑈) = 𝐽
1514cncnpi 21580 . . . 4 ((𝑇 ∈ (𝐽 Cn 𝐾) ∧ (0vec𝑈) ∈ (BaseSet‘𝑈)) → 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec𝑈)))
165, 15mpan2 678 . . 3 (𝑇 ∈ (𝐽 Cn 𝐾) → 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec𝑈)))
17 blocni.d . . . 4 𝐷 = (IndMet‘𝑊)
18 blocni.k . . . 4 𝐾 = (MetOpen‘𝐷)
19 blocni.4 . . . 4 𝐿 = (𝑈 LnOp 𝑊)
20 blocni.5 . . . 4 𝐵 = (𝑈 BLnOp 𝑊)
21 blocni.w . . . 4 𝑊 ∈ NrmCVec
22 blocni.l . . . 4 𝑇𝐿
236, 17, 11, 18, 19, 20, 1, 21, 22, 2blocnilem 28348 . . 3 (((0vec𝑈) ∈ (BaseSet‘𝑈) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec𝑈))) → 𝑇𝐵)
245, 16, 23sylancr 578 . 2 (𝑇 ∈ (𝐽 Cn 𝐾) → 𝑇𝐵)
25 eleq1 2847 . . 3 (𝑇 = (𝑈 0op 𝑊) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾)))
26 simprr 760 . . . . . . . 8 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
27 eqid 2772 . . . . . . . . . . . . 13 (BaseSet‘𝑊) = (BaseSet‘𝑊)
28 eqid 2772 . . . . . . . . . . . . 13 (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊)
292, 27, 28, 20nmblore 28330 . . . . . . . . . . . 12 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐵) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ)
301, 21, 29mp3an12 1430 . . . . . . . . . . 11 (𝑇𝐵 → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ)
31 eqid 2772 . . . . . . . . . . . . . 14 (𝑈 0op 𝑊) = (𝑈 0op 𝑊)
3228, 31, 19nmlnogt0 28341 . . . . . . . . . . . . 13 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
331, 21, 22, 32mp3an 1440 . . . . . . . . . . . 12 (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))
3433biimpi 208 . . . . . . . . . . 11 (𝑇 ≠ (𝑈 0op 𝑊) → 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))
3530, 34anim12i 603 . . . . . . . . . 10 ((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
36 elrp 12199 . . . . . . . . . 10 (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+ ↔ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
3735, 36sylibr 226 . . . . . . . . 9 ((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+)
3837adantr 473 . . . . . . . 8 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+)
3926, 38rpdivcld 12258 . . . . . . 7 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈ ℝ+)
40 simprl 758 . . . . . . . . . . 11 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ (BaseSet‘𝑈))
41 metcl 22635 . . . . . . . . . . . 12 ((𝐶 ∈ (Met‘(BaseSet‘𝑈)) ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
428, 41mp3an1 1427 . . . . . . . . . . 11 ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
4340, 42sylan 572 . . . . . . . . . 10 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
44 simplrr 765 . . . . . . . . . . 11 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ+)
4544rpred 12241 . . . . . . . . . 10 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ)
4635ad2antrr 713 . . . . . . . . . 10 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
47 ltmuldiv2 11307 . . . . . . . . . 10 (((𝑥𝐶𝑤) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
4843, 45, 46, 47syl3anc 1351 . . . . . . . . 9 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
49 id 22 . . . . . . . . . . . 12 ((𝑇𝐵𝑥 ∈ (BaseSet‘𝑈)) → (𝑇𝐵𝑥 ∈ (BaseSet‘𝑈)))
5049ad2ant2r 734 . . . . . . . . . . 11 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑇𝐵𝑥 ∈ (BaseSet‘𝑈)))
512, 27, 6, 17, 28, 20, 1, 21blometi 28347 . . . . . . . . . . . 12 ((𝑇𝐵𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
52513expa 1098 . . . . . . . . . . 11 (((𝑇𝐵𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
5350, 52sylan 572 . . . . . . . . . 10 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
542, 27, 19lnof 28299 . . . . . . . . . . . . . . 15 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇𝐿) → 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊))
551, 21, 22, 54mp3an 1440 . . . . . . . . . . . . . 14 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)
5655ffvelrni 6669 . . . . . . . . . . . . 13 (𝑥 ∈ (BaseSet‘𝑈) → (𝑇𝑥) ∈ (BaseSet‘𝑊))
5755ffvelrni 6669 . . . . . . . . . . . . 13 (𝑤 ∈ (BaseSet‘𝑈) → (𝑇𝑤) ∈ (BaseSet‘𝑊))
5827, 17imsmet 28235 . . . . . . . . . . . . . . 15 (𝑊 ∈ NrmCVec → 𝐷 ∈ (Met‘(BaseSet‘𝑊)))
5921, 58ax-mp 5 . . . . . . . . . . . . . 14 𝐷 ∈ (Met‘(BaseSet‘𝑊))
60 metcl 22635 . . . . . . . . . . . . . 14 ((𝐷 ∈ (Met‘(BaseSet‘𝑊)) ∧ (𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ∈ ℝ)
6159, 60mp3an1 1427 . . . . . . . . . . . . 13 (((𝑇𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ∈ ℝ)
6256, 57, 61syl2an 586 . . . . . . . . . . . 12 ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ∈ ℝ)
6340, 62sylan 572 . . . . . . . . . . 11 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇𝑥)𝐷(𝑇𝑤)) ∈ ℝ)
64 remulcl 10412 . . . . . . . . . . . . . . 15 ((((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
6530, 42, 64syl2an 586 . . . . . . . . . . . . . 14 ((𝑇𝐵 ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈))) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
6665anassrs 460 . . . . . . . . . . . . 13 (((𝑇𝐵𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
6766adantllr 706 . . . . . . . . . . . 12 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
6867adantlrr 708 . . . . . . . . . . 11 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
69 lelttr 10523 . . . . . . . . . . 11 ((((𝑇𝑥)𝐷(𝑇𝑤)) ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((((𝑇𝑥)𝐷(𝑇𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7063, 68, 45, 69syl3anc 1351 . . . . . . . . . 10 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑇𝑥)𝐷(𝑇𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7153, 70mpand 682 . . . . . . . . 9 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7248, 71sylbird 252 . . . . . . . 8 ((((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7372ralrimiva 3126 . . . . . . 7 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
74 breq2 4927 . . . . . . . 8 (𝑧 = (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
7574rspceaimv 3537 . . . . . . 7 (((𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈ ℝ+ ∧ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7639, 73, 75syl2anc 576 . . . . . 6 (((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7776ralrimivva 3135 . . . . 5 ((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) → ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))
7877, 55jctil 512 . . . 4 ((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) → (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦)))
79 metxmet 22637 . . . . . 6 (𝐷 ∈ (Met‘(BaseSet‘𝑊)) → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
8059, 79ax-mp 5 . . . . 5 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
8111, 18metcn 22846 . . . . 5 ((𝐶 ∈ (∞Met‘(BaseSet‘𝑈)) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦))))
8210, 80, 81mp2an 679 . . . 4 (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+𝑧 ∈ ℝ+𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇𝑥)𝐷(𝑇𝑤)) < 𝑦)))
8378, 82sylibr 226 . . 3 ((𝑇𝐵𝑇 ≠ (𝑈 0op 𝑊)) → 𝑇 ∈ (𝐽 Cn 𝐾))
84 eqid 2772 . . . . . . 7 (0vec𝑊) = (0vec𝑊)
852, 84, 310ofval 28331 . . . . . 6 ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈 0op 𝑊) = ((BaseSet‘𝑈) × {(0vec𝑊)}))
861, 21, 85mp2an 679 . . . . 5 (𝑈 0op 𝑊) = ((BaseSet‘𝑈) × {(0vec𝑊)})
8718mopntopon 22742 . . . . . . 7 (𝐷 ∈ (∞Met‘(BaseSet‘𝑊)) → 𝐾 ∈ (TopOn‘(BaseSet‘𝑊)))
8880, 87ax-mp 5 . . . . . 6 𝐾 ∈ (TopOn‘(BaseSet‘𝑊))
8927, 84nvzcl 28178 . . . . . . 7 (𝑊 ∈ NrmCVec → (0vec𝑊) ∈ (BaseSet‘𝑊))
9021, 89ax-mp 5 . . . . . 6 (0vec𝑊) ∈ (BaseSet‘𝑊)
91 cnconst2 21585 . . . . . 6 ((𝐽 ∈ (TopOn‘(BaseSet‘𝑈)) ∧ 𝐾 ∈ (TopOn‘(BaseSet‘𝑊)) ∧ (0vec𝑊) ∈ (BaseSet‘𝑊)) → ((BaseSet‘𝑈) × {(0vec𝑊)}) ∈ (𝐽 Cn 𝐾))
9213, 88, 90, 91mp3an 1440 . . . . 5 ((BaseSet‘𝑈) × {(0vec𝑊)}) ∈ (𝐽 Cn 𝐾)
9386, 92eqeltri 2856 . . . 4 (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾)
9493a1i 11 . . 3 (𝑇𝐵 → (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾))
9525, 83, 94pm2.61ne 3047 . 2 (𝑇𝐵𝑇 ∈ (𝐽 Cn 𝐾))
9624, 95impbii 201 1 (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 198  wa 387   = wceq 1507  wcel 2048  wne 2961  wral 3082  wrex 3083  {csn 4435   class class class wbr 4923   × cxp 5398  wf 6178  cfv 6182  (class class class)co 6970  cr 10326  0cc0 10327   · cmul 10332   < clt 10466  cle 10467   / cdiv 11090  +crp 12197  ∞Metcxmet 20222  Metcmet 20223  MetOpencmopn 20227  TopOnctopon 21212   Cn ccn 21526   CnP ccnp 21527  NrmCVeccnv 28128  BaseSetcba 28130  0veccn0v 28132  IndMetcims 28135   LnOp clno 28284   normOpOLD cnmoo 28285   BLnOp cblo 28286   0op c0o 28287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-13 2299  ax-ext 2745  ax-rep 5043  ax-sep 5054  ax-nul 5061  ax-pow 5113  ax-pr 5180  ax-un 7273  ax-cnex 10383  ax-resscn 10384  ax-1cn 10385  ax-icn 10386  ax-addcl 10387  ax-addrcl 10388  ax-mulcl 10389  ax-mulrcl 10390  ax-mulcom 10391  ax-addass 10392  ax-mulass 10393  ax-distr 10394  ax-i2m1 10395  ax-1ne0 10396  ax-1rid 10397  ax-rnegex 10398  ax-rrecex 10399  ax-cnre 10400  ax-pre-lttri 10401  ax-pre-lttrn 10402  ax-pre-ltadd 10403  ax-pre-mulgt0 10404  ax-pre-sup 10405  ax-addf 10406  ax-mulf 10407
This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3or 1069  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-mo 2544  df-eu 2580  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-ne 2962  df-nel 3068  df-ral 3087  df-rex 3088  df-reu 3089  df-rmo 3090  df-rab 3091  df-v 3411  df-sbc 3678  df-csb 3783  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-pss 3841  df-nul 4174  df-if 4345  df-pw 4418  df-sn 4436  df-pr 4438  df-tp 4440  df-op 4442  df-uni 4707  df-iun 4788  df-br 4924  df-opab 4986  df-mpt 5003  df-tr 5025  df-id 5305  df-eprel 5310  df-po 5319  df-so 5320  df-fr 5359  df-we 5361  df-xp 5406  df-rel 5407  df-cnv 5408  df-co 5409  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413  df-pred 5980  df-ord 6026  df-on 6027  df-lim 6028  df-suc 6029  df-iota 6146  df-fun 6184  df-fn 6185  df-f 6186  df-f1 6187  df-fo 6188  df-f1o 6189  df-fv 6190  df-riota 6931  df-ov 6973  df-oprab 6974  df-mpo 6975  df-om 7391  df-1st 7494  df-2nd 7495  df-wrecs 7743  df-recs 7805  df-rdg 7843  df-er 8081  df-map 8200  df-en 8299  df-dom 8300  df-sdom 8301  df-sup 8693  df-inf 8694  df-pnf 10468  df-mnf 10469  df-xr 10470  df-ltxr 10471  df-le 10472  df-sub 10664  df-neg 10665  df-div 11091  df-nn 11432  df-2 11496  df-3 11497  df-n0 11701  df-z 11787  df-uz 12052  df-q 12156  df-rp 12198  df-xneg 12317  df-xadd 12318  df-xmul 12319  df-seq 13178  df-exp 13238  df-cj 14309  df-re 14310  df-im 14311  df-sqrt 14445  df-abs 14446  df-topgen 16563  df-psmet 20229  df-xmet 20230  df-met 20231  df-bl 20232  df-mopn 20233  df-top 21196  df-topon 21213  df-bases 21248  df-cn 21529  df-cnp 21530  df-grpo 28037  df-gid 28038  df-ginv 28039  df-gdiv 28040  df-ablo 28089  df-vc 28103  df-nv 28136  df-va 28139  df-ba 28140  df-sm 28141  df-0v 28142  df-vs 28143  df-nmcv 28144  df-ims 28145  df-lno 28288  df-nmoo 28289  df-blo 28290  df-0o 28291
This theorem is referenced by:  lnocni  28350  blocn  28351
  Copyright terms: Public domain W3C validator