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	⊢ 𝑍 = ( 0_vec ‘ 𝑈 )
Assertion	0vfval	⊢ ( 𝑈 ∈ 𝑉 → 𝑍 = ( GId ‘ 𝐺 ) )

Proof

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

Metamath Proof Explorer

Theorem 0vfval

Proof