Metamath Proof Explorer


Theorem nvop2

Description: A normed complex vector space is an ordered pair of a vector space and a norm operation. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses nvop2.1 W=1stU
nvop2.6 N=normCVU
Assertion nvop2 UNrmCVecU=WN

Proof

Step Hyp Ref Expression
1 nvop2.1 W=1stU
2 nvop2.6 N=normCVU
3 nvrel RelNrmCVec
4 1st2nd RelNrmCVecUNrmCVecU=1stU2ndU
5 3 4 mpan UNrmCVecU=1stU2ndU
6 2 nmcvfval N=2ndU
7 1 6 opeq12i WN=1stU2ndU
8 5 7 eqtr4di UNrmCVecU=WN