Metamath Proof Explorer

Theorem nmoolb

Description: A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoolb.1 ⊢ X = BaseSet ⁡ U
nmoolb.2 ⊢ Y = BaseSet ⁡ W
nmoolb.l ⊢ L = norm CV ⁡ U
nmoolb.m ⊢ M = norm CV ⁡ W
nmoolb.3 ⊢ N = U normOp OLD W
Assertion nmoolb ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ A ∈ X ∧ L ⁡ A ≤ 1 → M ⁡ T ⁡ A ≤ N ⁡ T

Proof

Step Hyp Ref Expression
1 nmoolb.1 ⊢ X = BaseSet ⁡ U
2 nmoolb.2 ⊢ Y = BaseSet ⁡ W
3 nmoolb.l ⊢ L = norm CV ⁡ U
4 nmoolb.m ⊢ M = norm CV ⁡ W
5 nmoolb.3 ⊢ N = U normOp OLD W
6 2 4 nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ⊆ ℝ
7 ressxr ⊢ ℝ ⊆ ℝ *
8 6 7 sstrdi ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ⊆ ℝ *
9 8 3adant1 ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ⊆ ℝ *
10 fveq2 ⊢ y = A → L ⁡ y = L ⁡ A
11 10 breq1d ⊢ y = A → L ⁡ y ≤ 1 ↔ L ⁡ A ≤ 1
12 2fveq3 ⊢ y = A → M ⁡ T ⁡ y = M ⁡ T ⁡ A
13 12 eqeq2d ⊢ y = A → M ⁡ T ⁡ A = M ⁡ T ⁡ y ↔ M ⁡ T ⁡ A = M ⁡ T ⁡ A
14 11 13 anbi12d ⊢ y = A → L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y ↔ L ⁡ A ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ A
15 eqid ⊢ M ⁡ T ⁡ A = M ⁡ T ⁡ A
16 15 biantru ⊢ L ⁡ A ≤ 1 ↔ L ⁡ A ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ A
17 14 16 bitr4di ⊢ y = A → L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y ↔ L ⁡ A ≤ 1
18 17 rspcev ⊢ A ∈ X ∧ L ⁡ A ≤ 1 → ∃ y ∈ X L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y
19 fvex ⊢ M ⁡ T ⁡ A ∈ V
20 eqeq1 ⊢ x = M ⁡ T ⁡ A → x = M ⁡ T ⁡ y ↔ M ⁡ T ⁡ A = M ⁡ T ⁡ y
21 20 anbi2d ⊢ x = M ⁡ T ⁡ A → L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ↔ L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y
22 21 rexbidv ⊢ x = M ⁡ T ⁡ A → ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ↔ ∃ y ∈ X L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y
23 19 22 elab ⊢ M ⁡ T ⁡ A ∈ x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ↔ ∃ y ∈ X L ⁡ y ≤ 1 ∧ M ⁡ T ⁡ A = M ⁡ T ⁡ y
24 18 23 sylibr ⊢ A ∈ X ∧ L ⁡ A ≤ 1 → M ⁡ T ⁡ A ∈ x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y
25 supxrub ⊢ x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ⊆ ℝ * ∧ M ⁡ T ⁡ A ∈ x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y → M ⁡ T ⁡ A ≤ sup x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ℝ * <
26 9 24 25 syl2an ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ A ∈ X ∧ L ⁡ A ≤ 1 → M ⁡ T ⁡ A ≤ sup x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ℝ * <
27 1 2 3 4 5 nmooval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ℝ * <
28 27 adantr ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ A ∈ X ∧ L ⁡ A ≤ 1 → N ⁡ T = sup x | ∃ y ∈ X L ⁡ y ≤ 1 ∧ x = M ⁡ T ⁡ y ℝ * <
29 26 28 breqtrrd ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ A ∈ X ∧ L ⁡ A ≤ 1 → M ⁡ T ⁡ A ≤ N ⁡ T