# 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}=⟨⟨+,×⟩,\mathrm{abs}⟩$
Assertion cnnvba ${⊢}ℂ=\mathrm{BaseSet}\left({U}\right)$

### Proof

Step Hyp Ref Expression
1 cnnvba.6 ${⊢}{U}=⟨⟨+,×⟩,\mathrm{abs}⟩$
2 1 cnnvg ${⊢}+={+}_{v}\left({U}\right)$
3 2 rneqi ${⊢}\mathrm{ran}+=\mathrm{ran}{+}_{v}\left({U}\right)$
4 cnaddabloOLD ${⊢}+\in \mathrm{AbelOp}$
5 ablogrpo ${⊢}+\in \mathrm{AbelOp}\to +\in \mathrm{GrpOp}$
6 4 5 ax-mp ${⊢}+\in \mathrm{GrpOp}$
7 ax-addf ${⊢}+:ℂ×ℂ⟶ℂ$
8 7 fdmi ${⊢}\mathrm{dom}+=ℂ×ℂ$
9 6 8 grporn ${⊢}ℂ=\mathrm{ran}+$
10 eqid ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{BaseSet}\left({U}\right)$
11 eqid ${⊢}{+}_{v}\left({U}\right)={+}_{v}\left({U}\right)$
12 10 11 bafval ${⊢}\mathrm{BaseSet}\left({U}\right)=\mathrm{ran}{+}_{v}\left({U}\right)$
13 3 9 12 3eqtr4i ${⊢}ℂ=\mathrm{BaseSet}\left({U}\right)$