Theorem vc0rid

Description: The zero vector is a right identity element. (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	vc0rid	$$⊢\left(W\in {CVec}_{\mathrm{OLD}}\wedge A\in X\right)\to AGZ=A$$

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	grporid	$$⊢\left(G\in \mathrm{GrpOp}\wedge A\in X\right)\to AGZ=A$$
6	4 5	sylan	$$⊢\left(W\in {CVec}_{\mathrm{OLD}}\wedge A\in X\right)\to AGZ=A$$