Theorem nvop

Description: A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvop.2	$$⊢G={+}_v\left(U\right)$$
	nvop.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	nvop.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvop	$$⊢U\in \mathrm{NrmCVec}\to U=⟨⟨G,S⟩,N⟩$$

Proof

Step	Hyp	Ref	Expression
1		nvop.2	$$⊢G={+}_v\left(U\right)$$
2		nvop.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		nvop.6	$$⊢N={norm}_{CV}\left(U\right)$$
4		nvrel	$$⊢\mathrm{Rel}\mathrm{NrmCVec}$$
5		1st2nd	$$⊢\left(\mathrm{Rel}\mathrm{NrmCVec}\wedge U\in \mathrm{NrmCVec}\right)\to U=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
6	4 5	mpan	$$⊢U\in \mathrm{NrmCVec}\to U=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
7	3	nmcvfval	$$⊢N=2^{nd}\left(U\right)$$
8	7	opeq2i	$$⊢⟨1^{st}\left(U\right),N⟩=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
9		eqid	$$⊢1^{st}\left(U\right)=1^{st}\left(U\right)$$
10	9 1 2	nvvop	$$⊢U\in \mathrm{NrmCVec}\to 1^{st}\left(U\right)=⟨G,S⟩$$
11	10	opeq1d	$$⊢U\in \mathrm{NrmCVec}\to ⟨1^{st}\left(U\right),N⟩=⟨⟨G,S⟩,N⟩$$
12	8 11	syl5eqr	$$⊢U\in \mathrm{NrmCVec}\to ⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩=⟨⟨G,S⟩,N⟩$$
13	6 12	eqtrd	$$⊢U\in \mathrm{NrmCVec}\to U=⟨⟨G,S⟩,N⟩$$