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ℎ ‘ ( 𝑇 ‘ 𝑦 ) ) ) } ⊆ ℝ )