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	⊢ 𝑇 ∈ LinOp
	nmcopex.2	⊢ 𝑇 ∈ ContOp
Assertion	nmcoplbi	⊢ ( 𝐴 ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝐴 ) ) ≤ ( ( normop ‘ 𝑇 ) · ( normℎ ‘ 𝐴 ) ) )

Proof

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