Theorem blo3i

Description: Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008) (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	blo3i	⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )

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		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) = ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) )
9	8	breq2d	⊢ ( 𝑥 = 𝐴 → ( ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) )
10	9	ralbidv	⊢ ( 𝑥 = 𝐴 → ( ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) )
11	10	rspcev	⊢ ( ( 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) )
12	1 2 3 4 5 6 7	isblo3i	⊢ ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) )
13	12	biimpri	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ∃ 𝑥 ∈ ℝ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝑥 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )
14	11 13	sylan2	⊢ ( ( 𝑇 ∈ 𝐿 ∧ ( 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) ) → 𝑇 ∈ 𝐵 )
15	14	3impb	⊢ ( ( 𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀ 𝑦 ∈ 𝑋 ( 𝑁 ‘ ( 𝑇 ‘ 𝑦 ) ) ≤ ( 𝐴 · ( 𝑀 ‘ 𝑦 ) ) ) → 𝑇 ∈ 𝐵 )