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=normCV⁡U
nmoubi.m ⊢M=normCV⁡W
nmoubi.3 ⊢N=UnormOpOLDW
nmoubi.u ⊢U∈NrmCVec
nmoubi.w ⊢W∈NrmCVec
Assertion nmoubi ⊢T:X⟶Y∧A∈ℝ*→N⁡T≤A↔∀x∈XL⁡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=normCV⁡U
4 nmoubi.m ⊢M=normCV⁡W
5 nmoubi.3 ⊢N=UnormOpOLDW
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=supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<
9 6 7 8 mp3an12 ⊢T:X⟶Y→N⁡T=supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<
10 9 breq1d ⊢T:X⟶Y→N⁡T≤A↔supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<≤A
11 10 adantr ⊢T:X⟶Y∧A∈ℝ*→N⁡T≤A↔supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<≤A
12 2 4 nmosetre ⊢W∈NrmCVec∧T:X⟶Y→y|∃x∈XL⁡x≤1∧y=M⁡T⁡x⊆ℝ
13 7 12 mpan ⊢T:X⟶Y→y|∃x∈XL⁡x≤1∧y=M⁡T⁡x⊆ℝ
14 ressxr ⊢ℝ⊆ℝ*
15 13 14 sstrdi ⊢T:X⟶Y→y|∃x∈XL⁡x≤1∧y=M⁡T⁡x⊆ℝ*
16 supxrleub ⊢y|∃x∈XL⁡x≤1∧y=M⁡T⁡x⊆ℝ*∧A∈ℝ*→supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<≤A↔∀z∈y|∃x∈XL⁡x≤1∧y=M⁡T⁡xz≤A
17 15 16 sylan ⊢T:X⟶Y∧A∈ℝ*→supy|∃x∈XL⁡x≤1∧y=M⁡T⁡xℝ*<≤A↔∀z∈y|∃x∈XL⁡x≤1∧y=M⁡T⁡xz≤A
18 11 17 bitrd ⊢T:X⟶Y∧A∈ℝ*→N⁡T≤A↔∀z∈y|∃x∈XL⁡x≤1∧y=M⁡T⁡xz≤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∈XL⁡x≤1∧y=M⁡T⁡x↔∃x∈XL⁡x≤1∧z=M⁡T⁡x
22 21 ralab ⊢∀z∈y|∃x∈XL⁡x≤1∧y=M⁡T⁡xz≤A↔∀z∃x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A
23 ralcom4 ⊢∀x∈X∀zL⁡x≤1∧z=M⁡T⁡x→z≤A↔∀z∀x∈XL⁡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 ⊢∀zL⁡x≤1∧z=M⁡T⁡x→z≤A↔∀zz=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 ⊢∀zz=M⁡T⁡x→L⁡x≤1→z≤A↔L⁡x≤1→M⁡T⁡x≤A
32 27 31 bitri ⊢∀zL⁡x≤1∧z=M⁡T⁡x→z≤A↔L⁡x≤1→M⁡T⁡x≤A
33 32 ralbii ⊢∀x∈X∀zL⁡x≤1∧z=M⁡T⁡x→z≤A↔∀x∈XL⁡x≤1→M⁡T⁡x≤A
34 r19.23v ⊢∀x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A↔∃x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A
35 34 albii ⊢∀z∀x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A↔∀z∃x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A
36 23 33 35 3bitr3i ⊢∀x∈XL⁡x≤1→M⁡T⁡x≤A↔∀z∃x∈XL⁡x≤1∧z=M⁡T⁡x→z≤A
37 22 36 bitr4i ⊢∀z∈y|∃x∈XL⁡x≤1∧y=M⁡T⁡xz≤A↔∀x∈XL⁡x≤1→M⁡T⁡x≤A
38 18 37 bitrdi ⊢T:X⟶Y∧A∈ℝ*→N⁡T≤A↔∀x∈XL⁡x≤1→M⁡T⁡x≤A