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 = 1 st U
nvop2.6 N = norm CV U
Assertion nvop2 U NrmCVec U = W N

Proof

Step Hyp Ref Expression
1 nvop2.1 W = 1 st U
2 nvop2.6 N = norm CV U
3 nvrel Rel NrmCVec
4 1st2nd Rel NrmCVec U NrmCVec U = 1 st U 2 nd U
5 3 4 mpan U NrmCVec U = 1 st U 2 nd U
6 2 nmcvfval N = 2 nd U
7 1 6 opeq12i W N = 1 st U 2 nd U
8 5 7 eqtr4di U NrmCVec U = W N