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 ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → T ⁡ y ∈ ℋ
2 normcl ⊢ T ⁡ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ∈ ℝ
3 1 2 syl ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ → norm ℎ ⁡ T ⁡ y ∈ ℝ
4 eleq1 ⊢ x = norm ℎ ⁡ T ⁡ y → x ∈ ℝ ↔ norm ℎ ⁡ T ⁡ y ∈ ℝ
5 3 4 imbitrrid ⊢ x = norm ℎ ⁡ T ⁡ y → T : ℋ ⟶ ℋ ∧ y ∈ ℋ → x ∈ ℝ
6 5 impcom ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ ∧ x = norm ℎ ⁡ T ⁡ y → x ∈ ℝ
7 6 adantrl ⊢ T : ℋ ⟶ ℋ ∧ y ∈ ℋ ∧ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y → x ∈ ℝ
8 7 exp31 ⊢ T : ℋ ⟶ ℋ → y ∈ ℋ → norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y → x ∈ ℝ
9 8 rexlimdv ⊢ T : ℋ ⟶ ℋ → ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y → x ∈ ℝ
10 9 abssdv ⊢ T : ℋ ⟶ ℋ → x | ∃ y ∈ ℋ norm ℎ ⁡ y ≤ 1 ∧ x = norm ℎ ⁡ T ⁡ y ⊆ ℝ