MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  bafval Structured version   Unicode version

Theorem bafval 24133
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.)
Hypotheses
Ref Expression
bafval.1  |-  X  =  ( BaseSet `  U )
bafval.2  |-  G  =  ( +v `  U
)
Assertion
Ref Expression
bafval  |-  X  =  ran  G

Proof of Theorem bafval
Dummy variable  u is distinct from all other variables.
StepHypRef Expression
1 fveq2 5798 . . . . 5  |-  ( u  =  U  ->  ( +v `  u )  =  ( +v `  U
) )
21rneqd 5174 . . . 4  |-  ( u  =  U  ->  ran  ( +v `  u )  =  ran  ( +v
`  U ) )
3 df-ba 24125 . . . 4  |-  BaseSet  =  ( u  e.  _V  |->  ran  ( +v `  u
) )
4 fvex 5808 . . . . 5  |-  ( +v
`  U )  e. 
_V
54rnex 6621 . . . 4  |-  ran  ( +v `  U )  e. 
_V
62, 3, 5fvmpt 5882 . . 3  |-  ( U  e.  _V  ->  ( BaseSet
`  U )  =  ran  ( +v `  U ) )
7 rn0 5198 . . . . 5  |-  ran  (/)  =  (/)
87eqcomi 2467 . . . 4  |-  (/)  =  ran  (/)
9 fvprc 5792 . . . 4  |-  ( -.  U  e.  _V  ->  (
BaseSet `  U )  =  (/) )
10 fvprc 5792 . . . . 5  |-  ( -.  U  e.  _V  ->  ( +v `  U )  =  (/) )
1110rneqd 5174 . . . 4  |-  ( -.  U  e.  _V  ->  ran  ( +v `  U
)  =  ran  (/) )
128, 9, 113eqtr4a 2521 . . 3  |-  ( -.  U  e.  _V  ->  (
BaseSet `  U )  =  ran  ( +v `  U ) )
136, 12pm2.61i 164 . 2  |-  ( BaseSet `  U )  =  ran  ( +v `  U )
14 bafval.1 . 2  |-  X  =  ( BaseSet `  U )
15 bafval.2 . . 3  |-  G  =  ( +v `  U
)
1615rneqi 5173 . 2  |-  ran  G  =  ran  ( +v `  U )
1713, 14, 163eqtr4i 2493 1  |-  X  =  ran  G
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    = wceq 1370    e. wcel 1758   _Vcvv 3076   (/)c0 3744   ran crn 4948   ` cfv 5525   +vcpv 24114   BaseSetcba 24115
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-8 1760  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4520  ax-nul 4528  ax-pow 4577  ax-pr 4638  ax-un 6481
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2649  df-ral 2803  df-rex 2804  df-rab 2807  df-v 3078  df-sbc 3293  df-dif 3438  df-un 3440  df-in 3442  df-ss 3449  df-nul 3745  df-if 3899  df-sn 3985  df-pr 3987  df-op 3991  df-uni 4199  df-br 4400  df-opab 4458  df-mpt 4459  df-id 4743  df-xp 4953  df-rel 4954  df-cnv 4955  df-co 4956  df-dm 4957  df-rn 4958  df-iota 5488  df-fun 5527  df-fv 5533  df-ba 24125
This theorem is referenced by:  nvi  24143  nvgf  24147  nvsf  24148  nvgcl  24149  nvcom  24150  nvass  24151  nvadd32  24153  nvrcan  24154  nvlcan  24155  nvadd4  24156  nvscl  24157  nvsid  24158  nvsass  24159  nvdi  24161  nvdir  24162  nv2  24163  nvzcl  24165  nv0rid  24166  nv0lid  24167  nv0  24168  nvsz  24169  nvinv  24170  nvinvfval  24171  nvmval  24173  nvmfval  24175  nvnnncan1  24179  nvnnncan2  24180  nvnegneg  24182  nvrinv  24184  nvlinv  24185  nvaddsubass  24189  nvaddsub  24190  nvdm  24200  nvmtri2  24211  cnnvba  24220  sspba  24276  isph  24373  phpar  24375  ip0i  24376  ipdirilem  24380  hhba  24720  hhssabloi  24814  hhshsslem1  24819
  Copyright terms: Public domain W3C validator