Theorem nmcoplbi

Description: A lower bound for the norm of a continuous linear operator. Theorem 3.5(ii) of Beran p. 99. (Contributed by NM, 7-Feb-2006) (Revised by Mario Carneiro, 17-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmcopex.1	|- T e. LinOp
	nmcopex.2	|- T e. ContOp
Assertion	nmcoplbi	|- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmcopex.1	|- T e. LinOp
2		nmcopex.2	|- T e. ContOp
3		0le0	|- 0 <_ 0
4	3	a1i	|- ( A = 0h -> 0 <_ 0 )
5		fveq2	|- ( A = 0h -> ( T ` A ) = ( T ` 0h ) )
6	1	lnop0i	|- ( T ` 0h ) = 0h
7	5 6	eqtrdi	|- ( A = 0h -> ( T ` A ) = 0h )
8	7	fveq2d	|- ( A = 0h -> ( normh ` ( T ` A ) ) = ( normh ` 0h ) )
9		norm0	|- ( normh ` 0h ) = 0
10	8 9	eqtrdi	|- ( A = 0h -> ( normh ` ( T ` A ) ) = 0 )
11		fveq2	|- ( A = 0h -> ( normh ` A ) = ( normh ` 0h ) )
12	11 9	eqtrdi	|- ( A = 0h -> ( normh ` A ) = 0 )
13	12	oveq2d	|- ( A = 0h -> ( ( normop ` T ) x. ( normh ` A ) ) = ( ( normop ` T ) x. 0 ) )
14	1 2	nmcopexi	|- ( normop ` T ) e. RR
15	14	recni	|- ( normop ` T ) e. CC
16	15	mul01i	|- ( ( normop ` T ) x. 0 ) = 0
17	13 16	eqtrdi	|- ( A = 0h -> ( ( normop ` T ) x. ( normh ` A ) ) = 0 )
18	4 10 17	3brtr4d	|- ( A = 0h -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
19	18	adantl	|- ( ( A e. ~H /\ A = 0h ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
20		normcl	|- ( A e. ~H -> ( normh ` A ) e. RR )
21	20	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. RR )
22		normne0	|- ( A e. ~H -> ( ( normh ` A ) =/= 0 <-> A =/= 0h ) )
23	22	biimpar	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) =/= 0 )
24	21 23	rereccld	|- ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. RR )
25		normgt0	|- ( A e. ~H -> ( A =/= 0h <-> 0 < ( normh ` A ) ) )
26	25	biimpa	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( normh ` A ) )
27	21 26	recgt0d	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 < ( 1 / ( normh ` A ) ) )
28		0re	|- 0 e. RR
29		ltle	|- ( ( 0 e. RR /\ ( 1 / ( normh ` A ) ) e. RR ) -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
30	28 29	mpan	|- ( ( 1 / ( normh ` A ) ) e. RR -> ( 0 < ( 1 / ( normh ` A ) ) -> 0 <_ ( 1 / ( normh ` A ) ) ) )
31	24 27 30	sylc	|- ( ( A e. ~H /\ A =/= 0h ) -> 0 <_ ( 1 / ( normh ` A ) ) )
32	24 31	absidd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( abs ` ( 1 / ( normh ` A ) ) ) = ( 1 / ( normh ` A ) ) )
33	32	oveq1d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) = ( ( 1 / ( normh ` A ) ) x. ( normh ` ( T ` A ) ) ) )
34	24	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( 1 / ( normh ` A ) ) e. CC )
35		simpl	|- ( ( A e. ~H /\ A =/= 0h ) -> A e. ~H )
36	1	lnopmuli	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) )
37	34 35 36	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) = ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) )
38	37	fveq2d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) )
39	1	lnopfi	|- T : ~H --> ~H
40	39	ffvelrni	|- ( A e. ~H -> ( T ` A ) e. ~H )
41	40	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( T ` A ) e. ~H )
42		norm-iii	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ ( T ` A ) e. ~H ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
43	34 41 42	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h ( T ` A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
44	38 43	eqtrd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) = ( ( abs ` ( 1 / ( normh ` A ) ) ) x. ( normh ` ( T ` A ) ) ) )
45		normcl	|- ( ( T ` A ) e. ~H -> ( normh ` ( T ` A ) ) e. RR )
46	40 45	syl	|- ( A e. ~H -> ( normh ` ( T ` A ) ) e. RR )
47	46	adantr	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) e. RR )
48	47	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) e. CC )
49	21	recnd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` A ) e. CC )
50	48 49 23	divrec2d	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) = ( ( 1 / ( normh ` A ) ) x. ( normh ` ( T ` A ) ) ) )
51	33 44 50	3eqtr4rd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) = ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) )
52		hvmulcl	|- ( ( ( 1 / ( normh ` A ) ) e. CC /\ A e. ~H ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
53	34 35 52	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( 1 / ( normh ` A ) ) .h A ) e. ~H )
54		normcl	|- ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
55	53 54	syl	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR )
56		norm1	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 )
57		eqle	|- ( ( ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) e. RR /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) = 1 ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
58	55 56 57	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 )
59		nmoplb	|- ( ( T : ~H --> ~H /\ ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
60	39 59	mp3an1	|- ( ( ( ( 1 / ( normh ` A ) ) .h A ) e. ~H /\ ( normh ` ( ( 1 / ( normh ` A ) ) .h A ) ) <_ 1 ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
61	53 58 60	syl2anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` ( ( 1 / ( normh ` A ) ) .h A ) ) ) <_ ( normop ` T ) )
62	51 61	eqbrtrd	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) )
63	14	a1i	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normop ` T ) e. RR )
64		ledivmul2	|- ( ( ( normh ` ( T ` A ) ) e. RR /\ ( normop ` T ) e. RR /\ ( ( normh ` A ) e. RR /\ 0 < ( normh ` A ) ) ) -> ( ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) <-> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
65	47 63 21 26 64	syl112anc	|- ( ( A e. ~H /\ A =/= 0h ) -> ( ( ( normh ` ( T ` A ) ) / ( normh ` A ) ) <_ ( normop ` T ) <-> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) ) )
66	62 65	mpbid	|- ( ( A e. ~H /\ A =/= 0h ) -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )
67	19 66	pm2.61dane	|- ( A e. ~H -> ( normh ` ( T ` A ) ) <_ ( ( normop ` T ) x. ( normh ` A ) ) )