Theorem nmbdfnlb 9893

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

Hypothesis

Ref	Expression
nmbdfnlb.1	|- (T e. LinFn /\ (normfn` T) e. RR)

Assertion

Ref	Expression
nmbdfnlb	|- (A e. H~ -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))

Proof of Theorem nmbdfnlb

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . . . . 7 |- (A = 0h -> (T` A) = (T` 0h))
2		nmbdfnlb.1	. . . . . . . . 9 |- (T e. LinFn /\ (normfn` T) e. RR)
3	2	pm3.26i 320	. . . . . . . 8 |- T e. LinFn
4	3	lnfn0 9886	. . . . . . 7 |- (T` 0h) = 0
5	1, 4	syl6eq 1515	. . . . . 6 |- (A = 0h -> (T` A) = 0)
6	5	fveq2d 3713	. . . . 5 |- (A = 0h -> (abs` (T` A)) = (abs` 0))
7		abs0 6814	. . . . 5 |- (abs` 0) = 0
8	6, 7	syl6eq 1515	. . . 4 |- (A = 0h -> (abs` (T` A)) = 0)
9		fveq2 3709	. . . . . . . 8 |- (A = 0h -> (normh` A) = (normh` 0h))
10		norm0 8916	. . . . . . . 8 |- (normh` 0h) = 0
11	9, 10	syl6eq 1515	. . . . . . 7 |- (A = 0h -> (normh` A) = 0)
12	11	opreq2d 3961	. . . . . 6 |- (A = 0h -> ((normfn` T) x. (normh` A)) = ((normfn` T) x. 0))
13	2	pm3.27i 324	. . . . . . . 8 |- (normfn` T) e. RR
14	13	recn 5286	. . . . . . 7 |- (normfn` T) e. CC
15	14	mul01 5403	. . . . . 6 |- ((normfn` T) x. 0) = 0
16	12, 15	syl6req 1516	. . . . 5 |- (A = 0h -> 0 = ((normfn` T) x. (normh` A)))
17		0re 5412	. . . . . 6 |- 0 e. RR
18	17	leid 5584	. . . . 5 |- 0 <_ 0
19	16, 18	syl5breq 2640	. . . 4 |- (A = 0h -> 0 <_ ((normfn` T) x. (normh` A)))
20	8, 19	eqbrtrd 2625	. . 3 |- (A = 0h -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
21	20	adantl 388	. 2 |- ((A e. H~ /\ A = 0h) -> (abs` (T` A)) <_ ((normfn` T) x. (normh` A)))
22		divrec2t 5703	. . . . . . 7 |- (((abs` (T` A)) e. CC /\ (normh` A) e. CC /\ (normh` A) =/= 0) -> ((abs` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (abs` (T` A))))
23	3	lnfnf 9885	. . . . . . . . . . 11 |- T:H~-->CC
24	23	ffvelrni 3800	. . . . . . . . . 10 |- (A e. H~ -> (T` A) e. CC)
25		absclt 6768	. . . . . . . . . 10 |- ((T` A) e. CC -> (abs` (T` A)) e. RR)
26	24, 25	syl 10	. . . . . . . . 9 |- (A e. H~ -> (abs` (T` A)) e. RR)
27	26	adantr 389	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` A)) e. RR)
28	27	recnd 5287	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` A)) e. CC)
29		normclt 8912	. . . . . . . . 9 |- (A e. H~ -> (normh` A) e. RR)
30	29	adantr 389	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) e. RR)
31	30	recnd 5287	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) e. CC)
32		normne0t 8918	. . . . . . . 8 |- (A e. H~ -> ((normh` A) =/= 0 <-> A =/= 0h))
33	32	biimpar 417	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) =/= 0)
34	22, 28, 31, 33	syl3anc 856	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (abs` (T` A))))
35	3	lnfnmul 9888	. . . . . . . . 9 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) x. (T` A)))
36		rerecclt 5759	. . . . . . . . . . 11 |- (((normh` A) e. RR /\ (normh` A) =/= 0) -> (1 / (normh` A)) e. RR)
37	36, 30, 33	sylanc 471	. . . . . . . . . 10 |- ((A e. H~ /\ A =/= 0h) -> (1 / (normh` A)) e. RR)
38	37	recnd 5287	. . . . . . . . 9 |- ((A e. H~ /\ A =/= 0h) -> (1 / (normh` A)) e. CC)
39		pm3.26 319	. . . . . . . . 9 |- ((A e. H~ /\ A =/= 0h) -> A e. H~)
40	35, 38, 39	sylanc 471	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) x. (T` A)))
41	40	fveq2d 3713	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` ((1 / (normh` A)) .h A))) = (abs` ((1 / (normh` A)) x. (T` A))))
42		absmult 6793	. . . . . . . 8 |- (((1 / (normh` A)) e. CC /\ (T` A) e. CC) -> (abs` ((1 / (normh` A)) x. (T` A))) = ((abs` (1 / (normh` A))) x. (abs` (T` A))))
43	24	adantr 389	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (T` A) e. CC)
44	42, 38, 43	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` ((1 / (normh` A)) x. (T` A))) = ((abs` (1 / (normh` A))) x. (abs` (T` A))))
45		absidt 6797	. . . . . . . . 9 |- (((1 / (normh` A)) e. RR /\ 0 <_ (1 / (normh` A))) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
46		ltlet 5493	. . . . . . . . . . 11 |- ((0 e. RR /\ (1 / (normh` A)) e. RR) -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
47	17, 46	mpan 693	. . . . . . . . . 10 |- ((1 / (normh` A)) e. RR -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
48		recgt0t 5815	. . . . . . . . . . 11 |- (((normh` A) e. RR /\ 0 < (normh` A)) -> 0 < (1 / (normh` A)))
49		normgt0t 8915	. . . . . . . . . . . 12 |- (A e. H~ -> (A =/= 0h <-> 0 < (normh` A)))
50	49	biimpa 416	. . . . . . . . . . 11 |- ((A e. H~ /\ A =/= 0h) -> 0 < (normh` A))
51	48, 30, 50	sylanc 471	. . . . . . . . . 10 |- ((A e. H~ /\ A =/= 0h) -> 0 < (1 / (normh` A)))
52	47, 37, 51	sylc 68	. . . . . . . . 9 |- ((A e. H~ /\ A =/= 0h) -> 0 <_ (1 / (normh` A)))
53	45, 37, 52	sylanc 471	. . . . . . . 8 |- ((A e. H~ /\ A =/= 0h) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
54	53	opreq1d 3960	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (1 / (normh` A))) x. (abs` (T` A))) = ((1 / (normh` A)) x. (abs` (T` A))))
55	41, 44, 54	3eqtrrd 1504	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((1 / (normh` A)) x. (abs` (T` A))) = (abs` (T` ((1 / (normh` A)) .h A))))
56	34, 55	eqtrd 1499	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (T` A)) / (normh` A)) = (abs` (T` ((1 / (normh` A)) .h A))))
57		nmfnlbt 9764	. . . . . . 7 |- ((T:H~-->CC /\ ((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (abs` (T` ((1 / (normh` A)) .h A))) <_ (normfn` T))
58	23, 57	mp3an1 900	. . . . . 6 |- ((((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (abs` (T` ((1 / (normh` A)) .h A))) <_ (normfn` T))
59		hvmulclt 8804	. . . . . . 7 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> ((1 / (normh` A)) .h A) e. H~)
60	59, 38, 39	sylanc 471	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((1 / (normh` A)) .h A) e. H~)
61		eqlet 5544	. . . . . . 7 |- (((normh` ((1 / (normh` A)) .h A)) e. RR /\ (normh` ((1 / (normh` A)) .h A)) = 1) -> (normh` ((1 / (normh` A)) .h A)) <_ 1)
62		normclt 8912	. . . . . . . 8 |- (((1 / (normh` A)) .h A) e. H~ -> (normh` ((1 / (normh` A)) .h A)) e. RR)
63	60, 62	syl 10	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) e. RR)
64		norm1t 9042	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) = 1)
65	61, 63, 64	sylanc 471	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> (normh` ((1 / (normh` A)) .h A)) <_ 1)
66	58, 60, 65	sylanc 471	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` ((1 / (normh` A)