Description: The zero vector is a vector. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | vczcl.1 | ||
vczcl.2 | |||
vczcl.3 | |||
Assertion | vczcl |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | vczcl.1 | ||
2 | vczcl.2 | ||
3 | vczcl.3 | ||
4 | 1 | vcgrp | |
5 | 2 3 | grpoidcl | |
6 | 4 5 | syl |