Theorem bafval 30124

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 6890	. . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
2	1	rneqd 5936	. . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈))
3		df-ba 30116	. . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢))
4		fvex 6903	. . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V
5	4	rnex 7905	. . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V
6	2, 3, 5	fvmpt 6997	. . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
7		rn0 5924	. . . . 5 ⊢ ran ∅ = ∅
8	7	eqcomi 2739	. . . 4 ⊢ ∅ = ran ∅
9		fvprc 6882	. . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅)
10		fvprc 6882	. . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅)
11	10	rneqd 5936	. . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅)
12	8, 9, 11	3eqtr4a 2796	. . 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 5935	. 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈)
17	13, 14, 16	3eqtr4i 2768	1 ⊢ 𝑋 = ran 𝐺

Syntax hints:  ¬ wn 3   = wceq 1539   ∈ wcel 2104  Vcvv 3472  ∅c0 4321  ran crn 5676  ‘cfv 6542   +_𝑣 cpv 30105  BaseSetcba 30106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7727

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-br 5148  df-opab 5210  df-mpt 5231  df-id 5573  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-iota 6494  df-fun 6544  df-fv 6550  df-ba 30116

This theorem is referenced by:  nvi  30134  nvgf  30138  nvsf  30139  nvgcl  30140  nvcom  30141  nvass  30142  nvadd32  30143  nvrcan  30144  nvadd4  30145  nvscl  30146  nvsid  30147  nvsass  30148  nvdi  30150  nvdir  30151  nv2  30152  nvzcl  30154  nv0rid  30155  nv0lid  30156  nv0  30157  nvsz  30158  nvinv  30159  nvinvfval  30160  nvmval  30162  nvmfval  30164  nvnnncan1  30167  nvnegneg  30169  nvrinv  30171  nvlinv  30172  nvaddsub  30175  cnnvba  30199  sspba  30247  isph  30342  phpar  30344  ip0i  30345  ipdirilem  30349  hhba  30687  hhssabloilem  30781  hhshsslem1  30787