Theorem blocni 30829

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.

Step	Hyp	Ref	Expression
1		blocni.u	. . . 4 ⊢ 𝑈 ∈ NrmCVec
2		eqid 2734	. . . . 5 ⊢ (BaseSet‘𝑈) = (BaseSet‘𝑈)
3		eqid 2734	. . . . 5 ⊢ (0vec‘𝑈) = (0vec‘𝑈)
4	2, 3	nvzcl 30658	. . . 4 ⊢ (𝑈 ∈ NrmCVec → (0vec‘𝑈) ∈ (BaseSet‘𝑈))
5	1, 4	ax-mp 5	. . 3 ⊢ (0vec‘𝑈) ∈ (BaseSet‘𝑈)
6		blocni.8	. . . . . . . . . 10 ⊢ 𝐶 = (IndMet‘𝑈)
7	2, 6	imsmet 30715	. . . . . . . . 9 ⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈ (Met‘(BaseSet‘𝑈)))
8	1, 7	ax-mp 5	. . . . . . . 8 ⊢ 𝐶 ∈ (Met‘(BaseSet‘𝑈))
9		metxmet 24276	. . . . . . . 8 ⊢ (𝐶 ∈ (Met‘(BaseSet‘𝑈)) → 𝐶 ∈ (∞Met‘(BaseSet‘𝑈)))
10	8, 9	ax-mp 5	. . . . . . 7 ⊢ 𝐶 ∈ (∞Met‘(BaseSet‘𝑈))
11		blocni.j	. . . . . . . 8 ⊢ 𝐽 = (MetOpen‘𝐶)
12	11	mopntopon 24381	. . . . . . 7 ⊢ (𝐶 ∈ (∞Met‘(BaseSet‘𝑈)) → 𝐽 ∈ (TopOn‘(BaseSet‘𝑈)))
13	10, 12	ax-mp 5	. . . . . 6 ⊢ 𝐽 ∈ (TopOn‘(BaseSet‘𝑈))
14	13	toponunii 22858	. . . . 5 ⊢ (BaseSet‘𝑈) = ∪ 𝐽
15	14	cncnpi 23220	. . . 4 ⊢ ((𝑇 ∈ (𝐽 Cn 𝐾) ∧ (0vec‘𝑈) ∈ (BaseSet‘𝑈)) → 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec‘𝑈)))
16	5, 15	mpan2 691	. . 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 ⊢ 𝑇 ∈ 𝐿
23	6, 17, 11, 18, 19, 20, 1, 21, 22, 2	blocnilem 30828	. . 3 ⊢ (((0vec‘𝑈) ∈ (BaseSet‘𝑈) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec‘𝑈))) → 𝑇 ∈ 𝐵)
24	5, 16, 23	sylancr 587	. 2 ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) → 𝑇 ∈ 𝐵)
25		eleq1 2822	. . 3 ⊢ (𝑇 = (𝑈 0op 𝑊) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾)))
26		simprr 772	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈ ℝ+)
27		eqid 2734	. . . . . . . . . . . . 13 ⊢ (BaseSet‘𝑊) = (BaseSet‘𝑊)
28		eqid 2734	. . . . . . . . . . . . 13 ⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊)
29	2, 27, 28, 20	nmblore 30810	. . . . . . . . . . . 12 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ)
30	1, 21, 29	mp3an12 1453	. . . . . . . . . . 11 ⊢ (𝑇 ∈ 𝐵 → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ)
31		eqid 2734	. . . . . . . . . . . . . 14 ⊢ (𝑈 0op 𝑊) = (𝑈 0op 𝑊)
32	28, 31, 19	nmlnogt0 30821	. . . . . . . . . . . . 13 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
33	1, 21, 22, 32	mp3an 1463	. . . . . . . . . . . 12 ⊢ (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))
34	33	biimpi 216	. . . . . . . . . . 11 ⊢ (𝑇 ≠ (𝑈 0op 𝑊) → 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))
35	30, 34	anim12i 613	. . . . . . . . . 10 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
36		elrp 12905	. . . . . . . . . 10 ⊢ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+ ↔ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
37	35, 36	sylibr 234	. . . . . . . . 9 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+)
38	37	adantr 480	. . . . . . . 8 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+)
39	26, 38	rpdivcld 12964	. . . . . . 7 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈ ℝ+)
40		simprl 770	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ (BaseSet‘𝑈))
41		metcl 24274	. . . . . . . . . . . 12 ⊢ ((𝐶 ∈ (Met‘(BaseSet‘𝑈)) ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
42	8, 41	mp3an1 1450	. . . . . . . . . . 11 ⊢ ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
43	40, 42	sylan 580	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ)
44		simplrr 777	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ+)
45	44	rpred 12947	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ)
46	35	ad2antrr 726	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)))
47		ltmuldiv2 12014	. . . . . . . . . 10 ⊢ (((𝑥𝐶𝑤) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
48	43, 45, 46, 47	syl3anc 1373	. . . . . . . . 9 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
49		id 22	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) → (𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)))
50	49	ad2ant2r 747	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)))
51	2, 27, 6, 17, 28, 20, 1, 21	blometi 30827	. . . . . . . . . . . 12 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
52	51	3expa 1118	. . . . . . . . . . 11 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
53	50, 52	sylan 580	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)))
54	2, 27, 19	lnof 30779	. . . . . . . . . . . . . . 15 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊))
55	1, 21, 22, 54	mp3an 1463	. . . . . . . . . . . . . 14 ⊢ 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)
56	55	ffvelcdmi 7026	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ (BaseSet‘𝑈) → (𝑇‘𝑥) ∈ (BaseSet‘𝑊))
57	55	ffvelcdmi 7026	. . . . . . . . . . . . 13 ⊢ (𝑤 ∈ (BaseSet‘𝑈) → (𝑇‘𝑤) ∈ (BaseSet‘𝑊))
58	27, 17	imsmet 30715	. . . . . . . . . . . . . . 15 ⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈ (Met‘(BaseSet‘𝑊)))
59	21, 58	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ 𝐷 ∈ (Met‘(BaseSet‘𝑊))
60		metcl 24274	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ (Met‘(BaseSet‘𝑊)) ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ)
61	59, 60	mp3an1 1450	. . . . . . . . . . . . 13 ⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ)
62	56, 57, 61	syl2an 596	. . . . . . . . . . . 12 ⊢ ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ)
63	40, 62	sylan 580	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ)
64		remulcl 11109	. . . . . . . . . . . . . . 15 ⊢ ((((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
65	30, 42, 64	syl2an 596	. . . . . . . . . . . . . 14 ⊢ ((𝑇 ∈ 𝐵 ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈))) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
66	65	anassrs 467	. . . . . . . . . . . . 13 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
67	66	adantllr 719	. . . . . . . . . . . 12 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
68	67	adantlrr 721	. . . . . . . . . . 11 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ)
69		lelttr 11221	. . . . . . . . . . 11 ⊢ ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
70	63, 68, 45, 69	syl3anc 1373	. . . . . . . . . 10 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
71	53, 70	mpand 695	. . . . . . . . 9 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
72	48, 71	sylbird 260	. . . . . . . 8 ⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
73	72	ralrimiva 3126	. . . . . . 7 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
74		breq2 5100	. . . . . . . 8 ⊢ (𝑧 = (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇))))
75	74	rspceaimv 3580	. . . . . . 7 ⊢ (((𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈ ℝ+ ∧ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
76	39, 73, 75	syl2anc 584	. . . . . 6 ⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
77	76	ralrimivva 3177	. . . . 5 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))
78	77, 55	jctil 519	. . . 4 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)))
79		metxmet 24276	. . . . . 6 ⊢ (𝐷 ∈ (Met‘(BaseSet‘𝑊)) → 𝐷 ∈ (∞Met‘(BaseSet‘𝑊)))
80	59, 79	ax-mp 5	. . . . 5 ⊢ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))
81	11, 18	metcn 24485	. . . . 5 ⊢ ((𝐶 ∈ (∞Met‘(BaseSet‘𝑈)) ∧ 𝐷 ∈ (∞Met‘(BaseSet‘𝑊))) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))))
82	10, 80, 81	mp2an 692	. . . 4 ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)))
83	78, 82	sylibr 234	. . 3 ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → 𝑇 ∈ (𝐽 Cn 𝐾))
84		eqid 2734	. . . . . . 7 ⊢ (0vec‘𝑊) = (0vec‘𝑊)
85	2, 84, 31	0ofval 30811	. . . . . 6 ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈 0op 𝑊) = ((BaseSet‘𝑈) × {(0vec‘𝑊)}))
86	1, 21, 85	mp2an 692	. . . . 5 ⊢ (𝑈 0op 𝑊) = ((BaseSet‘𝑈) × {(0vec‘𝑊)})
87	18	mopntopon 24381	. . . . . . 7 ⊢ (𝐷 ∈ (∞Met‘(BaseSet‘𝑊)) → 𝐾 ∈ (TopOn‘(BaseSet‘𝑊)))
88	80, 87	ax-mp 5	. . . . . 6 ⊢ 𝐾 ∈ (TopOn‘(BaseSet‘𝑊))
89	27, 84	nvzcl 30658	. . . . . . 7 ⊢ (𝑊 ∈ NrmCVec → (0vec‘𝑊) ∈ (BaseSet‘𝑊))
90	21, 89	ax-mp 5	. . . . . 6 ⊢ (0vec‘𝑊) ∈ (BaseSet‘𝑊)
91		cnconst2 23225	. . . . . 6 ⊢ ((𝐽 ∈ (TopOn‘(BaseSet‘𝑈)) ∧ 𝐾 ∈ (TopOn‘(BaseSet‘𝑊)) ∧ (0vec‘𝑊) ∈ (BaseSet‘𝑊)) → ((BaseSet‘𝑈) × {(0vec‘𝑊)}) ∈ (𝐽 Cn 𝐾))
92	13, 88, 90, 91	mp3an 1463	. . . . 5 ⊢ ((BaseSet‘𝑈) × {(0vec‘𝑊)}) ∈ (𝐽 Cn 𝐾)
93	86, 92	eqeltri 2830	. . . 4 ⊢ (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾)
94	93	a1i 11	. . 3 ⊢ (𝑇 ∈ 𝐵 → (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾))
95	25, 83, 94	pm2.61ne 3015	. 2 ⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ (𝐽 Cn 𝐾))
96	24, 95	impbii 209	1 ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1541   ∈ wcel 2113   ≠ wne 2930  ∀wral 3049  ∃wrex 3058  {csn 4578   class class class wbr 5096   × cxp 5620  ⟶wf 6486  ‘cfv 6490  (class class class)co 7356  ℝcr 11023  0cc0 11024   · cmul 11029   < clt 11164   ≤ cle 11165   / cdiv 11792  ℝ⁺crp 12903  ∞Metcxmet 21292  Metcmet 21293  MetOpencmopn 21297  TopOnctopon 22852   Cn ccn 23166   CnP ccnp 23167  NrmCVeccnv 30608  BaseSetcba 30610  0_veccn0v 30612  IndMetcims 30615   LnOp clno 30764   normOp_OLD cnmoo 30765   BLnOp cblo 30766   0_op c0o 30767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2706  ax-rep 5222  ax-sep 5239  ax-nul 5249  ax-pow 5308  ax-pr 5375  ax-un 7678  ax-cnex 11080  ax-resscn 11081  ax-1cn 11082  ax-icn 11083  ax-addcl 11084  ax-addrcl 11085  ax-mulcl 11086  ax-mulrcl 11087  ax-mulcom 11088  ax-addass 11089  ax-mulass 11090  ax-distr 11091  ax-i2m1 11092  ax-1ne0 11093  ax-1rid 11094  ax-rnegex 11095  ax-rrecex 11096  ax-cnre 11097  ax-pre-lttri 11098  ax-pre-lttrn 11099  ax-pre-ltadd 11100  ax-pre-mulgt0 11101  ax-pre-sup 11102  ax-addf 11103  ax-mulf 11104

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2567  df-clab 2713  df-cleq 2726  df-clel 2809  df-nfc 2883  df-ne 2931  df-nel 3035  df-ral 3050  df-rex 3059  df-rmo 3348  df-reu 3349  df-rab 3398  df-v 3440  df-sbc 3739  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4284  df-if 4478  df-pw 4554  df-sn 4579  df-pr 4581  df-op 4585  df-uni 4862  df-iun 4946  df-br 5097  df-opab 5159  df-mpt 5178  df-tr 5204  df-id 5517  df-eprel 5522  df-po 5530  df-so 5531  df-fr 5575  df-we 5577  df-xp 5628  df-rel 5629  df-cnv 5630  df-co 5631  df-dm 5632  df-rn 5633  df-res 5634  df-ima 5635  df-pred 6257  df-ord 6318  df-on 6319  df-lim 6320  df-suc 6321  df-iota 6446  df-fun 6492  df-fn 6493  df-f 6494  df-f1 6495  df-fo 6496  df-f1o 6497  df-fv 6498  df-riota 7313  df-ov 7359  df-oprab 7360  df-mpo 7361  df-om 7807  df-1st 7931  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-er 8633  df-map 8763  df-en 8882  df-dom 8883  df-sdom 8884  df-sup 9343  df-inf 9344  df-pnf 11166  df-mnf 11167  df-xr 11168  df-ltxr 11169  df-le 11170  df-sub 11364  df-neg 11365  df-div 11793  df-nn 12144  df-2 12206  df-3 12207  df-n0 12400  df-z 12487  df-uz 12750  df-q 12860  df-rp 12904  df-xneg 13024  df-xadd 13025  df-xmul 13026  df-seq 13923  df-exp 13983  df-cj 15020  df-re 15021  df-im 15022  df-sqrt 15156  df-abs 15157  df-topgen 17361  df-psmet 21299  df-xmet 21300  df-met 21301  df-bl 21302  df-mopn 21303  df-top 22836  df-topon 22853  df-bases 22888  df-cn 23169  df-cnp 23170  df-grpo 30517  df-gid 30518  df-ginv 30519  df-gdiv 30520  df-ablo 30569  df-vc 30583  df-nv 30616  df-va 30619  df-ba 30620  df-sm 30621  df-0v 30622  df-vs 30623  df-nmcv 30624  df-ims 30625  df-lno 30768  df-nmoo 30769  df-blo 30770  df-0o 30771

This theorem is referenced by:  lnocni  30830  blocn  30831