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 ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( normℎ ‘ 𝑥 ) ) ) → ( normop ‘ 𝑇 ) ≤ 𝐴 )

Proof

Step Hyp Ref Expression
1 df-hba ⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
2 eqid ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
3 2 hhnm ⊢ normℎ = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4 eqid ⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
5 2 4 hhnmoi ⊢ normop = ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ normOpOLD ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
6 2 hhnv ⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
7 1 1 3 3 5 6 6 nmoub2i ⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ∀ 𝑥 ∈ ℋ ( normℎ ‘ ( 𝑇 ‘ 𝑥 ) ) ≤ ( 𝐴 · ( normℎ ‘ 𝑥 ) ) ) → ( normop ‘ 𝑇 ) ≤ 𝐴 )