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 ` U )
	phop.4	|- S = ( .sOLD ` U )
	phop.6	|- N = ( normCV ` U )
Assertion	phop	|- ( U e. CPreHilOLD -> U = <. <. G , S >. , N >. )

Proof

Step	Hyp	Ref	Expression
1		phop.2	|- G = ( +v ` U )
2		phop.4	|- S = ( .sOLD ` U )
3		phop.6	|- N = ( normCV ` U )
4		phrel	|- Rel CPreHilOLD
5		1st2nd	|- ( ( Rel CPreHilOLD /\ U e. CPreHilOLD ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
6	4 5	mpan	|- ( U e. CPreHilOLD -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
7	3	nmcvfval	|- N = ( 2nd ` U )
8	7	opeq2i	|- <. ( 1st ` U ) , N >. = <. ( 1st ` U ) , ( 2nd ` U ) >.
9		phnv	|- ( U e. CPreHilOLD -> U e. NrmCVec )
10		eqid	|- ( 1st ` U ) = ( 1st ` U )
11	10	nvvc	|- ( U e. NrmCVec -> ( 1st ` U ) e. CVecOLD )
12		vcrel	|- Rel CVecOLD
13		1st2nd	|- ( ( Rel CVecOLD /\ ( 1st ` U ) e. CVecOLD ) -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
14	12 13	mpan	|- ( ( 1st ` U ) e. CVecOLD -> ( 1st ` U ) = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >. )
15	1	vafval	|- G = ( 1st ` ( 1st ` U ) )
16	2	smfval	|- S = ( 2nd ` ( 1st ` U ) )
17	15 16	opeq12i	|- <. G , S >. = <. ( 1st ` ( 1st ` U ) ) , ( 2nd ` ( 1st ` U ) ) >.
18	14 17	eqtr4di	|- ( ( 1st ` U ) e. CVecOLD -> ( 1st ` U ) = <. G , S >. )
19	9 11 18	3syl	|- ( U e. CPreHilOLD -> ( 1st ` U ) = <. G , S >. )
20	19	opeq1d	|- ( U e. CPreHilOLD -> <. ( 1st ` U ) , N >. = <. <. G , S >. , N >. )
21	8 20	syl5eqr	|- ( U e. CPreHilOLD -> <. ( 1st ` U ) , ( 2nd ` U ) >. = <. <. G , S >. , N >. )
22	6 21	eqtrd	|- ( U e. CPreHilOLD -> U = <. <. G , S >. , N >. )