Theorem nmblore

Description: The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmblore.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nmblore.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmblore.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
	nmblore.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
Assertion	nmblore	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		nmblore.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nmblore.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
3		nmblore.3	⊢ 𝑁 = ( 𝑈 normOpOLD 𝑊 )
4		nmblore.5	⊢ 𝐵 = ( 𝑈 BLnOp 𝑊 )
5	1 2 4	blof	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → 𝑇 : 𝑋 ⟶ 𝑌 )
6	1 2 3	nmogtmnf	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → -∞ < ( 𝑁 ‘ 𝑇 ) )
7	5 6	syld3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → -∞ < ( 𝑁 ‘ 𝑇 ) )
8		eqid	⊢ ( 𝑈 LnOp 𝑊 ) = ( 𝑈 LnOp 𝑊 )
9	3 8 4	isblo	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ∈ 𝐵 ↔ ( 𝑇 ∈ ( 𝑈 LnOp 𝑊 ) ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )
10	9	simplbda	⊢ ( ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ) ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) < +∞ )
11	10	3impa	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) < +∞ )
12	1 2 3	nmoxr	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
13	5 12	syld3an3	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ* )
14		xrrebnd	⊢ ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ* → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( -∞ < ( 𝑁 ‘ 𝑇 ) ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )
15	13 14	syl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( ( 𝑁 ‘ 𝑇 ) ∈ ℝ ↔ ( -∞ < ( 𝑁 ‘ 𝑇 ) ∧ ( 𝑁 ‘ 𝑇 ) < +∞ ) ) )
16	7 11 15	mpbir2and	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵 ) → ( 𝑁 ‘ 𝑇 ) ∈ ℝ )