Theorem cnnvba

Description: The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	cnnvba.6	|- U = <. <. + , x. >. , abs >.
Assertion	cnnvba	|- CC = ( BaseSet ` U )

Proof

Step	Hyp	Ref	Expression
1		cnnvba.6	|- U = <. <. + , x. >. , abs >.
2	1	cnnvg	|- + = ( +v ` U )
3	2	rneqi	|- ran + = ran ( +v ` U )
4		cnaddabloOLD	|- + e. AbelOp
5		ablogrpo	|- ( + e. AbelOp -> + e. GrpOp )
6	4 5	ax-mp	|- + e. GrpOp
7		ax-addf	|- + : ( CC X. CC ) --> CC
8	7	fdmi	|- dom + = ( CC X. CC )
9	6 8	grporn	|- CC = ran +
10		eqid	|- ( BaseSet ` U ) = ( BaseSet ` U )
11		eqid	|- ( +v ` U ) = ( +v ` U )
12	10 11	bafval	|- ( BaseSet ` U ) = ran ( +v ` U )
13	3 9 12	3eqtr4i	|- CC = ( BaseSet ` U )