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 ` U )
Assertion	nvgrp	|- ( U e. NrmCVec -> G e. GrpOp )

Proof

Step	Hyp	Ref	Expression
1		nvabl.1	|- G = ( +v ` U )
2	1	nvablo	|- ( U e. NrmCVec -> G e. AbelOp )
3		ablogrpo	|- ( G e. AbelOp -> G e. GrpOp )
4	2 3	syl	|- ( U e. NrmCVec -> G e. GrpOp )