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}\left(W\right)$$
	vczcl.2	$$⊢X=\mathrm{ran}G$$
	vczcl.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
Assertion	vczcl	$$⊢W\in {CVec}_{\mathrm{OLD}}\to Z\in X$$

Proof

Step	Hyp	Ref	Expression
1		vczcl.1	$$⊢G=1^{st}\left(W\right)$$
2		vczcl.2	$$⊢X=\mathrm{ran}G$$
3		vczcl.3	$$⊢Z=\mathrm{GId}\left(G\right)$$
4	1	vcgrp	$$⊢W\in {CVec}_{\mathrm{OLD}}\to G\in \mathrm{GrpOp}$$
5	2 3	grpoidcl	$$⊢G\in \mathrm{GrpOp}\to Z\in X$$
6	4 5	syl	$$⊢W\in {CVec}_{\mathrm{OLD}}\to Z\in X$$