Definition df-ba

Description: Define the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	df-ba	⊢ BaseSet = ( 𝑥 ∈ V ↦ ran ( +𝑣 ‘ 𝑥 ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cba	⊢ BaseSet
1		vx	⊢ 𝑥
2		cvv	⊢ V
3		cpv	⊢ +𝑣
4	1	cv	⊢ 𝑥
5	4 3	cfv	⊢ ( +𝑣 ‘ 𝑥 )
6	5	crn	⊢ ran ( +𝑣 ‘ 𝑥 )
7	1 2 6	cmpt	⊢ ( 𝑥 ∈ V ↦ ran ( +𝑣 ‘ 𝑥 ) )
8	0 7	wceq	⊢ BaseSet = ( 𝑥 ∈ V ↦ ran ( +𝑣 ‘ 𝑥 ) )