Theorem nmbdfnlb 9916

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 3715	. . . . . . 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 9909	. . . . . . 7 |- (T` 0h) = 0
5	1, 4	syl6eq 1520	. . . . . 6 |- (A = 0h -> (T` A) = 0)
6	5	fveq2d 3719	. . . . 5 |- (A = 0h -> (abs` (T` A)) = (abs` 0))
7		abs0 6822	. . . . 5 |- (abs` 0) = 0
8	6, 7	syl6eq 1520	. . . 4 |- (A = 0h -> (abs` (T` A)) = 0)
9		fveq2 3715	. . . . . . . 8 |- (A = 0h -> (normh` A) = (normh` 0h))
10		norm0 8934	. . . . . . . 8 |- (normh` 0h) = 0
11	9, 10	syl6eq 1520	. . . . . . 7 |- (A = 0h -> (normh` A) = 0)
12	11	opreq2d 3967	. . . . . 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 5294	. . . . . . 7 |- (normfn` T) e. CC
15	14	mul01 5411	. . . . . 6 |- ((normfn` T) x. 0) = 0
16	12, 15	syl6req 1521	. . . . 5 |- (A = 0h -> 0 = ((normfn` T) x. (normh` A)))
17		0re 5420	. . . . . 6 |- 0 e. RR
18	17	leid 5592	. . . . 5 |- 0 <_ 0
19	16, 18	syl5breq 2645	. . . 4 |- (A = 0h -> 0 <_ ((normfn` T) x. (normh` A)))
20	8, 19	eqbrtrd 2630	. . 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 5711	. . . . . . 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 9908	. . . . . . . . . . 11 |- T:H~-->CC
24	23	ffvelrni 3806	. . . . . . . . . 10 |- (A e. H~ -> (T` A) e. CC)
25		absclt 6776	. . . . . . . . . 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 5295	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` A)) e. CC)
29		normclt 8930	. . . . . . . . 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 5295	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` A) e. CC)
32		normne0t 8936	. . . . . . . 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 857	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (abs` (T` A))))
35	3	lnfnmul 9911	. . . . . . . . 9 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) x. (T` A)))
36		rerecclt 5767	. . . . . . . . . . 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 5295	. . . . . . . . 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 3719	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (abs` (T` ((1 / (normh` A)) .h A))) = (abs` ((1 / (normh` A)) x. (T` A))))
42		absmult 6801	. . . . . . . 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 6805	. . . . . . . . 9 |- (((1 / (normh` A)) e. RR /\ 0 <_ (1 / (normh` A))) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
46		ltlet 5501	. . . . . . . . . . 11 |- ((0 e. RR /\ (1 / (normh` A)) e. RR) -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
47	17, 46	mpan 694	. . . . . . . . . 10 |- ((1 / (normh` A)) e. RR -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
48		recgt0t 5823	. . . . . . . . . . 11 |- (((normh` A) e. RR /\ 0 < (normh` A)) -> 0 < (1 / (normh` A)))
49		normgt0t 8933	. . . . . . . . . . . 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 3966	. . . . . . 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 1509	. . . . . 6 |- ((A e. H~ /\ A =/= 0h) -> ((1 / (normh` A)) x. (abs` (T` A))) = (abs` (T` ((1 / (normh` A)) .h A))))
56	34, 55	eqtrd 1504	. . . . 5 |- ((A e. H~ /\ A =/= 0h) -> ((abs` (T` A)) / (normh` A)) = (abs` (T` ((1 / (normh` A)) .h A))))
57		nmfnlbt 9787	. . . . . . 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 901	. . . . . 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 8822	. . . . . . 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 5552	. . . . . . 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 8930	. . . . . . . 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 9060	. . . . . . 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)