Theorem bafval 28966

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	⊢ 𝑋 = (BaseSet‘𝑈)
bafval.2	⊢ 𝐺 = ( +𝑣 ‘𝑈)

Assertion

Ref	Expression
bafval	⊢ 𝑋 = ran 𝐺

Proof of Theorem bafval

Dummy variable 𝑢 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		fveq2 6774	. . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
2	1	rneqd 5847	. . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈))
3		df-ba 28958	. . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢))
4		fvex 6787	. . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V
5	4	rnex 7759	. . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V
6	2, 3, 5	fvmpt 6875	. . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
7		rn0 5835	. . . . 5 ⊢ ran ∅ = ∅
8	7	eqcomi 2747	. . . 4 ⊢ ∅ = ran ∅
9		fvprc 6766	. . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅)
10		fvprc 6766	. . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅)
11	10	rneqd 5847	. . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅)
12	8, 9, 11	3eqtr4a 2804	. . 3 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
13	6, 12	pm2.61i 182	. 2 ⊢ (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈)
14		bafval.1	. 2 ⊢ 𝑋 = (BaseSet‘𝑈)
15		bafval.2	. . 3 ⊢ 𝐺 = ( +𝑣 ‘𝑈)
16	15	rneqi 5846	. 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈)
17	13, 14, 16	3eqtr4i 2776	1 ⊢ 𝑋 = ran 𝐺

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256  ran crn 5590  ‘cfv 6433   +_𝑣 cpv 28947  BaseSetcba 28948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ral 3069  df-rex 3070  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-br 5075  df-opab 5137  df-mpt 5158  df-id 5489  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-iota 6391  df-fun 6435  df-fv 6441  df-ba 28958

This theorem is referenced by:  nvi  28976  nvgf  28980  nvsf  28981  nvgcl  28982  nvcom  28983  nvass  28984  nvadd32  28985  nvrcan  28986  nvadd4  28987  nvscl  28988  nvsid  28989  nvsass  28990  nvdi  28992  nvdir  28993  nv2  28994  nvzcl  28996  nv0rid  28997  nv0lid  28998  nv0  28999  nvsz  29000  nvinv  29001  nvinvfval  29002  nvmval  29004  nvmfval  29006  nvnnncan1  29009  nvnegneg  29011  nvrinv  29013  nvlinv  29014  nvaddsub  29017  cnnvba  29041  sspba  29089  isph  29184  phpar  29186  ip0i  29187  ipdirilem  29191  hhba  29529  hhssabloilem  29623  hhshsslem1  29629