This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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