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

Proof

Step	Hyp	Ref	Expression
1		cnnvba.6	$$⊢U=⟨⟨+,\times ⟩,\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	$$⊢+:ℂ\times ℂ⟶ℂ$$
8	7	fdmi	$$⊢\mathrm{dom}+=ℂ\times ℂ$$
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)$$