Theorem bafval 28486

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 6658	. . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
2	1	rneqd 5779	. . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈))
3		df-ba 28478	. . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢))
4		fvex 6671	. . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V
5	4	rnex 7622	. . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V
6	2, 3, 5	fvmpt 6759	. . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
7		rn0 5767	. . . . 5 ⊢ ran ∅ = ∅
8	7	eqcomi 2767	. . . 4 ⊢ ∅ = ran ∅
9		fvprc 6650	. . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅)
10		fvprc 6650	. . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅)
11	10	rneqd 5779	. . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅)
12	8, 9, 11	3eqtr4a 2819	. . 3 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
13	6, 12	pm2.61i 185	. 2 ⊢ (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈)
14		bafval.1	. 2 ⊢ 𝑋 = (BaseSet‘𝑈)
15		bafval.2	. . 3 ⊢ 𝐺 = ( +𝑣 ‘𝑈)
16	15	rneqi 5778	. 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈)
17	13, 14, 16	3eqtr4i 2791	1 ⊢ 𝑋 = ran 𝐺

Syntax hints:  ¬ wn 3   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ∅c0 4225  ran crn 5525  ‘cfv 6335   +_𝑣 cpv 28467  BaseSetcba 28468

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-rab 3079  df-v 3411  df-sbc 3697  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-uni 4799  df-br 5033  df-opab 5095  df-mpt 5113  df-id 5430  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-iota 6294  df-fun 6337  df-fv 6343  df-ba 28478

This theorem is referenced by:  nvi  28496  nvgf  28500  nvsf  28501  nvgcl  28502  nvcom  28503  nvass  28504  nvadd32  28505  nvrcan  28506  nvadd4  28507  nvscl  28508  nvsid  28509  nvsass  28510  nvdi  28512  nvdir  28513  nv2  28514  nvzcl  28516  nv0rid  28517  nv0lid  28518  nv0  28519  nvsz  28520  nvinv  28521  nvinvfval  28522  nvmval  28524  nvmfval  28526  nvnnncan1  28529  nvnegneg  28531  nvrinv  28533  nvlinv  28534  nvaddsub  28537  cnnvba  28561  sspba  28609  isph  28704  phpar  28706  ip0i  28707  ipdirilem  28711  hhba  29049  hhssabloilem  29143  hhshsslem1  29149