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=+×abs
Assertion cnnvba =BaseSetU

Proof

Step Hyp Ref Expression
1 cnnvba.6 U=+×abs
2 1 cnnvg +=+vU
3 2 rneqi ran+=ran+vU
4 cnaddabloOLD +AbelOp
5 ablogrpo +AbelOp+GrpOp
6 4 5 ax-mp +GrpOp
7 ax-addf +:×
8 7 fdmi dom+=×
9 6 8 grporn =ran+
10 eqid BaseSetU=BaseSetU
11 eqid +vU=+vU
12 10 11 bafval BaseSetU=ran+vU
13 3 9 12 3eqtr4i =BaseSetU