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

Metamath Proof Explorer

Theorem nmopsetretALT

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.) (Proof modification is discouraged.)

Ref Expression
Assertion nmopsetretALT ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( 𝑇 ‘ 𝑦 ) ∈ ℋ )
2 normcl ⊢ ( ( 𝑇 ‘ 𝑦 ) ∈ ℋ → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
3 1 2 syl ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ )
4 eleq1 ⊢ ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) → ( 𝑥 ∈ ℝ ↔ ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ∈ ℝ ) )
5 3 4 imbitrrid ⊢ ( 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) → ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) → 𝑥 ∈ ℝ ) )
6 5 impcom ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ )
7 6 adantrl ⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑦 ∈ ℋ ) ∧ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) ) → 𝑥 ∈ ℝ )
8 7 exp31 ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( 𝑦 ∈ ℋ → ( ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ ) ) )
9 8 rexlimdv ⊢ ( 𝑇 : ℋ ⟶ ℋ → ( ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ ) )
10 9 abssdv ⊢ ( 𝑇 : ℋ ⟶ ℋ → { 𝑥 ∣ ∃ 𝑦 ∈ ℋ ( ( normℎ ‘ 𝑦 ) ≤ 1 ∧ 𝑥 = ( normℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )