This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ∧ 𝑥 = ( 𝑁 ‘ ( 𝑇 ‘ 𝑧 ) ) ) } ⊆ ℝ )