Theorem cnnvs

Description: The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnvs.6	|- U = <. <. + , x. >. , abs >.
Assertion	cnnvs	|- x. = ( .sOLD ` U )

Proof

Step	Hyp	Ref	Expression
1		cnnvs.6	|- U = <. <. + , x. >. , abs >.
2		eqid	|- ( .sOLD ` U ) = ( .sOLD ` U )
3	2	smfval	|- ( .sOLD ` U ) = ( 2nd ` ( 1st ` U ) )
4	1	fveq2i	|- ( 1st ` U ) = ( 1st ` <. <. + , x. >. , abs >. )
5		opex	|- <. + , x. >. e. _V
6		absf	|- abs : CC --> RR
7		cnex	|- CC e. _V
8		fex	|- ( ( abs : CC --> RR /\ CC e. _V ) -> abs e. _V )
9	6 7 8	mp2an	|- abs e. _V
10	5 9	op1st	|- ( 1st ` <. <. + , x. >. , abs >. ) = <. + , x. >.
11	4 10	eqtri	|- ( 1st ` U ) = <. + , x. >.
12	11	fveq2i	|- ( 2nd ` ( 1st ` U ) ) = ( 2nd ` <. + , x. >. )
13		addex	|- + e. _V
14		mulex	|- x. e. _V
15	13 14	op2nd	|- ( 2nd ` <. + , x. >. ) = x.
16	3 12 15	3eqtrri	|- x. = ( .sOLD ` U )