Theorem nmcfnlbi

Description: A lower bound for the norm of a continuous linear functional. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 14-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcfnex.1	|- T e. LinFn
	nmcfnex.2	|- T e. ContFn
Assertion	nmcfnlbi	|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmcfnex.1	|- T e. LinFn
2		nmcfnex.2	|- T e. ContFn
3		fveq2	|- ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
4	1	lnfn0i	|- ( T ` 0h ) = 0
5	3 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 2	nmcfnexi	|- ( 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	1	lnfnfi	|- T : ~H --> CC
20	19	ffvelcdmi	|- ( 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		norm-i	|- ( A e. ~H -> ( ( normh ` A ) = 0 <-> A = 0h ) )
28	27	notbid	|- ( A e. ~H -> ( -. ( normh ` A ) = 0 <-> -. A = 0h ) )
29	28	biimpar	|- ( ( A e. ~H /\ -. A = 0h ) -> -. ( normh ` A ) = 0 )
30	29	neqned	|- ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` A ) =/= 0 )
31	23 26 30	divrec2d	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
32	25 30	rereccld	|- ( ( A e. ~H /\ -. A = 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
33	32	recnd	|- ( ( A e. ~H /\ -. A = 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
34		simpl	|- ( ( A e. ~H /\ -. A = 0h ) -> A e. ~H )
35	1	lnfnmuli	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
36	33 34 35	syl2anc	|- ( ( A e. ~H /\ -. A = 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) )
37	36	fveq2d	|- ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) )
38	20	adantr	|- ( ( A e. ~H /\ -. A = 0h ) -> ( T ` A ) e. CC )
39	33 38	absmuld	|- ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( ( 1 / ( normh ` A ) ) x. ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) )
40		df-ne	|- ( A =/= 0h <-> -. A = 0h )
41		normgt0	|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
42	40 41	bitr3id	|- ( A e. ~H -> ( -. A = 0h <-> 0 < ( normh ` A ) ) )
43	42	biimpa	|- ( ( A e. ~H /\ -. A = 0h ) -> 0 < ( normh ` A ) )
44	25 43	recgt0d	|- ( ( A e. ~H /\ -. A = 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
45		0re	|- 0 e. RR
46		ltle	|- ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
47	45 46	mpan	|- ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
48	32 44 47	sylc	|- ( ( A e. ~H /\ -. A = 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
49	32 48	absidd	|- ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
50	49	oveq1d	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( abs ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) )
51	37 39 50	3eqtrrd	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( 1 / ( normh ` A ) ) x. ( abs ` ( T ` A ) ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
52	31 51	eqtrd	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) = ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
53		hvmulcl	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
54	33 34 53	syl2anc	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
55		normcl	|- ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
56	54 55	syl	|- ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
57		norm1	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
58	40 57	sylan2br	|- ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
59		eqle	|- ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
60	56 58 59	syl2anc	|- ( ( A e. ~H /\ -. A = 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
61		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 ) )
62	19 61	mp3an1	|- ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
63	54 60 62	syl2anc	|- ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normfn ` T ) )
64	52 63	eqbrtrd	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) )
65	12	a1i	|- ( ( A e. ~H /\ -. A = 0h ) -> ( normfn ` T ) e. RR )
66		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 ) ) ) )
67	22 65 25 43 66	syl112anc	|- ( ( A e. ~H /\ -. A = 0h ) -> ( ( ( abs ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normfn ` T ) <-> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) ) )
68	64 67	mpbid	|- ( ( A e. ~H /\ -. A = 0h ) -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )
69	18 68	pm2.61dan	|- ( A e. ~H -> ( abs ` ( T ` A ) ) <_ ( ( normfn ` T ) x. ( normh ` A ) ) )