Metamath Proof Explorer


Theorem vczcl

Description: The zero vector is a vector. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypotheses vczcl.1 G = 1 st W
vczcl.2 X = ran G
vczcl.3 Z = GId G
Assertion vczcl W CVec OLD Z X

Proof

Step Hyp Ref Expression
1 vczcl.1 G = 1 st W
2 vczcl.2 X = ran G
3 vczcl.3 Z = GId G
4 1 vcgrp W CVec OLD G GrpOp
5 2 3 grpoidcl G GrpOp Z X
6 4 5 syl W CVec OLD Z X