This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )