Theorem nmosetre

Description: The set in the supremum of the operator norm definition df-nmoo is a set of reals. (Contributed by NM, 13-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nmosetre.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
	nmosetre.4	⊢ 𝑁 = ( normCV ‘ 𝑊 )
Assertion	nmosetre	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝑀 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		nmosetre.2	⊢ 𝑌 = ( BaseSet ‘ 𝑊 )
2		nmosetre.4	⊢ 𝑁 = ( normCV ‘ 𝑊 )
3		ffvelcdm	⊢ ( ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑇 ‘ 𝑧 ) ∈ 𝑌 )
4	1 2	nvcl	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 ‘ 𝑧 ) ∈ 𝑌 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
5	3 4	sylan2	⊢ ( ( 𝑊 ∈ NrmCVec ∧ ( 𝑇 : 𝑋 ⟶ 𝑌 ∧ 𝑧 ∈ 𝑋 ) ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
6	5	anassrs	⊢ ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ )
7		eleq1	⊢ ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) → ( 𝑥 ∈ ℝ ↔ ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ∈ ℝ ) )
8	6 7	imbitrrid	⊢ ( 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) → ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) → 𝑥 ∈ ℝ ) )
9	8	impcom	⊢ ( ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) → 𝑥 ∈ ℝ )
10	9	adantrl	⊢ ( ( ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) ∧ 𝑧 ∈ 𝑋 ) ∧ ( ( 𝑀 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) ) → 𝑥 ∈ ℝ )
11	10	rexlimdva2	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → ( ∃ 𝑧 ∈ 𝑋 ( ( 𝑀 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) → 𝑥 ∈ ℝ ) )
12	11	abssdv	⊢ ( ( 𝑊 ∈ NrmCVec ∧ 𝑇 : 𝑋 ⟶ 𝑌 ) → { 𝑥 ∣ ∃ 𝑧 ∈ 𝑋 ( ( 𝑀 ‘ 𝑧 ) ≤ 1 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )