Theorem nmbdfnlbi

Description: A lower bound for the norm of a bounded linear functional. (Contributed by NM, 25-Apr-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nmbdfnlb.1	|- ( T e. LinFn /\ ( normfn ` T ) e. RR )
Assertion	nmbdfnlbi	|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmbdfnlb.1	|- ( T e. LinFn /\ ( normfn ` T ) e. RR )
2		fveq2	|- ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
3	1	simpli	|- T e. LinFn
4	3	lnfn0i	|- ( T ` 0h ) = 0
5	2 4	eqtrdi	|- ( A = 0h -> ( T ` A ) = 0 )
6	5	abs00bd	|- ( A = 0h -> ( abs ` ( T ` A ) ) = 0 )
7		0le0	|- 0 <_ 0
8		fveq2	|- ( A = 0h -> ( normh ` A ) = ( normh ` 0h ) )
9		norm0	|- ( normh ` 0h ) = 0
10	8 9	eqtrdi	|- ( A = 0h -> ( normh ` A ) = 0 )
11	10	oveq2d	|- ( A = 0h -> ( ( normfn ` T ) x. ( normh ` A ) ) = ( ( normfn ` T ) x. 0 ) )
12	1	simpri	|- ( normfn ` T ) e. RR
13	12	recni	|- ( normfn ` T ) e. CC
14	13	mul01i	|- ( ( normfn ` T ) x. 0 ) = 0
15	11 14	eqtr2di	|- ( A = 0h -> 0 = ( ( normfn ` T ) x. ( normh ` A ) ) )
16	7 15	breqtrid	|- ( A = 0h -> 0 <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
17	6 16	eqbrtrd	|- ( A = 0h -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
18	17	adantl	|- ( ( A e. ~H /\ A = 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
19	3	lnfnfi	|- T : ~H --> CC
20	19	ffvelrni	|- ( A e. ~H -> ( T ` A ) e. CC )
21	20	abscld	|- ( A e. ~H -> ( abs ` ( T ` A ) ) e. RR )
22	21	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) e. RR )
23	22	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) e. CC )
24		normcl	|- ( A e. ~H -> ( normh ` A ) e. RR )
25	24	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. RR )
26	25	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. CC )
27		normne0	|- ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
28	27	biimpar	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) =/= 0 )
29	23 26 28	divrec2d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
30	25 28	rereccld	|- ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
31	30	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
32		simpl	|- ( ( A e. ~H /\ A =/= 0h ) -> A e. ~H )
33	3	lnfnmuli	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
34	31 32 33	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
35	34	fveq2d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) )
36	20	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( T ` A ) e. CC )
37	31 36	absmuld	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) )
38		normgt0	|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
39	38	biimpa	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( normh ` A ) )
40	25 39	recgt0d	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
41		0re	|- 0 e. RR
42		ltle	|- ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
43	41 42	mpan	|- ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
44	30 40 43	sylc	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
45	30 44	absidd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
46	45	oveq1d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
47	35 37 46	3eqtrrd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
48	29 47	eqtrd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
49		hvmulcl	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
50	31 32 49	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
51		normcl	|- ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
52	50 51	syl	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
53		norm1	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
54		eqle	|- ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
55	52 53 54	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
56		nmfnlb	|- ( ( 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 ) )
57	19 56	mp3an1	|- ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
58	50 55 57	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
59	48 58	eqbrtrd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) )
60	12	a1i	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normfn ` T ) e. RR )
61		ledivmul2	|- ( ( ( abs ` ( T ` A ) ) e. RR /\ ( normfn ` T ) e. RR /\ ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
62	22 60 25 39 61	syl112anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
63	59 62	mpbid	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
64	18 63	pm2.61dane	|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )