Theorem bafval 29609

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 6847	. . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
2	1	rneqd 5898	. . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈))
3		df-ba 29601	. . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢))
4		fvex 6860	. . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V
5	4	rnex 7854	. . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V
6	2, 3, 5	fvmpt 6953	. . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
7		rn0 5886	. . . . 5 ⊢ ran ∅ = ∅
8	7	eqcomi 2740	. . . 4 ⊢ ∅ = ran ∅
9		fvprc 6839	. . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅)
10		fvprc 6839	. . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅)
11	10	rneqd 5898	. . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅)
12	8, 9, 11	3eqtr4a 2797	. . 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 5897	. 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈)
17	13, 14, 16	3eqtr4i 2769	1 ⊢ 𝑋 = ran 𝐺

Syntax hints:  ¬ wn 3   = wceq 1541   ∈ wcel 2106  Vcvv 3446  ∅c0 4287  ran crn 5639  ‘cfv 6501   +_𝑣 cpv 29590  BaseSetcba 29591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  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 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389  ax-un 7677

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-uni 4871  df-br 5111  df-opab 5173  df-mpt 5194  df-id 5536  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-iota 6453  df-fun 6503  df-fv 6509  df-ba 29601

This theorem is referenced by:  nvi  29619  nvgf  29623  nvsf  29624  nvgcl  29625  nvcom  29626  nvass  29627  nvadd32  29628  nvrcan  29629  nvadd4  29630  nvscl  29631  nvsid  29632  nvsass  29633  nvdi  29635  nvdir  29636  nv2  29637  nvzcl  29639  nv0rid  29640  nv0lid  29641  nv0  29642  nvsz  29643  nvinv  29644  nvinvfval  29645  nvmval  29647  nvmfval  29649  nvnnncan1  29652  nvnegneg  29654  nvrinv  29656  nvlinv  29657  nvaddsub  29660  cnnvba  29684  sspba  29732  isph  29827  phpar  29829  ip0i  29830  ipdirilem  29834  hhba  30172  hhssabloilem  30266  hhshsslem1  30272