nvvop

Description: The vector space component of a normed complex vector space is an ordered pair of the underlying group and a scalar product. (Contributed by NM, 28-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvvop.1	$⊢ W = 1^{st} (U)$
	nvvop.2	$⊢ G = +_{v} (U)$
	nvvop.4	$⊢ S = \cdot_{𝑠OLD} (U)$
Assertion	nvvop	$⊢ U \in NrmCVec \to W = ⟨G, S⟩$

Proof

Step	Hyp	Ref	Expression
1		nvvop.1	$⊢ W = 1^{st} (U)$
2		nvvop.2	$⊢ G = +_{v} (U)$
3		nvvop.4	$⊢ S = \cdot_{𝑠OLD} (U)$
4		vcrel	$⊢ Rel {CVec}_{OLD}$
5		nvss	$⊢ NrmCVec \subseteq {CVec}_{OLD} \times V$
6		eqid	$⊢ {norm}_{CV} (U) = {norm}_{CV} (U)$
7	1 6	nvop2	$⊢ U \in NrmCVec \to U = ⟨W, {norm}_{CV} (U)⟩$
8	7	eleq1d	$⊢ U \in NrmCVec \to (U \in NrmCVec \leftrightarrow ⟨W, {norm}_{CV} (U)⟩ \in NrmCVec)$
9	8	ibi	$⊢ U \in NrmCVec \to ⟨W, {norm}_{CV} (U)⟩ \in NrmCVec$
10	5 9	sseldi	$⊢ U \in NrmCVec \to ⟨W, {norm}_{CV} (U)⟩ \in ({CVec}_{OLD} \times V)$
11		opelxp1	$⊢ ⟨W, {norm}_{CV} (U)⟩ \in ({CVec}_{OLD} \times V) \to W \in {CVec}_{OLD}$
12	10 11	syl	$⊢ U \in NrmCVec \to W \in {CVec}_{OLD}$
13		1st2nd	$⊢ (Rel {CVec}_{OLD} \land W \in {CVec}_{OLD}) \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
14	4 12 13	sylancr	$⊢ U \in NrmCVec \to W = ⟨1^{st} (W), 2^{nd} (W)⟩$
15	2	vafval	$⊢ G = 1^{st} (1^{st} (U))$
16	1	fveq2i	$⊢ 1^{st} (W) = 1^{st} (1^{st} (U))$
17	15 16	eqtr4i	$⊢ G = 1^{st} (W)$
18	3	smfval	$⊢ S = 2^{nd} (1^{st} (U))$
19	1	fveq2i	$⊢ 2^{nd} (W) = 2^{nd} (1^{st} (U))$
20	18 19	eqtr4i	$⊢ S = 2^{nd} (W)$
21	17 20	opeq12i	$⊢ ⟨G, S⟩ = ⟨1^{st} (W), 2^{nd} (W)⟩$
22	14 21	eqtr4di	$⊢ U \in NrmCVec \to W = ⟨G, S⟩$

Metamath Proof Explorer

Theorem nvvop

Proof