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	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
Assertion	cnnvba	⊢ ℂ = ( BaseSet ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		cnnvba.6	⊢ 𝑈 = ⟨ ⟨ + , · ⟩ , abs ⟩
2	1	cnnvg	⊢ + = ( +𝑣 ‘ 𝑈 )
3	2	rneqi	⊢ ran + = ran ( +𝑣 ‘ 𝑈 )
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 ‘ 𝑈 ) = ( BaseSet ‘ 𝑈 )
11		eqid	⊢ ( +𝑣 ‘ 𝑈 ) = ( +𝑣 ‘ 𝑈 )
12	10 11	bafval	⊢ ( BaseSet ‘ 𝑈 ) = ran ( +𝑣 ‘ 𝑈 )
13	3 9 12	3eqtr4i	⊢ ℂ = ( BaseSet ‘ 𝑈 )