Theorem vcgrp

Description: Vector addition is a group operation. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypothesis	vcabl.1	|- G = ( 1st ` W )
Assertion	vcgrp	|- ( W e. CVecOLD -> G e. GrpOp )

Proof

Step	Hyp	Ref	Expression
1		vcabl.1	|- G = ( 1st ` W )
2	1	vcablo	|- ( W e. CVecOLD -> G e. AbelOp )
3		ablogrpo	|- ( G e. AbelOp -> G e. GrpOp )
4	2 3	syl	|- ( W e. CVecOLD -> G e. GrpOp )