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

Metamath Proof Explorer

Theorem nmopsetretHIL

Description: The set in the supremum of the operator norm definition df-nmop is a set of reals. (Contributed by NM, 2-Feb-2006) (New usage is discouraged.)

Ref Expression
Assertion nmopsetretHIL ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ

Proof

Step Hyp Ref Expression
1 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
2 1 hhnv ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec
3 df-hba ⊢ ℋ = BaseSet ⁡ + ℎ ⋅ ℎ norm ℎ
4 1 hhnm ⊢ norm ℎ = norm CV ⁡ + ℎ ⋅ ℎ norm ℎ
5 3 4 nmosetre ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec ∧ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ
6 2 5 mpan ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ