Theorem 0vfval

Description: Value of the function for the zero vector on a normed complex vector space. (Contributed by NM, 24-Apr-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	0vfval.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
	0vfval.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
Assertion	0vfval	⊢ ( 𝑈 ∈ 𝑉 → 𝑍 = ( GId ‘ 𝐺 ) )

Proof

Step	Hyp	Ref	Expression
1		0vfval.2	⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
2		0vfval.5	⊢ 𝑍 = ( 0vec ‘ 𝑈 )
3		elex	⊢ ( 𝑈 ∈ 𝑉 → 𝑈 ∈ V )
4		fo1st	⊢ 1st : V –onto→ V
5		fofn	⊢ ( 1st : V –onto→ V → 1st Fn V )
6	4 5	ax-mp	⊢ 1st Fn V
7		ssv	⊢ ran 1st ⊆ V
8		fnco	⊢ ( ( 1st Fn V ∧ 1st Fn V ∧ ran 1st ⊆ V ) → ( 1st ∘ 1st ) Fn V )
9	6 6 7 8	mp3an	⊢ ( 1st ∘ 1st ) Fn V
10		df-va	⊢ +𝑣 = ( 1st ∘ 1st )
11	10	fneq1i	⊢ ( +𝑣 Fn V ↔ ( 1st ∘ 1st ) Fn V )
12	9 11	mpbir	⊢ +𝑣 Fn V
13		fvco2	⊢ ( ( +𝑣 Fn V ∧ 𝑈 ∈ V ) → ( ( GId ∘ +𝑣 ) ‘ 𝑈 ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) )
14	12 13	mpan	⊢ ( 𝑈 ∈ V → ( ( GId ∘ +𝑣 ) ‘ 𝑈 ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) ) )
15		df-0v	⊢ 0vec = ( GId ∘ +𝑣 )
16	15	fveq1i	⊢ ( 0vec ‘ 𝑈 ) = ( ( GId ∘ +𝑣 ) ‘ 𝑈 )
17	2 16	eqtri	⊢ 𝑍 = ( ( GId ∘ +𝑣 ) ‘ 𝑈 )
18	1	fveq2i	⊢ ( GId ‘ 𝐺 ) = ( GId ‘ ( +𝑣 ‘ 𝑈 ) )
19	14 17 18	3eqtr4g	⊢ ( 𝑈 ∈ V → 𝑍 = ( GId ‘ 𝐺 ) )
20	3 19	syl	⊢ ( 𝑈 ∈ 𝑉 → 𝑍 = ( GId ‘ 𝐺 ) )