Metamath Proof Explorer


Theorem nmoxr

Description: The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nmoxr.1 X=BaseSetU
nmoxr.2 Y=BaseSetW
nmoxr.3 N=UnormOpOLDW
Assertion nmoxr UNrmCVecWNrmCVecT:XYNT*

Proof

Step Hyp Ref Expression
1 nmoxr.1 X=BaseSetU
2 nmoxr.2 Y=BaseSetW
3 nmoxr.3 N=UnormOpOLDW
4 eqid normCVU=normCVU
5 eqid normCVW=normCVW
6 1 2 4 5 3 nmooval UNrmCVecWNrmCVecT:XYNT=supx|zXnormCVUz1x=normCVWTz*<
7 2 5 nmosetre WNrmCVecT:XYx|zXnormCVUz1x=normCVWTz
8 ressxr *
9 7 8 sstrdi WNrmCVecT:XYx|zXnormCVUz1x=normCVWTz*
10 supxrcl x|zXnormCVUz1x=normCVWTz*supx|zXnormCVUz1x=normCVWTz*<*
11 9 10 syl WNrmCVecT:XYsupx|zXnormCVUz1x=normCVWTz*<*
12 11 3adant1 UNrmCVecWNrmCVecT:XYsupx|zXnormCVUz1x=normCVWTz*<*
13 6 12 eqeltrd UNrmCVecWNrmCVecT:XYNT*