This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 \in NrmCVec \to 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 \land U \in NrmCVec) \to U = ⟨1^{st} (U), 2^{nd} (U)⟩$
5	3 4	mpan	$⊢ U \in NrmCVec \to 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 \in NrmCVec \to U = ⟨W, N⟩$