Theorem 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 = ( 1st ` U )
	nvvop.2	|- G = ( +v ` U )
	nvvop.4	|- S = ( .sOLD ` U )
Assertion	nvvop	|- ( U e. NrmCVec -> W = <. G , S >. )

Proof

Step	Hyp	Ref	Expression
1		nvvop.1	|- W = ( 1st ` U )
2		nvvop.2	|- G = ( +v ` U )
3		nvvop.4	|- S = ( .sOLD ` U )
4		vcrel	|- Rel CVecOLD
5		nvss	|- NrmCVec C_ ( CVecOLD X. _V )
6		eqid	|- ( normCV ` U ) = ( normCV ` U )
7	1 6	nvop2	|- ( U e. NrmCVec -> U = <. W , ( normCV ` U ) >. )
8	7	eleq1d	|- ( U e. NrmCVec -> ( U e. NrmCVec <-> <. W , ( normCV ` U ) >. e. NrmCVec ) )
9	8	ibi	|- ( U e. NrmCVec -> <. W , ( normCV ` U ) >. e. NrmCVec )
10	5 9	sseldi	|- ( U e. NrmCVec -> <. W , ( normCV ` U ) >. e. ( CVecOLD X. _V ) )
11		opelxp1	|- ( <. W , ( normCV ` U ) >. e. ( CVecOLD X. _V ) -> W e. CVecOLD )
12	10 11	syl	|- ( U e. NrmCVec -> W e. CVecOLD )
13		1st2nd	|- ( ( Rel CVecOLD /\ W e. CVecOLD ) -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
14	4 12 13	sylancr	|- ( U e. NrmCVec -> W = <. ( 1st ` W ) , ( 2nd ` W ) >. )
15	2	vafval	|- G = ( 1st ` ( 1st ` U ) )
16	1	fveq2i	|- ( 1st ` W ) = ( 1st ` ( 1st ` U ) )
17	15 16	eqtr4i	|- G = ( 1st ` W )
18	3	smfval	|- S = ( 2nd ` ( 1st ` U ) )
19	1	fveq2i	|- ( 2nd ` W ) = ( 2nd ` ( 1st ` U ) )
20	18 19	eqtr4i	|- S = ( 2nd ` W )
21	17 20	opeq12i	|- <. G , S >. = <. ( 1st ` W ) , ( 2nd ` W ) >.
22	14 21	eqtr4di	|- ( U e. NrmCVec -> W = <. G , S >. )