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=1^{st}\left(W\right)$$
Assertion	vcgrp	$$⊢W\in {CVec}_{\mathrm{OLD}}\to G\in \mathrm{GrpOp}$$

Proof

Step	Hyp	Ref	Expression
1		vcabl.1	$$⊢G=1^{st}\left(W\right)$$
2	1	vcablo	$$⊢W\in {CVec}_{\mathrm{OLD}}\to G\in \mathrm{AbelOp}$$
3		ablogrpo	$$⊢G\in \mathrm{AbelOp}\to G\in \mathrm{GrpOp}$$
4	2 3	syl	$$⊢W\in {CVec}_{\mathrm{OLD}}\to G\in \mathrm{GrpOp}$$