Theorem isblo3i

Description: The predicate "is a bounded linear operator." Definition 2.7-1 of Kreyszig p. 91. (Contributed by NM, 11-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	isblo3i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	isblo3i.m	⊢ 𝑀 = ( normCV ‘ 𝑈 )
	isblo3i.n	⊢ 𝑁 = ( normCV ‘ 𝑊 )
	isblo3i.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
	isblo3i.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
	isblo3i.u	⊢ 𝑈 ∈ NrmCVec
	isblo3i.w	⊢ 𝑊 ∈ NrmCVec
Assertion	isblo3i	⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		isblo3i.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		isblo3i.m	⊢ 𝑀 = ( normCV ‘ 𝑈 )
3		isblo3i.n	⊢ 𝑁 = ( normCV ‘ 𝑊 )
4		isblo3i.4	⊢ 𝐿 = ( 𝑈 LnOp 𝑊 )
5		isblo3i.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
6		isblo3i.u	⊢ 𝑈 ∈ NrmCVec
7		isblo3i.w	⊢ 𝑊 ∈ NrmCVec
8	4 5	bloln	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 ∈ 𝐿 )
9	6 7 8	mp3an12	⊢ ( 𝑇 ∈ 𝐵 → 𝑇 ∈ 𝐿 )
10		eqid	⊢ ( BaseSet ‘ 𝑊 ) = ( BaseSet ‘ 𝑊 )
11		eqid	⊢ ( 𝑈 normOpOLD 𝑊 ) = ( 𝑈 normOpOLD 𝑊 )
12	1 10 11 5	nmblore	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
13	6 7 12	mp3an12	⊢ ( 𝑇 ∈ 𝐵 → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ )
14	1 2 3 11 5 6 7	nmblolbi	⊢ ( ( 𝑇 ∈ 𝐵 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
15	14	ralrimiva	⊢ ( 𝑇 ∈ 𝐵 → ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
16		oveq1	⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) = ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) )
17	16	breq2d	⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) )
18	17	ralbidv	⊢ ( 𝑥 = ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) )
19	18	rspcev	⊢ ( ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) · ( 𝑀 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
20	13 15 19	syl2anc	⊢ ( 𝑇 ∈ 𝐵 → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
21	9 20	jca	⊢ ( 𝑇 ∈ 𝐵 → ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )
22		simp1	⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐿 )
23	1 10 4	lnof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿 ) → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
24	6 7 23	mp3an12	⊢ ( 𝑇 ∈ 𝐿 → 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) )
25	1 10 11	nmoxr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
26	6 7 25	mp3an12	⊢ ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
27	26	3ad2ant1	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ∈ ℝ* )
28		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
29	28	abscld	⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ )
30	29	rexrd	⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) ∈ ℝ* )
31	30	3ad2ant2	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( abs ‘ 𝑥 ) ∈ ℝ* )
32		pnfxr	⊢ +∞ ∈ ℝ*
33	32	a1i	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → +∞ ∈ ℝ* )
34	1 10 2 3 11 6 7	nmoub3i	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) ≤ ( abs ‘ 𝑥 ) )
35		ltpnf	⊢ ( ( abs ‘ 𝑥 ) ∈ ℝ → ( abs ‘ 𝑥 ) < +∞ )
36	29 35	syl	⊢ ( 𝑥 ∈ ℝ → ( abs ‘ 𝑥 ) < +∞ )
37	36	3ad2ant2	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( abs ‘ 𝑥 ) < +∞ )
38	27 31 33 34 37	xrlelttrd	⊢ ( ( 𝑇 : 𝑋 ⟶ ( BaseSet ‘ 𝑊 ) ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ )
39	24 38	syl3an1	⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ )
40	11 4 5	isblo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ ) ) )
41	6 7 40	mp2an	⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ( ( 𝑈 normOpOLD 𝑊 ) ‘ 𝑇 ) < +∞ ) )
42	22 39 41	sylanbrc	⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
43	42	rexlimdv3a	⊢ ( 𝑇 ∈ 𝐿 → ( ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) → 𝑇 ∈ 𝐵 ) )
44	43	imp	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
45	21 44	impbii	⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )