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 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
bafval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
Assertion bafval 𝑋 = ran 𝐺

Proof

Step Hyp Ref Expression
1 bafval.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 bafval.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 fveq2 ⊢ ( 𝑢 = 𝑈 → ( +𝑣 ‘ 𝑢 ) = ( +𝑣 ‘ 𝑈 ) )
4 3 rneqd ⊢ ( 𝑢 = 𝑈 → ran ( +𝑣 ‘ 𝑢 ) = ran ( +𝑣 ‘ 𝑈 ) )
5 df-ba ⊢ BaseSet = ( 𝑢 ∈ V ↦ ran ( +𝑣 ‘ 𝑢 ) )
6 fvex ⊢ ( +𝑣 ‘ 𝑈 ) ∈ V
7 6 rnex ⊢ ran ( +𝑣 ‘ 𝑈 ) ∈ V
8 4 5 7 fvmpt ⊢ ( 𝑈 ∈ V → ( BaseSet ‘ 𝑈 ) = ran ( +𝑣 ‘ 𝑈 ) )
9 rn0 ⊢ ran ∅ = ∅
10 9 eqcomi ⊢ ∅ = ran ∅
11 fvprc ⊢ ( ¬ 𝑈 ∈ V → ( BaseSet ‘ 𝑈 ) = ∅ )
12 fvprc ⊢ ( ¬ 𝑈 ∈ V → ( +𝑣 ‘ 𝑈 ) = ∅ )
13 12 rneqd ⊢ ( ¬ 𝑈 ∈ V → ran ( +𝑣 ‘ 𝑈 ) = ran ∅ )
14 10 11 13 3eqtr4a ⊢ ( ¬ 𝑈 ∈ V → ( BaseSet ‘ 𝑈 ) = ran ( +𝑣 ‘ 𝑈 ) )
15 8 14 pm2.61i ⊢ ( BaseSet ‘ 𝑈 ) = ran ( +𝑣 ‘ 𝑈 )
16 2 rneqi ⊢ ran 𝐺 = ran ( +𝑣 ‘ 𝑈 )
17 15 1 16 3eqtr4i ⊢ 𝑋 = ran 𝐺