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 ⊢ Y = BaseSet ⁡ W
nmosetre.4 ⊢ N = norm CV ⁡ W
Assertion nmosetre ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X M ⁡ z ≤ 1 ∧ x = N ⁡ T ⁡ z ⊆ ℝ

Proof

Step Hyp Ref Expression
1 nmosetre.2 ⊢ Y = BaseSet ⁡ W
2 nmosetre.4 ⊢ N = norm CV ⁡ W
3 ffvelcdm ⊢ T : X ⟶ Y ∧ z ∈ X → T ⁡ z ∈ Y
4 1 2 nvcl ⊢ W ∈ NrmCVec ∧ T ⁡ z ∈ Y → N ⁡ T ⁡ z ∈ ℝ
5 3 4 sylan2 ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ z ∈ X → N ⁡ T ⁡ z ∈ ℝ
6 5 anassrs ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ z ∈ X → N ⁡ T ⁡ z ∈ ℝ
7 eleq1 ⊢ x = N ⁡ T ⁡ z → x ∈ ℝ ↔ N ⁡ T ⁡ z ∈ ℝ
8 6 7 imbitrrid ⊢ x = N ⁡ T ⁡ z → W ∈ NrmCVec ∧ T : X ⟶ Y ∧ z ∈ X → x ∈ ℝ
9 8 impcom ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ z ∈ X ∧ x = N ⁡ T ⁡ z → x ∈ ℝ
10 9 adantrl ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y ∧ z ∈ X ∧ M ⁡ z ≤ 1 ∧ x = N ⁡ T ⁡ z → x ∈ ℝ
11 10 rexlimdva2 ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → ∃ z ∈ X M ⁡ z ≤ 1 ∧ x = N ⁡ T ⁡ z → x ∈ ℝ
12 11 abssdv ⊢ W ∈ NrmCVec ∧ T : X ⟶ Y → x | ∃ z ∈ X M ⁡ z ≤ 1 ∧ x = N ⁡ T ⁡ z ⊆ ℝ