Metamath Proof Explorer

Theorem vafval

Description: Value of the function for the vector addition (group) operation on a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	vafval.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
	Assertion	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )

Proof

Step	Hyp	Ref	Expression
1		vafval.2	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
2		df-va	⊢ +_𝑣 = ( 1^st ∘ 1^st )
3	2	fveq1i	⊢ ( +_𝑣 ‘ 𝑈 ) = ( ( 1^st ∘ 1^st ) ‘ 𝑈 )
4		fo1st	⊢ 1^st : V –onto→ V
5		fof	⊢ ( 1^st : V –onto→ V → 1^st : V ⟶ V )
6	4 5	ax-mp	⊢ 1^st : V ⟶ V
7		fvco3	⊢ ( ( 1^st : V ⟶ V ∧ 𝑈 ∈ V ) → ( ( 1^st ∘ 1^st ) ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
8	6 7	mpan	⊢ ( 𝑈 ∈ V → ( ( 1^st ∘ 1^st ) ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
9	3 8	syl5eq	⊢ ( 𝑈 ∈ V → ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
10		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( +_𝑣 ‘ 𝑈 ) = ∅ )
11		fvprc	⊢ ( ¬ 𝑈 ∈ V → ( 1^st ‘ 𝑈 ) = ∅ )
12	11	fveq2d	⊢ ( ¬ 𝑈 ∈ V → ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) = ( 1^st ‘ ∅ ) )
13		1st0	⊢ ( 1^st ‘ ∅ ) = ∅
14	12 13	eqtr2di	⊢ ( ¬ 𝑈 ∈ V → ∅ = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
15	10 14	eqtrd	⊢ ( ¬ 𝑈 ∈ V → ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) ) )
16	9 15	pm2.61i	⊢ ( +_𝑣 ‘ 𝑈 ) = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
17	1 16	eqtri	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )