Metamath Proof Explorer

Theorem nmoubi

Description: An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoubi.1 ⊢ X = BaseSet ⁡ U
nmoubi.y ⊢ Y = BaseSet ⁡ W
nmoubi.l ⊢ L = norm CV ⁡ U
nmoubi.m ⊢ M = norm CV ⁡ W
nmoubi.3 ⊢ N = U normOp OLD W
nmoubi.u ⊢ U ∈ NrmCVec
nmoubi.w ⊢ W ∈ NrmCVec
Assertion nmoubi ⊢ T : X ⟶ Y ∧ A ∈ ℝ * → N ⁡ T ≤ A ↔ ∀ x ∈ X L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A

Proof

Step Hyp Ref Expression
1 nmoubi.1 ⊢ X = BaseSet ⁡ U
2 nmoubi.y ⊢ Y = BaseSet ⁡ W
3 nmoubi.l ⊢ L = norm CV ⁡ U
4 nmoubi.m ⊢ M = norm CV ⁡ W
5 nmoubi.3 ⊢ N = U normOp OLD W
6 nmoubi.u ⊢ U ∈ NrmCVec
7 nmoubi.w ⊢ W ∈ NrmCVec
8 1 2 3 4 5 nmooval ⊢ U ∈ NrmCVec ∧ W ∈ NrmCVec ∧ T : X ⟶ Y → N ⁡ T = sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * <
9 6 7 8 mp3an12 ⊢ T : X ⟶ Y → N ⁡ T = sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * <
10 9 breq1d ⊢ T : X ⟶ Y → N ⁡ T ≤ A ↔ sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * < ≤ A
11 10 adantr ⊢ T : X ⟶ Y ∧ A ∈ ℝ * → N ⁡ T ≤ A ↔ sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * < ≤ A
12 2 4 nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ⊆ ℝ
13 7 12 mpan ⊢ T : X ⟶ Y → y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ⊆ ℝ
14 ressxr ⊢ ℝ ⊆ ℝ *
15 13 14 sstrdi ⊢ T : X ⟶ Y → y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ⊆ ℝ *
16 supxrleub ⊢ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ⊆ ℝ * ∧ A ∈ ℝ * → sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * < ≤ A ↔ ∀ z ∈ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x z ≤ A
17 15 16 sylan ⊢ T : X ⟶ Y ∧ A ∈ ℝ * → sup y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ℝ * < ≤ A ↔ ∀ z ∈ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x z ≤ A
18 11 17 bitrd ⊢ T : X ⟶ Y ∧ A ∈ ℝ * → N ⁡ T ≤ A ↔ ∀ z ∈ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x z ≤ A
19 eqeq1 ⊢ y = z → y = M ⁡ T ⁡ x ↔ z = M ⁡ T ⁡ x
20 19 anbi2d ⊢ y = z → L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ↔ L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x
21 20 rexbidv ⊢ y = z → ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x ↔ ∃ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x
22 21 ralab ⊢ ∀ z ∈ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x z ≤ A ↔ ∀ z ∃ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A
23 ralcom4 ⊢ ∀ x ∈ X ∀ z L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ ∀ z ∀ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A
24 ancomst ⊢ L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ z = M ⁡ T ⁡ x ∧ L ⁡ x ≤ 1 → z ≤ A
25 impexp ⊢ z = M ⁡ T ⁡ x ∧ L ⁡ x ≤ 1 → z ≤ A ↔ z = M ⁡ T ⁡ x → L ⁡ x ≤ 1 → z ≤ A
26 24 25 bitri ⊢ L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ z = M ⁡ T ⁡ x → L ⁡ x ≤ 1 → z ≤ A
27 26 albii ⊢ ∀ z L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ ∀ z z = M ⁡ T ⁡ x → L ⁡ x ≤ 1 → z ≤ A
28 fvex ⊢ M ⁡ T ⁡ x ∈ V
29 breq1 ⊢ z = M ⁡ T ⁡ x → z ≤ A ↔ M ⁡ T ⁡ x ≤ A
30 29 imbi2d ⊢ z = M ⁡ T ⁡ x → L ⁡ x ≤ 1 → z ≤ A ↔ L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A
31 28 30 ceqsalv ⊢ ∀ z z = M ⁡ T ⁡ x → L ⁡ x ≤ 1 → z ≤ A ↔ L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A
32 27 31 bitri ⊢ ∀ z L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A
33 32 ralbii ⊢ ∀ x ∈ X ∀ z L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ ∀ x ∈ X L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A
34 r19.23v ⊢ ∀ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ ∃ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A
35 34 albii ⊢ ∀ z ∀ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A ↔ ∀ z ∃ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A
36 23 33 35 3bitr3i ⊢ ∀ x ∈ X L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A ↔ ∀ z ∃ x ∈ X L ⁡ x ≤ 1 ∧ z = M ⁡ T ⁡ x → z ≤ A
37 22 36 bitr4i ⊢ ∀ z ∈ y | ∃ x ∈ X L ⁡ x ≤ 1 ∧ y = M ⁡ T ⁡ x z ≤ A ↔ ∀ x ∈ X L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A
38 18 37 syl6bb ⊢ T : X ⟶ Y ∧ A ∈ ℝ * → N ⁡ T ≤ A ↔ ∀ x ∈ X L ⁡ x ≤ 1 → M ⁡ T ⁡ x ≤ A