Metamath Proof Explorer

Theorem nmorepnf

Description: The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 ⊢X=BaseSet⁡U
nmoxr.2 ⊢Y=BaseSet⁡W
nmoxr.3 ⊢N=UnormOpOLDW
Assertion nmorepnf ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T∈ℝ↔N⁡T≠+∞

Proof

Step Hyp Ref Expression
1 nmoxr.1 ⊢X=BaseSet⁡U
2 nmoxr.2 ⊢Y=BaseSet⁡W
3 nmoxr.3 ⊢N=UnormOpOLDW
4 eqid ⊢normCV⁡W=normCV⁡W
5 2 4 nmosetre ⊢W∈NrmCVec∧T:X⟶Y→x|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡z⊆ℝ
6 eqid ⊢0vec⁡U=0vec⁡U
7 eqid ⊢normCV⁡U=normCV⁡U
8 1 6 7 nmosetn0 ⊢U∈NrmCVec→normCV⁡W⁡T⁡0vec⁡U∈x|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡z
9 8 ne0d ⊢U∈NrmCVec→x|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡z≠∅
10 supxrre2 ⊢x|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡z⊆ℝ∧x|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡z≠∅→supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<∈ℝ↔supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<≠+∞
11 5 9 10 syl2anr ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<∈ℝ↔supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<≠+∞
12 11 3impb ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<∈ℝ↔supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<≠+∞
13 1 2 7 4 3 nmooval ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T=supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<
14 13 eleq1d ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T∈ℝ↔supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<∈ℝ
15 13 neeq1d ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T≠+∞↔supx|∃z∈XnormCV⁡U⁡z≤1∧x=normCV⁡W⁡T⁡zℝ*<≠+∞
16 12 14 15 3bitr4d ⊢U∈NrmCVec∧W∈NrmCVec∧T:X⟶Y→N⁡T∈ℝ↔N⁡T≠+∞