Theorem phop

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

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

Proof

Step	Hyp	Ref	Expression
1		phop.2	$$⊢G={+}_v\left(U\right)$$
2		phop.4	$$⊢S={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
3		phop.6	$$⊢N={norm}_{CV}\left(U\right)$$
4		phrel	$$⊢\mathrm{Rel}{CPreHil}_{\mathrm{OLD}}$$
5		1st2nd	$$⊢\left(\mathrm{Rel}{CPreHil}_{\mathrm{OLD}}\wedge U\in {CPreHil}_{\mathrm{OLD}}\right)\to U=⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩$$
6	4 5	mpan	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\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		phnv	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to U\in \mathrm{NrmCVec}$$
10		eqid	$$⊢1^{st}\left(U\right)=1^{st}\left(U\right)$$
11	10	nvvc	$$⊢U\in \mathrm{NrmCVec}\to 1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}$$
12		vcrel	$$⊢\mathrm{Rel}{CVec}_{\mathrm{OLD}}$$
13		1st2nd	$$⊢\left(\mathrm{Rel}{CVec}_{\mathrm{OLD}}\wedge 1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}\right)\to 1^{st}\left(U\right)=⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩$$
14	12 13	mpan	$$⊢1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}\to 1^{st}\left(U\right)=⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩$$
15	1	vafval	$$⊢G=1^{st}\left(1^{st}\left(U\right)\right)$$
16	2	smfval	$$⊢S=2^{nd}\left(1^{st}\left(U\right)\right)$$
17	15 16	opeq12i	$$⊢⟨G,S⟩=⟨1^{st}\left(1^{st}\left(U\right)\right),2^{nd}\left(1^{st}\left(U\right)\right)⟩$$
18	14 17	eqtr4di	$$⊢1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}\to 1^{st}\left(U\right)=⟨G,S⟩$$
19	9 11 18	3syl	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to 1^{st}\left(U\right)=⟨G,S⟩$$
20	19	opeq1d	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to ⟨1^{st}\left(U\right),N⟩=⟨⟨G,S⟩,N⟩$$
21	8 20	syl5eqr	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to ⟨1^{st}\left(U\right),2^{nd}\left(U\right)⟩=⟨⟨G,S⟩,N⟩$$
22	6 21	eqtrd	$$⊢U\in {CPreHil}_{\mathrm{OLD}}\to U=⟨⟨G,S⟩,N⟩$$