Theorem vcgrp

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

	Ref	Expression
Hypothesis	vcabl.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
Assertion	vcgrp	⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp )

Proof

Step	Hyp	Ref	Expression
1		vcabl.1	⊢ 𝐺 = ( 1st ‘ 𝑊 )
2	1	vcablo	⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ AbelOp )
3		ablogrpo	⊢ ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
4	2 3	syl	⊢ ( 𝑊 ∈ CVecOLD → 𝐺 ∈ GrpOp )