Theorem bafval 31188

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 6877	. . . . 5 ⊢ (𝑢 = 𝑈 → ( +𝑣 ‘𝑢) = ( +𝑣 ‘𝑈))
2	1	rneqd 5920	. . . 4 ⊢ (𝑢 = 𝑈 → ran ( +𝑣 ‘𝑢) = ran ( +𝑣 ‘𝑈))
3		df-ba 31180	. . . 4 ⊢ BaseSet = (𝑢 ∈ V ↦ ran ( +𝑣 ‘𝑢))
4		fvex 6890	. . . . 5 ⊢ ( +𝑣 ‘𝑈) ∈ V
5	4	rnex 7911	. . . 4 ⊢ ran ( +𝑣 ‘𝑈) ∈ V
6	2, 3, 5	fvmpt 6985	. . 3 ⊢ (𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
7		rn0 5908	. . . . 5 ⊢ ran ∅ = ∅
8	7	eqcomi 2770	. . . 4 ⊢ ∅ = ran ∅
9		fvprc 6869	. . . 4 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ∅)
10		fvprc 6869	. . . . 5 ⊢ (¬ 𝑈 ∈ V → ( +𝑣 ‘𝑈) = ∅)
11	10	rneqd 5920	. . . 4 ⊢ (¬ 𝑈 ∈ V → ran ( +𝑣 ‘𝑈) = ran ∅)
12	8, 9, 11	3eqtr4a 2822	. . 3 ⊢ (¬ 𝑈 ∈ V → (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈))
13	6, 12	pm2.61i 184	. 2 ⊢ (BaseSet‘𝑈) = ran ( +𝑣 ‘𝑈)
14		bafval.1	. 2 ⊢ 𝑋 = (BaseSet‘𝑈)
15		bafval.2	. . 3 ⊢ 𝐺 = ( +𝑣 ‘𝑈)
16	15	rneqi 5919	. 2 ⊢ ran 𝐺 = ran ( +𝑣 ‘𝑈)
17	13, 14, 16	3eqtr4i 2794	1 ⊢ 𝑋 = ran 𝐺

This proof depends on syntax axioms:  ¬ wn 3   = wceq 1570   ∈ wcel 2145  Vcvv 3451  ∅c0 4279  ran crn 5652  ‘cfv 6531   +_𝑣 cpv 31169  BaseSetcba 31170

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pr 5391  ax-un 7740

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-id 5546  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-iota 6487  df-fun 6533  df-fv 6539  df-ba 31180

This theorem is used by:  nvi  31198  nvgf  31202  nvsf  31203  nvgcl  31204  nvcom  31205  nvass  31206  nvadd32  31207  nvrcan  31208  nvadd4  31209  nvscl  31210  nvsid  31211  nvsass  31212  nvdi  31214  nvdir  31215  nv2  31216  nvzcl  31218  nv0rid  31219  nv0lid  31220  nv0  31221  nvsz  31222  nvinv  31223  nvinvfval  31224  nvmval  31226  nvmfval  31228  nvnnncan1  31231  nvnegneg  31233  nvrinv  31235  nvlinv  31236  nvaddsub  31239  cnnvba  31263  sspba  31311  isph  31406  phpar  31408  ip0i  31409  ipdirilem  31413  hhba  31751  hhssabloilem  31845  hhshsslem1  31851