Theorem nmcoplb 9873

Description: A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of [Beran] p. 99.

Hypotheses

Ref	Expression
nmcopex.1	|- T e. LinOp
nmcopex.2	|- T e. ConOp

Assertion

Ref	Expression
nmcoplb	|- (A e. H~ -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))

Proof of Theorem nmcoplb

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . . . . 7 |- (A = 0h -> (T` A) = (T` 0h))
2		nmcopex.1	. . . . . . . 8 |- T e. LinOp
3	2	lnop0 9810	. . . . . . 7 |- (T` 0h) = 0h
4	1, 3	syl6eq 1515	. . . . . 6 |- (A = 0h -> (T` A) = 0h)
5	4	fveq2d 3713	. . . . 5 |- (A = 0h -> (normh` (T` A)) = (normh` 0h))
6		norm0 8916	. . . . 5 |- (normh` 0h) = 0
7	5, 6	syl6eq 1515	. . . 4 |- (A = 0h -> (normh` (T` A)) = 0)
8		fveq2 3709	. . . . . . . 8 |- (A = 0h -> (normh` A) = (normh` 0h))
9	8, 6	syl6eq 1515	. . . . . . 7 |- (A = 0h -> (normh` A) = 0)
10	9	opreq2d 3961	. . . . . 6 |- (A = 0h -> ((normop` T) x. (normh` A)) = ((normop` T) x. 0))
11		nmcopex.2	. . . . . . . . 9 |- T e. ConOp
12	2, 11	nmcopex 9872	. . . . . . . 8 |- (normop` T) e. RR
13	12	recn 5286	. . . . . . 7 |- (normop` T) e. CC
14	13	mul01 5403	. . . . . 6 |- ((normop` T) x. 0) = 0
15	10, 14	syl6req 1516	. . . . 5 |- (A = 0h -> 0 = ((normop` T) x. (normh` A)))
16		0re 5412	. . . . . 6 |- 0 e. RR
17	16	leid 5584	. . . . 5 |- 0 <_ 0
18	15, 17	syl5breq 2640	. . . 4 |- (A = 0h -> 0 <_ ((normop` T) x. (normh` A)))
19	7, 18	eqbrtrd 2625	. . 3 |- (A = 0h -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
20	19	adantl 388	. 2 |- ((A e. H~ /\ A = 0h) -> (normh` (T` A)) <_ ((normop` T) x. (normh` A)))
21		divrec2t 5703	. . . . . 6 |- (((normh` (T` A)) e. CC /\ (normh` A) e. CC /\ (normh` A) =/= 0) -> ((normh` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (normh` (T` A))))
22	2	lnopf 9809	. . . . . . . . . 10 |- T:H~-->H~
23	22	ffvelrni 3800	. . . . . . . . 9 |- (A e. H~ -> (T` A) e. H~)
24		normclt 8912	. . . . . . . . 9 |- ((T` A) e. H~ -> (normh` (T` A)) e. RR)
25	23, 24	syl 10	. . . . . . . 8 |- (A e. H~ -> (normh` (T` A)) e. RR)
26	25	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (normh` (T` A)) e. RR)
27	26	recnd 5287	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` (T` A)) e. CC)
28		normclt 8912	. . . . . . . 8 |- (A e. H~ -> (normh` A) e. RR)
29	28	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) e. RR)
30	29	recnd 5287	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) e. CC)
31		norm-it 8917	. . . . . . . . 9 |- (A e. H~ -> ((normh` A) = 0 <-> A = 0h))
32	31	negbid 609	. . . . . . . 8 |- (A e. H~ -> (-. (normh` A) = 0 <-> -. A = 0h))
33	32	biimpar 417	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> -. (normh` A) = 0)
34		df-ne 1579	. . . . . . 7 |- ((normh` A) =/= 0 <-> -. (normh` A) = 0)
35	33, 34	sylibr 200	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) =/= 0)
36	21, 27, 30, 35	syl3anc 856	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((normh` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (normh` (T` A))))
37	2	lnopmul 9812	. . . . . . . 8 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) .h (T` A)))
38		rerecclt 5759	. . . . . . . . . 10 |- (((normh` A) e. RR /\ (normh` A) =/= 0) -> (1 / (normh` A)) e. RR)
39	38, 29, 35	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ -. A = 0h) -> (1 / (normh` A)) e. RR)
40	39	recnd 5287	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> (1 / (normh` A)) e. CC)
41		pm3.26 319	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> A e. H~)
42	37, 40, 41	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) .h (T` A)))
43	42	fveq2d 3713	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` (T` ((1 / (normh` A)) .h A))) = (normh` ((1 / (normh` A)) .h (T` A))))
44		norm-iiit 8928	. . . . . . 7 |- (((1 / (normh` A)) e. CC /\ (T` A) e. H~) -> (normh` ((1 / (normh` A)) .h (T` A))) = ((abs` (1 / (normh` A))) x. (normh` (T` A))))
45	23	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (T` A) e. H~)
46	44, 40, 45	sylanc 471	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` ((1 / (normh` A)) .h (T` A))) = ((abs` (1 / (normh` A))) x. (normh` (T` A))))
47		absidt 6797	. . . . . . . 8 |- (((1 / (normh` A)) e. RR /\ 0 <_ (1 / (normh` A))) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
48		ltlet 5493	. . . . . . . . . 10 |- ((0 e. RR /\ (1 / (normh` A)) e. RR) -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
49	16, 48	mpan 693	. . . . . . . . 9 |- ((1 / (normh` A)) e. RR -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
50		recgt0t 5815	. . . . . . . . . 10 |- (((normh` A) e. RR /\ 0 < (normh` A)) -> 0 < (1 / (normh` A)))
51		normgt0tOLD 8914	. . . . . . . . . . 11 |- (A e. H~ -> (-. A = 0h <-> 0 < (normh` A)))
52	51	biimpa 416	. . . . . . . . . 10 |- ((A e. H~ /\ -. A = 0h) -> 0 < (normh` A))
53	50, 29, 52	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ -. A = 0h) -> 0 < (1 / (normh` A)))
54	49, 39, 53	sylc 68	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> 0 <_ (1 / (normh` A)))
55	47, 39, 54	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
56	55	opreq1d 3960	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> ((abs` (1 / (normh` A))) x. (normh` (T` A))) = ((1 / (normh` A)) x. (normh` (T` A))))
57	43, 46, 56	3eqtrrd 1504	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((1 / (normh` A)) x. (normh` (T` A))) = (normh` (T` ((1 / (normh` A)) .h A))))
58	36, 57	eqtrd 1499	. . . 4 |- ((A e. H~ /\ -. A = 0h) -> ((normh` (T` A)) / (normh` A)) = (normh` (T` ((1 / (normh` A)) .h A))))
59		nmoplbt 9748	. . . . . 6 |- ((T:H~-->H~ /\ ((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (normh` (T` ((1 / (normh` A)) .h A))) <_ (normop` T))
60	22, 59	mp3an1 900	. . . . 5 |- ((((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (normh` (T` ((1 / (normh` A)) .h A))) <_ (normop` T))
61		hvmulclt 8804	. . . . . 6 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> ((1 / (normh` A)) .h A) e. H~)
62	61, 40, 41	sylanc 471	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((1 / (normh` A)) .h A) e. H~)
63		eqlet 5544	. . . . . 6 |- (((normh` ((1 / (normh` A)) .h A)) e. RR /\ (normh` ((1 / (normh` A)) .h A)) = 1) -> (normh` ((1 / (normh` A)) .h A)) <_ 1)
64		normclt 8912	. . . . . . 7 |- (((1 / (normh` A)) .h A) e. H~ -> (normh` ((1 / (normh` A)) .h A)) e. RR)
65	62, 64	syl 10	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` ((1 / (normh` A)) .h A)) e. RR)
66		norm1t 9042	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h