Metamath Proof Explorer

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 = ( x e. _V |-> ran ( +v ` x ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cba 
 |-  BaseSet
1 vx 
 |-  x
2 cvv 
 |-  _V
3 cpv 
 |-  +v
4 1 cv 
 |-  x
5 4 3 cfv 
 |-  ( +v ` x )
6 5 crn 
 |-  ran ( +v ` x )
7 1 2 6 cmpt 
 |-  ( x e. _V |-> ran ( +v ` x ) )
8 0 7 wceq 
 |-  BaseSet = ( x e. _V |-> ran ( +v ` x ) )