Theorem bafval

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.)

	Ref	Expression
Hypotheses	bafval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	bafval.2	$$⊢G={+}_v\left(U\right)$$
Assertion	bafval	$$⊢X=\mathrm{ran}G$$

Proof

Step	Hyp	Ref	Expression
1		bafval.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		bafval.2	$$⊢G={+}_v\left(U\right)$$
3		fveq2	$$⊢u=U\to {+}_v\left(u\right)={+}_v\left(U\right)$$
4	3	rneqd	$$⊢u=U\to \mathrm{ran}{+}_v\left(u\right)=\mathrm{ran}{+}_v\left(U\right)$$
5		df-ba	$$⊢\mathrm{BaseSet}=\left(u\in \mathrm{V}⟼\mathrm{ran}{+}_v\left(u\right)\right)$$
6		fvex	$$⊢{+}_v\left(U\right)\in \mathrm{V}$$
7	6	rnex	$$⊢\mathrm{ran}{+}_v\left(U\right)\in \mathrm{V}$$
8	4 5 7	fvmpt	$$⊢U\in \mathrm{V}\to \mathrm{BaseSet}\left(U\right)=\mathrm{ran}{+}_v\left(U\right)$$
9		rn0	$$⊢\mathrm{ran}\varnothing =\varnothing$$
10	9	eqcomi	$$⊢\varnothing =\mathrm{ran}\varnothing$$
11		fvprc	$$⊢\neg U\in \mathrm{V}\to \mathrm{BaseSet}\left(U\right)=\varnothing$$
12		fvprc	$$⊢\neg U\in \mathrm{V}\to {+}_v\left(U\right)=\varnothing$$
13	12	rneqd	$$⊢\neg U\in \mathrm{V}\to \mathrm{ran}{+}_v\left(U\right)=\mathrm{ran}\varnothing$$
14	10 11 13	3eqtr4a	$$⊢\neg U\in \mathrm{V}\to \mathrm{BaseSet}\left(U\right)=\mathrm{ran}{+}_v\left(U\right)$$
15	8 14	pm2.61i	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{ran}{+}_v\left(U\right)$$
16	2	rneqi	$$⊢\mathrm{ran}G=\mathrm{ran}{+}_v\left(U\right)$$
17	15 1 16	3eqtr4i	$$⊢X=\mathrm{ran}G$$