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⟩, abs⟩$
	Assertion	cnnvba	$⊢ ℂ = BaseSet (U)$

Step	Hyp	Ref	Expression
1		cnnvba.6	$⊢ U = ⟨⟨+ \times⟩, abs⟩$
2	1	cnnvg	$⊢ + = +_{v} (U)$
3	2	rneqi	$⊢ ran + = ran +_{v} (U)$
4		cnaddabloOLD	$⊢ + \in AbelOp$
5		ablogrpo	$⊢ + \in AbelOp \to + \in GrpOp$
6	4 5	ax-mp	$⊢ + \in GrpOp$
7		ax-addf	$⊢ + : ℂ \times ℂ ⟶ ℂ$
8	7	fdmi	$⊢ dom + = ℂ \times ℂ$
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)$

Metamath Proof Explorer