Theorem nvgrp

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

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

Proof

Step	Hyp	Ref	Expression
1		nvabl.1	$$⊢G={+}_v\left(U\right)$$
2	1	nvablo	$$⊢U\in \mathrm{NrmCVec}\to G\in \mathrm{AbelOp}$$
3		ablogrpo	$$⊢G\in \mathrm{AbelOp}\to G\in \mathrm{GrpOp}$$
4	2 3	syl	$$⊢U\in \mathrm{NrmCVec}\to G\in \mathrm{GrpOp}$$