# Metamath Proof Explorer

## 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 ${⊢}¬{U}\in \mathrm{V}\to \mathrm{BaseSet}\left({U}\right)=\varnothing$
12 fvprc ${⊢}¬{U}\in \mathrm{V}\to {+}_{v}\left({U}\right)=\varnothing$
13 12 rneqd ${⊢}¬{U}\in \mathrm{V}\to \mathrm{ran}{+}_{v}\left({U}\right)=\mathrm{ran}\varnothing$
14 10 11 13 3eqtr4a ${⊢}¬{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}$