Theorem nmcfnlb 9902

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

Hypotheses

Ref	Expression
nmcfnex.1	|- T e. LinFn
nmcfnex.2	|- T e. ConFn

Assertion

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

Proof of Theorem nmcfnlb

Step	Hyp	Ref	Expression
1		fveq2 3709	. . . . . . 7 |- (A = 0h -> (T` A) = (T` 0h))
2		nmcfnex.1	. . . . . . . 8 |- T e. LinFn
3	2	lnfn0 9886	. . . . . . 7 |- (T` 0h) = 0
4	1, 3	syl6eq 1515	. . . . . 6 |- (A = 0h -> (T` A) = 0)
5	4	fveq2d 3713	. . . . 5 |- (A = 0h -> (abs` (T` A)) = (abs` 0))
6		abs0 6814	. . . . 5 |- (abs` 0) = 0
7	5, 6	syl6eq 1515	. . . 4 |- (A = 0h -> (abs` (T` A)) = 0)
8		fveq2 3709	. . . . . . . 8 |- (A = 0h -> (normh` A) = (normh` 0h))
9		norm0 8916	. . . . . . . 8 |- (normh` 0h) = 0
10	8, 9	syl6eq 1515	. . . . . . 7 |- (A = 0h -> (normh` A) = 0)
11	10	opreq2d 3961	. . . . . 6 |- (A = 0h -> ((normfn` T) x. (normh` A)) = ((normfn` T) x. 0))
12		nmcfnex.2	. . . . . . . . 9 |- T e. ConFn
13	2, 12	nmcfnex 9901	. . . . . . . 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	11, 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	7, 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	. . . . . 6 |- (((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	2	lnfnf 9885	. . . . . . . . . 10 |- T:H~-->CC
24	23	ffvelrni 3800	. . . . . . . . 9 |- (A e. H~ -> (T` A) e. CC)
25		absclt 6768	. . . . . . . . 9 |- ((T` A) e. CC -> (abs` (T` A)) e. RR)
26	24, 25	syl 10	. . . . . . . 8 |- (A e. H~ -> (abs` (T` A)) e. RR)
27	26	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (abs` (T` A)) e. RR)
28	27	recnd 5287	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (abs` (T` A)) e. CC)
29		normclt 8912	. . . . . . . 8 |- (A e. H~ -> (normh` A) e. RR)
30	29	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) e. RR)
31	30	recnd 5287	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) e. CC)
32		norm-it 8917	. . . . . . . . 9 |- (A e. H~ -> ((normh` A) = 0 <-> A = 0h))
33	32	negbid 609	. . . . . . . 8 |- (A e. H~ -> (-. (normh` A) = 0 <-> -. A = 0h))
34	33	biimpar 417	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> -. (normh` A) = 0)
35		df-ne 1579	. . . . . . 7 |- ((normh` A) =/= 0 <-> -. (normh` A) = 0)
36	34, 35	sylibr 200	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` A) =/= 0)
37	22, 28, 31, 36	syl3anc 856	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((abs` (T` A)) / (normh` A)) = ((1 / (normh` A)) x. (abs` (T` A))))
38	2	lnfnmul 9888	. . . . . . . 8 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) x. (T` A)))
39		rerecclt 5759	. . . . . . . . . 10 |- (((normh` A) e. RR /\ (normh` A) =/= 0) -> (1 / (normh` A)) e. RR)
40	39, 30, 36	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ -. A = 0h) -> (1 / (normh` A)) e. RR)
41	40	recnd 5287	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> (1 / (normh` A)) e. CC)
42		pm3.26 319	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> A e. H~)
43	38, 41, 42	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (T` ((1 / (normh` A)) .h A)) = ((1 / (normh` A)) x. (T` A)))
44	43	fveq2d 3713	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (abs` (T` ((1 / (normh` A)) .h A))) = (abs` ((1 / (normh` A)) x. (T` A))))
45		absmult 6793	. . . . . . 7 |- (((1 / (normh` A)) e. CC /\ (T` A) e. CC) -> (abs` ((1 / (normh` A)) x. (T` A))) = ((abs` (1 / (normh` A))) x. (abs` (T` A))))
46	24	adantr 389	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (T` A) e. CC)
47	45, 41, 46	sylanc 471	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (abs` ((1 / (normh` A)) x. (T` A))) = ((abs` (1 / (normh` A))) x. (abs` (T` A))))
48		absidt 6797	. . . . . . . 8 |- (((1 / (normh` A)) e. RR /\ 0 <_ (1 / (normh` A))) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
49		ltlet 5493	. . . . . . . . . 10 |- ((0 e. RR /\ (1 / (normh` A)) e. RR) -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
50	17, 49	mpan 693	. . . . . . . . 9 |- ((1 / (normh` A)) e. RR -> (0 < (1 / (normh` A)) -> 0 <_ (1 / (normh` A))))
51		recgt0t 5815	. . . . . . . . . 10 |- (((normh` A) e. RR /\ 0 < (normh` A)) -> 0 < (1 / (normh` A)))
52		normgt0tOLD 8914	. . . . . . . . . . 11 |- (A e. H~ -> (-. A = 0h <-> 0 < (normh` A)))
53	52	biimpa 416	. . . . . . . . . 10 |- ((A e. H~ /\ -. A = 0h) -> 0 < (normh` A))
54	51, 30, 53	sylanc 471	. . . . . . . . 9 |- ((A e. H~ /\ -. A = 0h) -> 0 < (1 / (normh` A)))
55	50, 40, 54	sylc 68	. . . . . . . 8 |- ((A e. H~ /\ -. A = 0h) -> 0 <_ (1 / (normh` A)))
56	48, 40, 55	sylanc 471	. . . . . . 7 |- ((A e. H~ /\ -. A = 0h) -> (abs` (1 / (normh` A))) = (1 / (normh` A)))
57	56	opreq1d 3960	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> ((abs` (1 / (normh` A))) x. (abs` (T` A))) = ((1 / (normh` A)) x. (abs` (T` A))))
58	44, 47, 57	3eqtrrd 1504	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((1 / (normh` A)) x. (abs` (T` A))) = (abs` (T` ((1 / (normh` A)) .h A))))
59	37, 58	eqtrd 1499	. . . 4 |- ((A e. H~ /\ -. A = 0h) -> ((abs` (T` A)) / (normh` A)) = (abs` (T` ((1 / (normh` A)) .h A))))
60		nmfnlbt 9764	. . . . . 6 |- ((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))
61	23, 60	mp3an1 900	. . . . 5 |- ((((1 / (normh` A)) .h A) e. H~ /\ (normh` ((1 / (normh` A)) .h A)) <_ 1) -> (abs` (T` ((1 / (normh` A)) .h A))) <_ (normfn` T))
62		hvmulclt 8804	. . . . . 6 |- (((1 / (normh` A)) e. CC /\ A e. H~) -> ((1 / (normh` A)) .h A) e. H~)
63	62, 41, 42	sylanc 471	. . . . 5 |- ((A e. H~ /\ -. A = 0h) -> ((1 / (normh` A)) .h A) e. H~)
64		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)
65		normclt 8912	. . . . . . 7 |- (((1 / (normh` A)) .h A) e. H~ -> (normh` ((1 / (normh` A)) .h A)) e. RR)
66	63, 65	syl 10	. . . . . 6 |- ((A e. H~ /\ -. A = 0h) -> (normh` ((1 / (normh` A)) .h A)) e. RR)
67		norm1t 9042	. . . . . . 7 |- ((A e. H~ /\ A =/= 0h) -> (normh` (<