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 = BaseSet U

Proof

Step Hyp Ref Expression
1 cnnvba.6 U = + × abs
2 1 cnnvg + = + v U
3 2 rneqi ran + = ran + v U
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 BaseSet U = BaseSet U
11 eqid + v U = + v U
12 10 11 bafval BaseSet U = ran + v U
13 3 9 12 3eqtr4i = BaseSet U