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:A0AxnormTxAnormxnormopTA

Proof

Step Hyp Ref Expression
1 df-hba =BaseSet+norm
2 eqid +norm=+norm
3 2 hhnm norm=normCV+norm
4 eqid +normnormOpOLD+norm=+normnormOpOLD+norm
5 2 4 hhnmoi normop=+normnormOpOLD+norm
6 2 hhnv +normNrmCVec
7 1 1 3 3 5 6 6 nmoub2i T:A0AxnormTxAnormxnormopTA