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 𝐺