This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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} (W)$
	Assertion	vcgrp	$⊢ W \in {CVec}_{OLD} \to G \in GrpOp$

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