Theorem cnnvg

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

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

Proof

Step	Hyp	Ref	Expression
1		cnnvg.6	|- U = <. <. + , x. >. , abs >.
2		eqid	|- ( +v ` U ) = ( +v ` U )
3	2	vafval	|- ( +v ` U ) = ( 1st ` ( 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	|- ( 1st ` ( 1st ` U ) ) = ( 1st ` <. + , x. >. )
13		addex	|- + e. _V
14		mulex	|- x. e. _V
15	13 14	op1st	|- ( 1st ` <. + , x. >. ) = +
16	3 12 15	3eqtrri	|- + = ( +v ` U )