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 ‘ 𝑇 ) ≤ 𝐴 )