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

Theorem bafval 22071
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 5719 . . . . 5  |-  ( u  =  U  ->  ( +v `  u )  =  ( +v `  U
) )
21rneqd 5088 . . . 4  |-  ( u  =  U  ->  ran  ( +v `  u )  =  ran  ( +v
`  U ) )
3 df-ba 22063 . . . 4  |-  BaseSet  =  ( u  e.  _V  |->  ran  ( +v `  u
) )
4 fvex 5733 . . . . 5  |-  ( +v
`  U )  e. 
_V
54rnex 5124 . . . 4  |-  ran  ( +v `  U )  e. 
_V
62, 3, 5fvmpt 5797 . . 3  |-  ( U  e.  _V  ->  ( BaseSet
`  U )  =  ran  ( +v `  U ) )
7 rn0 5118 . . . . 5  |-  ran  (/)  =  (/)
87eqcomi 2439 . . . 4  |-  (/)  =  ran  (/)
9 fvprc 5713 . . . 4  |-  ( -.  U  e.  _V  ->  (
BaseSet `  U )  =  (/) )
10 fvprc 5713 . . . . 5  |-  ( -.  U  e.  _V  ->  ( +v `  U )  =  (/) )
1110rneqd 5088 . . . 4  |-  ( -.  U  e.  _V  ->  ran  ( +v `  U
)  =  ran  (/) )
128, 9, 113eqtr4a 2493 . . 3  |-  ( -.  U  e.  _V  ->  (
BaseSet `  U )  =  ran  ( +v `  U ) )
136, 12pm2.61i 158 . 2  |-  ( BaseSet `  U )  =  ran  ( +v `  U )
14 bafval.1 . 2  |-  X  =  ( BaseSet `  U )
15 bafval.2 . . 3  |-  G  =  ( +v `  U
)
1615rneqi 5087 . 2  |-  ran  G  =  ran  ( +v `  U )
1713, 14, 163eqtr4i 2465 1  |-  X  =  ran  G
Colors of variables: wff set class
Syntax hints:   -. wn 3    = wceq 1652    e. wcel 1725   _Vcvv 2948   (/)c0 3620   ran crn 4870   ` cfv 5445   +vcpv 22052   BaseSetcba 22053
This theorem is referenced by:  nvi  22081  nvgf  22085  nvsf  22086  nvgcl  22087  nvcom  22088  nvass  22089  nvadd32  22091  nvrcan  22092  nvlcan  22093  nvadd4  22094  nvscl  22095  nvsid  22096  nvsass  22097  nvdi  22099  nvdir  22100  nv2  22101  nvzcl  22103  nv0rid  22104  nv0lid  22105  nv0  22106  nvsz  22107  nvinv  22108  nvinvfval  22109  nvmval  22111  nvmfval  22113  nvnnncan1  22117  nvnnncan2  22118  nvnegneg  22120  nvrinv  22122  nvlinv  22123  nvaddsubass  22127  nvaddsub  22128  nvdm  22138  nvmtri2  22149  cnnvba  22158  sspba  22214  isph  22311  phpar  22313  ip0i  22314  ipdirilem  22318  hhba  22657  hhssabloi  22750  hhshsslem1  22755
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-rab 2706  df-v 2950  df-sbc 3154  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-nul 3621  df-if 3732  df-sn 3812  df-pr 3813  df-op 3815  df-uni 4008  df-br 4205  df-opab 4259  df-mpt 4260  df-id 4490  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-iota 5409  df-fun 5447  df-fv 5453  df-ba 22063
  Copyright terms: Public domain W3C validator