Theorem bafval

Description: Value of the function for the base set of a normed complex vector space. (Contributed by NM, 23-Apr-2007) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bafval.1	|- X = ( BaseSet ` U )
	bafval.2	|- G = ( +v ` U )
Assertion	bafval	|- X = ran G

Proof

Step	Hyp	Ref	Expression
1		bafval.1	|- X = ( BaseSet ` U )
2		bafval.2	|- G = ( +v ` U )
3		fveq2	|- ( u = U -> ( +v ` u ) = ( +v ` U ) )
4	3	rneqd	|- ( u = U -> ran ( +v ` u ) = ran ( +v ` U ) )
5		df-ba	|- BaseSet = ( u e. _V |-> ran ( +v ` u ) )
6		fvex	|- ( +v ` U ) e. _V
7	6	rnex	|- ran ( +v ` U ) e. _V
8	4 5 7	fvmpt	|- ( U e. _V -> ( BaseSet ` U ) = ran ( +v ` U ) )
9		rn0	|- ran (/) = (/)
10	9	eqcomi	|- (/) = ran (/)
11		fvprc	|- ( -. U e. _V -> ( BaseSet ` U ) = (/) )
12		fvprc	|- ( -. U e. _V -> ( +v ` U ) = (/) )
13	12	rneqd	|- ( -. U e. _V -> ran ( +v ` U ) = ran (/) )
14	10 11 13	3eqtr4a	|- ( -. U e. _V -> ( BaseSet ` U ) = ran ( +v ` U ) )
15	8 14	pm2.61i	|- ( BaseSet ` U ) = ran ( +v ` U )
16	2	rneqi	|- ran G = ran ( +v ` U )
17	15 1 16	3eqtr4i	|- X = ran G