Theorem nvablo

Description: The vector addition operation of a normed complex vector space is an Abelian group. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nvabl.1	$$⊢G={+}_v\left(U\right)$$
Assertion	nvablo	$$⊢U\in \mathrm{NrmCVec}\to G\in \mathrm{AbelOp}$$

Proof

Step	Hyp	Ref	Expression
1		nvabl.1	$$⊢G={+}_v\left(U\right)$$
2		eqid	$$⊢1^{st}\left(U\right)=1^{st}\left(U\right)$$
3	2	nvvc	$$⊢U\in \mathrm{NrmCVec}\to 1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}$$
4	1	vafval	$$⊢G=1^{st}\left(1^{st}\left(U\right)\right)$$
5	4	vcablo	$$⊢1^{st}\left(U\right)\in {CVec}_{\mathrm{OLD}}\to G\in \mathrm{AbelOp}$$
6	3 5	syl	$$⊢U\in \mathrm{NrmCVec}\to G\in \mathrm{AbelOp}$$