Metamath Proof Explorer

Theorem nmoxr

Description: The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypotheses	nmoxr.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
		nmoxr.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
		nmoxr.3	⊢ 𝑁 = ( 𝑈 normOp_OLD 𝑊 )
	Assertion	nmoxr	⊢ ( ( 𝑈 ∈ 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		eqid	⊢ ( norm_CV ‘ 𝑊 ) = ( norm_CV ‘ 𝑊 )
6	1 2 4 5 3	nmooval	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) = sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) )
7	2 5	nmosetre	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )
8		ressxr	⊢ ℝ ⊆ ℝ^*
9	7 8	sstrdi	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ^* )
10		supxrcl	⊢ ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ^* → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ^* )
11	9 10	syl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ^* )
12	11	3adant1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → sup ( { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( ( norm_CV ‘ 𝑈 ) ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( ( norm_CV ‘ 𝑊 ) ‘ ( 𝑇 ‘ 𝑧 ) ) ) } , ℝ^* , < ) ∈ ℝ^* )
13	6 12	eqeltrd	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ^* )