Metamath Proof Explorer

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 ⊢ X = BaseSet ⁡ U
isblo3i.m ⊢ M = norm CV ⁡ U
isblo3i.n ⊢ N = norm CV ⁡ W
isblo3i.4 ⊢ L = U LnOp W
isblo3i.5 ⊢ B = U BLnOp W
isblo3i.u ⊢ U ∈ NrmCVec
isblo3i.w ⊢ W ∈ NrmCVec
Assertion blo3i ⊢ T ∈ L ∧ A ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y → T ∈ B

Proof

Step Hyp Ref Expression
1 isblo3i.1 ⊢ X = BaseSet ⁡ U
2 isblo3i.m ⊢ M = norm CV ⁡ U
3 isblo3i.n ⊢ N = norm CV ⁡ W
4 isblo3i.4 ⊢ L = U LnOp W
5 isblo3i.5 ⊢ B = U BLnOp W
6 isblo3i.u ⊢ U ∈ NrmCVec
7 isblo3i.w ⊢ W ∈ NrmCVec
8 oveq1 ⊢ x = A → x ⁢ M ⁡ y = A ⁢ M ⁡ y
9 8 breq2d ⊢ x = A → N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y ↔ N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y
10 9 ralbidv ⊢ x = A → ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y ↔ ∀ y ∈ X N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y
11 10 rspcev ⊢ A ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y → ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y
12 1 2 3 4 5 6 7 isblo3i ⊢ T ∈ B ↔ T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y
13 12 biimpri ⊢ T ∈ L ∧ ∃ x ∈ ℝ ∀ y ∈ X N ⁡ T ⁡ y ≤ x ⁢ M ⁡ y → T ∈ B
14 11 13 sylan2 ⊢ T ∈ L ∧ A ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y → T ∈ B
15 14 3impb ⊢ T ∈ L ∧ A ∈ ℝ ∧ ∀ y ∈ X N ⁡ T ⁡ y ≤ A ⁢ M ⁡ y → T ∈ B