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	⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2	1	hhnv	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
3		df-hba	⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4	1	hhnm	⊢ normℎ = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
5	3 4	nmosetre	⊢ ( ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec ∧ 𝑇 : ℋ ⟶ ℋ ) → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )
6	2 5	mpan	⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )