Metamath Proof Explorer


Theorem nmooge0

Description: The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nmoxr.1 X=BaseSetU
2 nmoxr.2 Y=BaseSetW
3 nmoxr.3 N=UnormOpOLDW
4 0xr 0*
5 4 a1i UNrmCVecWNrmCVecT:XY0*
6 simp2 UNrmCVecWNrmCVecT:XYWNrmCVec
7 eqid 0vecU=0vecU
8 1 7 nvzcl UNrmCVec0vecUX
9 ffvelrn T:XY0vecUXT0vecUY
10 8 9 sylan2 T:XYUNrmCVecT0vecUY
11 10 ancoms UNrmCVecT:XYT0vecUY
12 11 3adant2 UNrmCVecWNrmCVecT:XYT0vecUY
13 eqid normCVW=normCVW
14 2 13 nvcl WNrmCVecT0vecUYnormCVWT0vecU
15 6 12 14 syl2anc UNrmCVecWNrmCVecT:XYnormCVWT0vecU
16 15 rexrd UNrmCVecWNrmCVecT:XYnormCVWT0vecU*
17 1 2 3 nmoxr UNrmCVecWNrmCVecT:XYNT*
18 2 13 nvge0 WNrmCVecT0vecUY0normCVWT0vecU
19 6 12 18 syl2anc UNrmCVecWNrmCVecT:XY0normCVWT0vecU
20 2 13 nmosetre WNrmCVecT:XYx|zXnormCVUz1x=normCVWTz
21 ressxr *
22 20 21 sstrdi WNrmCVecT:XYx|zXnormCVUz1x=normCVWTz*
23 eqid normCVU=normCVU
24 1 7 23 nmosetn0 UNrmCVecnormCVWT0vecUx|zXnormCVUz1x=normCVWTz
25 supxrub x|zXnormCVUz1x=normCVWTz*normCVWT0vecUx|zXnormCVUz1x=normCVWTznormCVWT0vecUsupx|zXnormCVUz1x=normCVWTz*<
26 22 24 25 syl2an WNrmCVecT:XYUNrmCVecnormCVWT0vecUsupx|zXnormCVUz1x=normCVWTz*<
27 26 3impa WNrmCVecT:XYUNrmCVecnormCVWT0vecUsupx|zXnormCVUz1x=normCVWTz*<
28 27 3comr UNrmCVecWNrmCVecT:XYnormCVWT0vecUsupx|zXnormCVUz1x=normCVWTz*<
29 1 2 23 13 3 nmooval UNrmCVecWNrmCVecT:XYNT=supx|zXnormCVUz1x=normCVWTz*<
30 28 29 breqtrrd UNrmCVecWNrmCVecT:XYnormCVWT0vecUNT
31 5 16 17 19 30 xrletrd UNrmCVecWNrmCVecT:XY0NT