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

Proof

Step	Hyp	Ref	Expression
1		nvop.2	|- G = ( +v ` U )
2		nvop.4	|- S = ( .sOLD ` U )
3		nvop.6	|- N = ( normCV ` U )
4		nvrel	|- Rel NrmCVec
5		1st2nd	|- ( ( Rel NrmCVec /\ U e. NrmCVec ) -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
6	4 5	mpan	|- ( U e. NrmCVec -> U = <. ( 1st ` U ) , ( 2nd ` U ) >. )
7	3	nmcvfval	|- N = ( 2nd ` U )
8	7	opeq2i	|- <. ( 1st ` U ) , N >. = <. ( 1st ` U ) , ( 2nd ` U ) >.
9		eqid	|- ( 1st ` U ) = ( 1st ` U )
10	9 1 2	nvvop	|- ( U e. NrmCVec -> ( 1st ` U ) = <. G , S >. )
11	10	opeq1d	|- ( U e. NrmCVec -> <. ( 1st ` U ) , N >. = <. <. G , S >. , N >. )
12	8 11	syl5eqr	|- ( U e. NrmCVec -> <. ( 1st ` U ) , ( 2nd ` U ) >. = <. <. G , S >. , N >. )
13	6 12	eqtrd	|- ( U e. NrmCVec -> U = <. <. G , S >. , N >. )