Theorem nmblolbii 8390

Description: A lower bound for the norm of a bounded linear operator.

Hypotheses

Ref	Expression
nmblolbi.1	|- X = (Base` U)
nmblolbi.4	|- L = (norm` U)
nmblolbi.5	|- M = (norm` W)
nmblolbi.6	|- N = (UnormOpW)
nmblolbi.7	|- B = (U BLnOp W)
nmblolbi.u	|- U e. NrmCVec
nmblolbi.w	|- W e. NrmCVec
nmblolbii.b	|- T e. B

Assertion

Ref	Expression
nmblolbii	|- (A e. X -> (M` (T` A)) <_ ((N` T) x. (L` A)))

Proof of Theorem nmblolbii

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . 4 |- (A = (0v` U) -> (T` A) = (T` (0v` U)))
2	1	fveq2d 3713	. . 3 |- (A = (0v` U) -> (M` (T` A)) = (M` (T` (0v` U))))
3		fveq2 3709	. . . 4 |- (A = (0v` U) -> (L` A) = (L` (0v` U)))
4	3	opreq2d 3961	. . 3 |- (A = (0v` U) -> ((N` T) x. (L` A)) = ((N` T) x. (L` (0v` U))))
5	2, 4	breq12d 2621	. 2 |- (A = (0v` U) -> ((M` (T` A)) <_ ((N` T) x. (L` A)) <-> (M` (T` (0v` U))) <_ ((N` T) x. (L` (0v` U)))))
6		nmblolbi.w	. . . . . . 7 |- W e. NrmCVec
7		eqid 1468	. . . . . . . 8 |- (Base` W) = (Base` W)
8		eqid 1468	. . . . . . . 8 |- (.s` W) = (.s` W)
9		nmblolbi.5	. . . . . . . 8 |- M = (norm` W)
10	7, 8, 9	nvsge0 8230	. . . . . . 7 |- ((W e. NrmCVec /\ ((1 / (L` A)) e. RR /\ 0 <_ (1 / (L` A))) /\ (T` A) e. (Base` W)) -> (M` ((1 / (L` A))(.s` W)(T` A))) = ((1 / (L` A)) x. (M` (T` A))))
11	6, 10	mp3an1 900	. . . . . 6 |- ((((1 / (L` A)) e. RR /\ 0 <_ (1 / (L` A))) /\ (T` A) e. (Base` W)) -> (M` ((1 / (L` A))(.s` W)(T` A))) = ((1 / (L` A)) x. (M` (T` A))))
12		rerecclt 5759	. . . . . . . 8 |- (((L` A) e. RR /\ (L` A) =/= 0) -> (1 / (L` A)) e. RR)
13		nmblolbi.u	. . . . . . . . . 10 |- U e. NrmCVec
14		nmblolbi.1	. . . . . . . . . . 11 |- X = (Base` U)
15		nmblolbi.4	. . . . . . . . . . 11 |- L = (norm` U)
16	14, 15	nvcl 8227	. . . . . . . . . 10 |- ((U e. NrmCVec /\ A e. X) -> (L` A) e. RR)
17	13, 16	mpan 693	. . . . . . . . 9 |- (A e. X -> (L` A) e. RR)
18	17	adantr 389	. . . . . . . 8 |- ((A e. X /\ A =/= (0v` U)) -> (L` A) e. RR)
19		eqid 1468	. . . . . . . . . . . 12 |- (0v` U) = (0v` U)
20	14, 19, 15	nvz 8236	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> ((L` A) = 0 <-> A = (0v` U)))
21	13, 20	mpan 693	. . . . . . . . . 10 |- (A e. X -> ((L` A) = 0 <-> A = (0v` U)))
22	21	necon3bid 1593	. . . . . . . . 9 |- (A e. X -> ((L` A) =/= 0 <-> A =/= (0v` U)))
23	22	biimpar 417	. . . . . . . 8 |- ((A e. X /\ A =/= (0v` U)) -> (L` A) =/= 0)
24	12, 18, 23	sylanc 471	. . . . . . 7 |- ((A e. X /\ A =/= (0v` U)) -> (1 / (L` A)) e. RR)
25		recgt0t 5815	. . . . . . . . 9 |- (((L` A) e. RR /\ 0 < (L` A)) -> 0 < (1 / (L` A)))
26	14, 19, 15	nvgt0 8242	. . . . . . . . . . 11 |- ((U e. NrmCVec /\ A e. X) -> (A =/= (0v` U) <-> 0 < (L` A)))
27	13, 26	mpan 693	. . . . . . . . . 10 |- (A e. X -> (A =/= (0v` U) <-> 0 < (L` A)))
28	27	biimpa 416	. . . . . . . . 9 |- ((A e. X /\ A =/= (0v` U)) -> 0 < (L` A))
29	25, 18, 28	sylanc 471	. . . . . . . 8 |- ((A e. X /\ A =/= (0v` U)) -> 0 < (1 / (L` A)))
30		0re 5412	. . . . . . . . . 10 |- 0 e. RR
31		ltlet 5493	. . . . . . . . . 10 |- ((0 e. RR /\ (1 / (L` A)) e. RR) -> (0 < (1 / (L` A)) -> 0 <_ (1 / (L` A))))
32	30, 31	mpan 693	. . . . . . . . 9 |- ((1 / (L` A)) e. RR -> (0 < (1 / (L` A)) -> 0 <_ (1 / (L` A))))
33	24, 32	syl 10	. . . . . . . 8 |- ((A e. X /\ A =/= (0v` U)) -> (0 < (1 / (L` A)) -> 0 <_ (1 / (L` A))))
34	29, 33	mpd 26	. . . . . . 7 |- ((A e. X /\ A =/= (0v` U)) -> 0 <_ (1 / (L` A)))
35	24, 34	jca 288	. . . . . 6 |- ((A e. X /\ A =/= (0v` U)) -> ((1 / (L` A)) e. RR /\ 0 <_ (1 / (L` A))))
36		nmblolbii.b	. . . . . . . . 9 |- T e. B
37		nmblolbi.7	. . . . . . . . . 10 |- B = (U BLnOp W)
38	14, 7, 37	blof 8377	. . . . . . . . 9 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> T:X-->(Base` W))
39	13, 6, 36, 38	mp3an 913	. . . . . . . 8 |- T:X-->(Base` W)
40	39	ffvelrni 3800	. . . . . . 7 |- (A e. X -> (T` A) e. (Base` W))
41	40	adantr 389	. . . . . 6 |- ((A e. X /\ A =/= (0v` U)) -> (T` A) e. (Base` W))
42	11, 35, 41	sylanc 471	. . . . 5 |- ((A e. X /\ A =/= (0v` U)) -> (M` ((1 / (L` A))(.s` W)(T` A))) = ((1 / (L` A)) x. (M` (T` A))))
43		eqid 1468	. . . . . . . . . . 11 |- (U LnOp W) = (U LnOp W)
44	43, 37	bloln 8376	. . . . . . . . . 10 |- ((U e. NrmCVec /\ W e. NrmCVec /\ T e. B) -> T e. (U LnOp W))
45	13, 6, 36, 44	mp3an 913	. . . . . . . . 9 |- T e. (U LnOp W)
46	13, 6, 45	3pm3.2i 816	. . . . . . . 8 |- (U e. NrmCVec /\ W e. NrmCVec /\ T e. (U LnOp W))
47		eqid 1468	. . . . . . . . 9 |- (.s` U) = (.s` U)
48	14, 47, 8, 43	lnomul 8354	. . . . . . . 8 |- (((U e. NrmCVec /\ W e. NrmCVec /\ T e. (U LnOp W)) /\ ((1 / (L` A)) e. CC /\ A e. X)) -> (T` ((1 / (L` A))(.s` U)A)) = ((1 / (L` A))(.s` W)(T` A)))
49	46, 48	mpan 693	. . . . . . 7 |- (((1 / (L` A)) e. CC /\ A e. X) -> (T` ((1 / (L` A))(.s` U)A)) = ((1 / (L` A))(.s` W)(T` A)))
50	24	recnd 5287	. . . . . . 7 |- ((A e. X /\ A =/= (0v` U)) -> (1 / (L` A)) e. CC)
51		pm3.26 319	. . . . . . 7 |- ((A e. X /\ A =/= (0v` U)) -> A e. X)
52	49, 50, 51	sylanc 471	. . . . . 6 |- ((A e. X /\ A =/= (0v` U)) -> (T` ((1 / (L` A))(.s` U)A)) = ((1 / (L` A))(.s` W)(T` A)))
53	52	fveq2d 3713	. . . . 5 |- ((A e. X /\ A =/= (0v` U)) -> (M` (T` ((1 / (L` A))(.s` U)A))) = (M` ((1 / (L` A))(.s` W)(T` A))))
54		divrec2t 5703	. . . . . 6 |- (((M` (T` A)) e. CC /\ (L` A) e. CC /\ (L` A) =/= 0) -> ((M` (T` A)) / (L` A)) = ((1 / (L` A)) x. (M` (T` A))))
55	7, 9	nvcl 8227	. . . . . . . . . 10 |- ((W e. NrmCVec /\ (T` A) e. (Base` W)) -> (M` (T` A)) e. RR)
56	6, 55	mpan 693	. . . . . . . . 9 |- ((T` A) e. (Base` W) -> (M` (T` A)) e. RR)
57	40, 56	syl 10	. . . . . . . 8 |- (A e. X -> (M` (T` A)) e. RR)
58	57	adantr 389	. . . . . . 7 |- ((A e. X /\ A =/= (0v` U)) -> (M` (T` A)) e. RR)
59	58	recnd 5287	. . . . . 6 |- ((A e. X /\ A =/= (0v` U)) -> (M` (T` A)) e. CC)
60	18	recnd 5287	. . . . . 6 |- ((A e. X /\ A =/= (0v` U)) -> (L` A) e. CC)
61	54, 59, 60, 23	syl3anc 856	. . . . 5 |- ((A e. X /\ A =/= (0v` U)) -> ((M` (T` A)) / (L` A)) = ((1 / (L` A)) x. (M` (T` A))))
62	42, 53, 61	3eqtr4rd 1510	. . . 4 |- ((A e. X /\ A =/= (0v` U)) -> ((M` (T` A)) / (L` A)) = (M` (T` ((1 / (L` A))(.s` U)A))))
63	13, 6, 39	3pm3.2i 816	. . . . . 6 |- (U e. NrmCVec /\ W e. NrmCVec /\ T:X-->(Base` W))
64		nmblolbi.6	. . . . . . 7 |- N = (UnormOpW)
65	14, 7, 15, 9, 64	nmolb 8366	. . . . . 6 |- (((U e. NrmCVec /\ W e. NrmCVec /\ T:X-->(Base` W)) /\ ((