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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		nmoxr.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
		nmoxr.3	⊢ 𝑁 = ( 𝑈 normOp_OLD 𝑊 )
	Assertion	nmorepnf	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )

Proof

Step	Hyp	Ref	Expression
1		nmoxr.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmoxr.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		nmoxr.3	⊢ 𝑁 = ( 𝑈 normOp_OLD 𝑊 )
4		eqid	⊢ ( norm_CV ‘ 𝑊 ) = ( norm_CV ‘ 𝑊 )
5	2 4	nmosetre	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )
6		eqid	⊢ ( 0_vec ‘ 𝑈 ) = ( 0_vec ‘ 𝑈 )
7		eqid	⊢ ( norm_CV ‘ 𝑈 ) = ( norm_CV ‘ 𝑈 )
8	1 6 7	nmosetn0	⊢ ( 𝑈 ∈ NrmCVec → ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ ( 0_vec ‘ 𝑈 ) ) ) ∈ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } )
9	8	ne0d	⊢ ( 𝑈 ∈ NrmCVec → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ≠ ∅ )
10		supxrre2	⊢ ( ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ ∧ { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ≠ ∅ ) → ( sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ≠ +∞ ) )
11	5 9 10	syl2anr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ) → ( sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ≠ +∞ ) )
12	11	3impb	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ≠ +∞ ) )
13	1 2 7 4 3	nmooval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) )
14	13	eleq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ ) )
15	13	neeq1d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ≠ +∞ ↔ sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ≠ +∞ ) )
16	12 14 15	3bitr4d	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( 𝑁 ‘ 𝑇 ) ≠ +∞ ) )