Theorem nmbdoplb 9887

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

Hypothesis

Ref	Expression
nmbdoplb.1	|- T e. BndLinOp

Assertion

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

Proof of Theorem nmbdoplb

Step	Hyp	Ref	Expression
1		fveq2 3715	. . . 4 |- (A = 0h -> (T` A) = (T` 0h))
2	1	fveq2d 3719	. . 3 |- (A = 0h -> (normh` (T` A)) = (normh` (T` 0h)))
3		fveq2 3715	. . . 4 |- (A = 0h -> (normh` A) = (normh` 0h))
4	3	opreq2d 3967	. . 3 |- (A = 0h -> ((normop` T) x. (normh` A)) = ((normop` T) x. (normh` 0h)))
5	2, 4	breq12d 2626	. 2 |- (A = 0h -> ((normh` (T` A)) <_ ((normop` T) x. (normh` A)) <-> (normh` (T` 0h)) <_ ((normop` T) x. (normh` 0h))))
6		divrec2t 5711	. . . . . 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))))
7		nmbdoplb.1	. . . . . . . . . . . 12 |- T e. BndLinOp
8		bdoplnt 9728	. . . . . . . . . . . 12 |- (T e. BndLinOp -> T e. LinOp)
9	7, 8	ax-mp 7	. . . . . . . . . . 11 |- T e. LinOp
10	9	lnopf 9832	. . . . . . . . . 10 |- T:H~-->H~
11	10	ffvelrni 3806	. . . . . . . . 9 |- (A e. H~ -> (T` A) e. H~)
12		normclt 8930	. . . . . . . . 9 |- ((T` A) e. H~ -> (normh` (T` A)) e. RR)
13	11, 12	syl 10	. . . . . . . 8 |- (A e. H~ -> (normh` (T` A)) e. RR)
14	13	adantr 389	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` (T` A)) e. RR)
15	14	recnd 5295	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` (T` A)) e. CC)
16		normclt 8930	. . . . . . . 8 |- (A e. H~ -> (normh` A) e. RR)
17	16	adantr 389	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) e. RR)
18	17	recnd 5295	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) e. CC)
19		normne0t 8936	. . . . . . 7 |- (A e. H~ -> ((normh` A) =/= 0 <-> A =/= 0h))
20	19	biimpar 417	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) =/= 0)
21	6, 15, 18, 20	syl3anc 857	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> ((normh` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (normh` (T` A))))
22	9	lnopmul 9835	. . . . . . . 8 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) .h (T` A)))
23		rerecclt 5767	. . . . . . . . . 10 |- (((normh` A) e. RR /\ (normh` A) =/= 0) -> (1 / (normh` A)) e. RR)
24	23, 17, 20	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ A =/= 0h) -> (1 / (normh` A)) e. RR)
25	24	recnd 5295	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (1 / (normh` A)) e. CC)
26		pm3.26 319	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> A e. H~)
27	22, 25, 26	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) .h (T` A)))
28	27	fveq2d 3719	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` (T` ((1 / (normh` A)) .h A))) = (normh` ((1 / (normh` A)) .h (T` A))))
29		norm-iiit 8946	. . . . . . 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))))
30	11	adantr 389	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (T` A) e. H~)
31	29, 25, 30	sylanc 471	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h (T` A))) = ((abs` (1 / (normh` A))) x. (normh` (T` A))))
32		absidt 6805	. . . . . . . 8 |- (((1 / (normh` A)) e. RR /\ 0 <_ (1 / (normh` A))) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
33		0re 5420	. . . . . . . . . 10 |- 0 e. RR
34		ltlet 5501	. . . . . . . . . 10 |- ((0 e. RR /\ (1 / (normh` A)) e. RR) -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
35	33, 34	mpan 694	. . . . . . . . 9 |- ((1 / (normh` A)) e. RR -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
36		recgt0t 5823	. . . . . . . . . 10 |- (((normh` A) e. RR /\ 0 < (normh` A)) -> 0 < (1 / (normh` A)))
37		normgt0t 8933	. . . . . . . . . . 11 |- (A e. H~ -> (A =/= 0h <-> 0 < (normh` A)))
38	37	biimpa 416	. . . . . . . . . 10 |- ((A e. H~ /\ A =/= 0h) -> 0 < (normh` A))
39	36, 17, 38	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ A =/= 0h) -> 0 < (1 / (normh` A)))
40	35, 24, 39	sylc 68	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> 0 <_ (1 / (normh` A)))
41	32, 24, 40	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
42	41	opreq1d 3966	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (1 / (normh` A))) x. (normh` (T` A))) = ((1 / (normh` A)) x. (normh` (T` A))))
43	28, 31, 42	3eqtrrd 1509	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> ((1 / (normh` A)) x. (normh` (T` A))) = (normh` (T` ((1 / (normh` A)) .h A))))
44	21, 43	eqtrd 1504	. . . 4 |- ((A e. H~ /\ A =/= 0h) -> ((normh` (T` A)) / (normh` A)) = (normh` (T` ((1 / (normh` A)) .h A))))
45		nmoplbt 9771	. . . . . 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))
46	10, 45	mp3an1 901	. . . . 5 |- ((((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (normh` (T` ((1 / (normh` A)) .h A))) <_ (normop` T))
47		hvmulclt 8822	. . . . . 6 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> ((1 / (normh` A)) .h A) e. H~)
48	47, 25, 26	sylanc 471	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> ((1 / (normh` A)) .h A) e. H~)
49		eqlet 5552	. . . . . 6 |- (((normh` ((1 / (normh` A)) .h A)) e. RR /\ (normh` ((1 / (normh` A)) .h A)) = 1) -> (normh` ((1 / (normh` A)) .h A)) <_ 1)
50		normclt 8930	. . . . . . 7 |- (((1 / (normh` A)) .h A) e. H~ -> (normh` ((1 / (normh` A)) .h A)) e. RR)
51	48, 50	syl 10	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) e. RR)
52		norm1t 9060	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) = 1)
53	49, 51, 52	sylanc 471	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) <_ 1)
54	46, 48, 53	sylanc 471	. . . 4 |- ((A e. H~ /\ A =/= 0h) -> (normh` (T` ((1 / (normh` A)) .h A))) <_ (normop` T))
55	44, 54	eqbrtrd 2630	. . 3 |- ((A e. H~ /\ A =/= 0h) -> ((normh` (T` A)) / (normh` A)) <_ (normop` T))
56		ledivmul2t 5831	. . . 4 |- ((((normh` (T` A)) e. RR /\ (normh` A) e. RR /\ (normop` T) e. RR) /\ 0 < (normh` A)) -> (((normh` (T` A)) / (normh` A)) <_ (normop` T) <-> (normh` (T` A)) <_ ((normop` T) x. (normh` A))))
57		nmopret 9737	. . . . . . 7 |- (T e. BndLinOp -> (normop` T) e. RR)
58	7, 57	ax-mp 7	. . . . . 6 |- (normop` T) e. RR
59	58	a1i 8	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> (normop` T) e. RR)
60	14, 17, 59