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

Metamath Proof Explorer

Theorem nmopub2tHIL

Description: An upper bound for an operator norm. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

Ref Expression
Assertion nmopub2tHIL ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm op ⁡ T ≤ A

Proof

Step Hyp Ref Expression
1 df-hba ⊢ ℋ = BaseSet ⁡ + ℎ ⋅ ℎ norm ℎ
2 eqid ⊢ + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ
3 2 hhnm ⊢ norm ℎ = norm CV ⁡ + ℎ ⋅ ℎ norm ℎ
4 eqid ⊢ + ℎ ⋅ ℎ norm ℎ normOp OLD + ℎ ⋅ ℎ norm ℎ = + ℎ ⋅ ℎ norm ℎ normOp OLD + ℎ ⋅ ℎ norm ℎ
5 2 4 hhnmoi ⊢ norm op = + ℎ ⋅ ℎ norm ℎ normOp OLD + ℎ ⋅ ℎ norm ℎ
6 2 hhnv ⊢ + ℎ ⋅ ℎ norm ℎ ∈ NrmCVec
7 1 1 3 3 5 6 6 nmoub2i ⊢ T : ℋ ⟶ ℋ ∧ A ∈ ℝ ∧ 0 ≤ A ∧ ∀ x ∈ ℋ norm ℎ ⁡ T ⁡ x ≤ A ⁢ norm ℎ ⁡ x → norm op ⁡ T ≤ A