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}\left(U\right)$$
	nvop2.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvop2	$$⊢U\in \mathrm{NrmCVec}\to U=⟨W,N⟩$$

Proof

Step	Hyp	Ref	Expression
1		nvop2.1	$$⊢W=1^{st}\left(U\right)$$
2		nvop2.6	$$⊢N={norm}_{CV}\left(U\right)$$
3		nvrel	$$⊢\mathrm{Rel}\mathrm{NrmCVec}$$
4		1st2nd	$$⊢\left(\mathrm{Rel}\mathrm{NrmCVec}\wedge U\in \mathrm{NrmCVec}\right)\to U=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
5	3 4	mpan	$$⊢U\in \mathrm{NrmCVec}\to U=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
6	2	nmcvfval	$$⊢N=2^{nd}\left(U\right)$$
7	1 6	opeq12i	$$⊢⟨W,N⟩=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
8	5 7	eqtr4di	$$⊢U\in \mathrm{NrmCVec}\to U=⟨W,N⟩$$