Theorem nmoleub2a

Description: The operator norm is the supremum of the value of a linear operator in the closed unit ball. (Contributed by Mario Carneiro, 19-Oct-2015)

	Ref	Expression
Hypotheses	nmoleub2.n	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
	nmoleub2.v	⊢ 𝑉 = ( Base ‘ 𝑆 )
	nmoleub2.l	⊢ 𝐿 = ( norm ‘ 𝑆 )
	nmoleub2.m	⊢ 𝑀 = ( norm ‘ 𝑇 )
	nmoleub2.g	⊢ 𝐺 = ( Scalar ‘ 𝑆 )
	nmoleub2.w	⊢ 𝐾 = ( Base ‘ 𝐺 )
	nmoleub2.s	⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
	nmoleub2.t	⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
	nmoleub2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
	nmoleub2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
	nmoleub2.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
	nmoleub2a.5	⊢ ( 𝜑 → ℚ ⊆ 𝐾 )
Assertion	nmoleub2a	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmoleub2.n	⊢ 𝑁 = ( 𝑆 normOp 𝑇 )
2		nmoleub2.v	⊢ 𝑉 = ( Base ‘ 𝑆 )
3		nmoleub2.l	⊢ 𝐿 = ( norm ‘ 𝑆 )
4		nmoleub2.m	⊢ 𝑀 = ( norm ‘ 𝑇 )
5		nmoleub2.g	⊢ 𝐺 = ( Scalar ‘ 𝑆 )
6		nmoleub2.w	⊢ 𝐾 = ( Base ‘ 𝐺 )
7		nmoleub2.s	⊢ ( 𝜑 → 𝑆 ∈ ( NrmMod ∩ ℂMod ) )
8		nmoleub2.t	⊢ ( 𝜑 → 𝑇 ∈ ( NrmMod ∩ ℂMod ) )
9		nmoleub2.f	⊢ ( 𝜑 → 𝐹 ∈ ( 𝑆 LMHom 𝑇 ) )
10		nmoleub2.a	⊢ ( 𝜑 → 𝐴 ∈ ℝ* )
11		nmoleub2.r	⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
12		nmoleub2a.5	⊢ ( 𝜑 → ℚ ⊆ 𝐾 )
13		idd	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
14		ltle	⊢ ( ( ( 𝐿 ‘ 𝑥 ) ∈ ℝ ∧ 𝑅 ∈ ℝ ) → ( ( 𝐿 ‘ 𝑥 ) < 𝑅 → ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 ) )
15	1 2 3 4 5 6 7 8 9 10 11 12 13 14	nmoleub2lem2	⊢ ( 𝜑 → ( ( 𝑁 ‘ 𝐹 ) ≤ 𝐴 ↔ ∀ 𝑥 ∈ 𝑉 ( ( 𝐿 ‘ 𝑥 ) ≤ 𝑅 → ( ( 𝑀 ‘ ( 𝐹 ‘ 𝑥 ) ) / 𝑅 ) ≤ 𝐴 ) ) )