This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = BaseSet ⁡ U
bafval.2 ⊢ G = + v ⁡ U
Assertion bafval ⊢ X = ran ⁡ G

Proof

Step Hyp Ref Expression
1 bafval.1 ⊢ X = BaseSet ⁡ U
2 bafval.2 ⊢ G = + v ⁡ U
3 fveq2 ⊢ u = U → + v ⁡ u = + v ⁡ U
4 3 rneqd ⊢ u = U → ran ⁡ + v ⁡ u = ran ⁡ + v ⁡ U
5 df-ba ⊢ BaseSet = u ∈ V ⟼ ran ⁡ + v ⁡ u
6 fvex ⊢ + v ⁡ U ∈ V
7 6 rnex ⊢ ran ⁡ + v ⁡ U ∈ V
8 4 5 7 fvmpt ⊢ U ∈ V → BaseSet ⁡ U = ran ⁡ + v ⁡ U
9 rn0 ⊢ ran ⁡ ∅ = ∅
10 9 eqcomi ⊢ ∅ = ran ⁡ ∅
11 fvprc ⊢ ¬ U ∈ V → BaseSet ⁡ U = ∅
12 fvprc ⊢ ¬ U ∈ V → + v ⁡ U = ∅
13 12 rneqd ⊢ ¬ U ∈ V → ran ⁡ + v ⁡ U = ran ⁡ ∅
14 10 11 13 3eqtr4a ⊢ ¬ U ∈ V → BaseSet ⁡ U = ran ⁡ + v ⁡ U
15 8 14 pm2.61i ⊢ BaseSet ⁡ U = ran ⁡ + v ⁡ U
16 2 rneqi ⊢ ran ⁡ G = ran ⁡ + v ⁡ U
17 15 1 16 3eqtr4i ⊢ X = ran ⁡ G