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	$$⊢G={+}_v\left(U\right)$$
Assertion	vafval	$$⊢G=1^{st}\left(1^{st}\left(U\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		vafval.2	$$⊢G={+}_v\left(U\right)$$
2		df-va	$$⊢{+}_v=1^{st}\circ 1^{st}$$
3	2	fveq1i	$$⊢{+}_v\left(U\right)=\left(1^{st}\circ 1^{st}\right)\left(U\right)$$
4		fo1st	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}$$
5		fof	$$⊢1^{st}:\mathrm{V}\underset{onto}{⟶}\mathrm{V}\to 1^{st}:\mathrm{V}⟶\mathrm{V}$$
6	4 5	ax-mp	$$⊢1^{st}:\mathrm{V}⟶\mathrm{V}$$
7		fvco3	$$⊢\left(1^{st}:\mathrm{V}⟶\mathrm{V}\wedge U\in \mathrm{V}\right)\to \left(1^{st}\circ 1^{st}\right)\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
8	6 7	mpan	$$⊢U\in \mathrm{V}\to \left(1^{st}\circ 1^{st}\right)\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
9	3 8	syl5eq	$$⊢U\in \mathrm{V}\to {+}_v\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
10		fvprc	$$⊢\neg U\in \mathrm{V}\to {+}_v\left(U\right)=\varnothing$$
11		fvprc	$$⊢\neg U\in \mathrm{V}\to 1^{st}\left(U\right)=\varnothing$$
12	11	fveq2d	$$⊢\neg U\in \mathrm{V}\to 1^{st}\left(1^{st}\left(U\right)\right)=1^{st}\left(\varnothing \right)$$
13		1st0	$$⊢1^{st}\left(\varnothing \right)=\varnothing$$
14	12 13	eqtr2di	$$⊢\neg U\in \mathrm{V}\to \varnothing =1^{st}\left(1^{st}\left(U\right)\right)$$
15	10 14	eqtrd	$$⊢\neg U\in \mathrm{V}\to {+}_v\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
16	9 15	pm2.61i	$$⊢{+}_v\left(U\right)=1^{st}\left(1^{st}\left(U\right)\right)$$
17	1 16	eqtri	$$⊢G=1^{st}\left(1^{st}\left(U\right)\right)$$