Theorem blocni 8409

Description: A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97.

Hypotheses

Ref	Expression
blocni.8	|- C = (IndMet` U)
blocni.d	|- D = (IndMet` W)
blocni.j	|- J = (Open` C)
blocni.k	|- K = (Open` D)
blocni.4	|- L = (U LnOp W)
blocni.5	|- B = (U BLnOp W)
blocni.u	|- U e. NrmCVec
blocni.w	|- W e. NrmCVec
blocni.l	|- T e. L

Assertion

Ref	Expression
blocni	|- (T e. (J Cn K) <-> T e. B)

Proof of Theorem blocni

Step	Hyp	Ref	Expression
1		blocni.u	. . . . . 6 |- U e. NrmCVec
2		eqid 1473	. . . . . . 7 |- (Base` U) = (Base` U)
3		eqid 1473	. . . . . . 7 |- (0v` U) = (0v` U)
4	2, 3	nvzcl 8207	. . . . . 6 |- (U e. NrmCVec -> (0v` U) e. (Base` U))
5	1, 4	ax-mp 7	. . . . 5 |- (0v` U) e. (Base` U)
6		blocni.8	. . . . . . . 8 |- C = (IndMet` U)
7	6	imsmet 8275	. . . . . . 7 |- (U e. NrmCVec -> C e. Met)
8	1, 7	ax-mp 7	. . . . . 6 |- C e. Met
9	2, 6, 1	imsbai 8273	. . . . . . 7 |- (Base` U) = dom dom C
10		blocni.j	. . . . . . 7 |- J = (Open` C)
11	9, 10	uniopn 7813	. . . . . 6 |- (C e. Met -> U.J = (Base` U))
12	8, 11	ax-mp 7	. . . . 5 |- U.J = (Base` U)
13	5, 12	eleqtrr 1544	. . . 4 |- (0v` U) e. U.J
14	10	opntop 7822	. . . . . 6 |- (C e. Met -> J e. Top)
15	8, 14	ax-mp 7	. . . . 5 |- J e. Top
16		blocni.w	. . . . . . 7 |- W e. NrmCVec
17		blocni.d	. . . . . . . 8 |- D = (IndMet` W)
18	17	imsmet 8275	. . . . . . 7 |- (W e. NrmCVec -> D e. Met)
19	16, 18	ax-mp 7	. . . . . 6 |- D e. Met
20		blocni.k	. . . . . . 7 |- K = (Open` D)
21	20	opntop 7822	. . . . . 6 |- (D e. Met -> K e. Top)
22	19, 21	ax-mp 7	. . . . 5 |- K e. Top
23		eqid 1473	. . . . . 6 |- U.J = U.J
24		eqid 1473	. . . . . 6 |- U.K = U.K
25	23, 24	cncnpi 7723	. . . . 5 |- (((J e. Top /\ K e. Top) /\ (T e. (J Cn K) /\ (0v` U) e. U.J)) -> T e. ((J CnP K)` (0v` U)))
26	15, 22, 25	mpanl12 707	. . . 4 |- ((T e. (J Cn K) /\ (0v` U) e. U.J) -> T e. ((J CnP K)` (0v` U)))
27	13, 26	mpan2 695	. . 3 |- (T e. (J Cn K) -> T e. ((J CnP K)` (0v` U)))
28		blocni.4	. . . . 5 |- L = (U LnOp W)
29		blocni.5	. . . . 5 |- B = (U BLnOp W)
30		blocni.l	. . . . 5 |- T e. L
31	6, 17, 10, 20, 28, 29, 1, 16, 30, 2	blocnilem 8408	. . . 4 |- (((0v` U) e. (Base` U) /\ T e. ((J CnP K)` (0v` U))) -> T e. B)
32	5, 31	mpan 694	. . 3 |- (T e. ((J CnP K)` (0v` U)) -> T e. B)
33	27, 32	syl 10	. 2 |- (T e. (J Cn K) -> T e. B)
34		eleq1 1531	. . 3 |- (T = (U 0op W) -> (T e. (J Cn K) <-> (U 0op W) e. (J Cn K)))
35		breq2 2618	. . . . . . . . . . 11 |- (z = (y / ((UnormOpW)` T)) -> (0 < z <-> 0 < (y / ((UnormOpW)` T))))
36		breq2 2618	. . . . . . . . . . . . 13 |- (z = (y / ((UnormOpW)` T)) -> ((xCw) < z <-> (xCw) < (y / ((UnormOpW)` T))))
37	36	imbi1d 612	. . . . . . . . . . . 12 |- (z = (y / ((UnormOpW)` T)) -> (((xCw) < z -> ((T` x)D(T` w)) < y) <-> ((xCw) < (y / ((UnormOpW)` T)) -> ((T` x)D(T` w)) < y)))
38	37	ralbidv 1660	. . . . . . . . . . 11 |- (z = (y / ((UnormOpW)` T)) -> (A.w e. (Base` U)((xCw) < z -> ((T` x)D(T` w)) < y) <-> A.w e. (Base` U)((xCw) < (y / ((UnormOpW)` T)) -> ((T` x)D(T` w)) < y)))
39	35, 38	anbi12d 627	. . . . . . . . . 10 |- (z = (y / ((UnormOpW)` T)) -> ((0 < z /\ A.w e. (Base` U)((xCw) < z -> ((T` x)D(T` w)) < y)) <-> (0 < (y / ((UnormOpW)` T)) /\ A.w e. (Base` U)((xCw) < (y / ((UnormOpW)` T)) -> ((T` x)D(T` w)) < y))))
40	39	rcla4ev 1873	. . . . . . . . 9 |- (((y / ((UnormOpW)` T)) e. RR /\ (0 < (y / ((UnormOpW)` T)) /\ A.w e. (Base` U)((xCw) < (y / ((UnormOpW)` T)) -> ((T` x)D(T` w)) < y))) -> E.z e. RR (0 < z /\ A.w e. (Base` U)((xCw) < z -> ((T` x)D(T` w)) < y)))
41		redivclt 5764	. . . . . . . . . . 11 |- ((y e. RR /\ ((UnormOpW)` T) e. RR /\ ((UnormOpW)` T) =/= 0) -> (y / ((UnormOpW)` T)) e. RR)
42		pm3.27 323	. . . . . . . . . . 11 |- (((T e. B /\ T =/= (U 0op W)) /\ y e. RR) -> y e. RR)
43		eqid 1473	. . . . . . . . . . . . . 14 |- (Base` W) = (Base` W)
44		eqid 1473	. . . . . . . . . . . . . 14 |- (UnormOpW) = (UnormOpW)
45	2, 43, 44, 29	nmblore 8391	. . . . . . . . . . . . 13 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> ((UnormOpW)` T) e. RR)
46	1, 16, 45	mp3an12 904	. . . . . . . . . . . 12 |- (T e. B -> ((UnormOpW)` T) e. RR)
47	46	ad2antrr 404	. . . . . . . . . . 11 |- (((T e. B /\ T =/= (U 0op W)) /\ y e. RR) -> ((UnormOpW)` T) e. RR)
48		eqid 1473	. . . . . . . . . . . . . . . 16 |- (U 0op W) = (U 0op W)
49	44, 48, 28, 1, 16	nmlno0i 8399	. . . . . . . . . . . . . . 15 |- (T e. L -> (((UnormOpW)` T) = 0 <-> T = (U 0op W)))
50	30, 49	ax-mp 7	. . . . . . . . . . . . . 14 |- (((UnormOpW)` T) = 0 <-> T = (U 0op W))
51	50	biimp 151	. . . . . . . . . . . . 13 |- (((UnormOpW)` T) = 0 -> T = (U 0op W))
52	51	necon3i 1602	. . . . . . . . . . . 12 |- (T =/= (U 0op W) -> ((UnormOpW)` T) =/= 0)
53	52	ad2antlr 405	. . . . . . . . . . 11 |- (((T e. B /\ T =/= (U 0op W)) /\ y e. RR) -> ((UnormOpW)` T) =/= 0)
54	41, 42, 47, 53	syl3anc 857	. . . . . . . . . 10 |- (((T e. B /\ T =/= (U 0op W)) /\ y e. RR) -> (y / ((UnormOpW)` T)) e. RR)
55	54	ad2ant2r 409	. . . . . . . . 9 |- ((((T e. B /\ T =/= (U 0op W)) /\ x e. (Base` U)) /\ (y e. RR /\ 0 < y)) -> (y / ((UnormOpW)` T)) e. RR)
56		divgt0t 5817	. . . . . . . . . . . 12 |- (((y e. RR /\ 0 < y) /\ (((UnormOpW)` T) e. RR /\ 0 < ((UnormOpW)` T))) -> 0 < (y / ((UnormOpW)` T)))
57		pm3.27 323	. . . . . . . . . . . 12 |- (((T e. B /\ T =/= (U 0op W)) /\ (y e. RR /\ 0 < y)) -> (y e. RR /\ 0 < y))
58	44, 48, 28	nmlnogt0 8402	. . . . . . . . . . . . . . . 16 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. L) -> (T =/= (U 0op W) <-> 0 < ((UnormOpW)` T)))
59	1, 16, 30, 58	mp3an 914	. . . . . . . . . . . . . . 15 |- (T =/= (U 0op W) <-> 0 < ((UnormOpW)` T))
60	59	biimp 151	. . . . . . . . . . . . . 14 |- (T =/= (U 0op W) -> 0 < ((UnormOpW)` T))
61	46, 60	anim12i 333	. . . . . . . . . . . . 13 |- ((T e. B /\ T =/= (U 0op W)) -> (((UnormOpW)` T) e. RR /\ 0 < ((UnormOpW)` T)))
62	61	adantr 389	. . . . . . . . . . . 12 |- (((T e. B /\ T =/= (U 0op W)) /\ (y e. RR /\ 0 < y)) -> (((UnormOpW)` T) e. RR /\ 0 < ((UnormOpW)` T)))
63	56, 57, 62	sylanc 471	. . . . . . . . . . 11 |- (((T e. B /\ T =/= (U 0op W)) /\ (y e. RR /\ 0 < y)) -> 0 < (y / ((UnormOpW)` T)))
64	63	adantlr 393	. . . . . . . . . 10 |- ((((T e. B /\ T =/= (U 0op W)) /\ x e. (Base` U)) /\ (y e. RR /\ 0 < y)) -> 0 < (y / ((UnormOpW)` T)))
65		ltmuldiv2t 5826	. . . . . . . . . . . . . . 15 |- (((((UnormOpW)` T) e. RR /\ (xCw) e. RR /\ y e. RR) /\ 0 < ((UnormOpW)` T)) -> ((((UnormOpW)` T) x. (xCw)) < y <-> (xCw) < (y / ((UnormOpW)` T))))
66	46	ad2antrr 404	. . . . . . . . . . . . . . . . 17 |- (((T e. B /\ T =/= (U 0op W)) /\ x e. (Base` U)) -> ((UnormOpW)` T) e. RR)
67	66	ad2antrr 404	. . . . . . . . . . . . . . . 16 |- (((((T e. B /\ T =/= (U 0op W)) /\ x e. (Base` U)) /\ (y e. RR /\ 0 < y)) /\ w e. (Base` U)) -> ((UnormOpW)` T) e. RR)
68	9	metcl 7761	. . . . . . . . . . . . . . . . . . 19 |- ((C e. Met /\ x e. (Base` U) /\ w e. (Base` U)) -> (xCw) e. RR)
69	8, 68	mp3an1 901	. . . . . . . . . . . . . . . . . 18 |- ((x e. (Base` U) /\ w e. (Base` U)) -> (xCw) e. RR)
70	69	adantlr 393	. . . . . . . . . . . . . . . . 17 |- (((x e. (Base` U) /\ (y e. RR /\ 0