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 = ( 1st ` W )
	vczcl.2	|- X = ran G
	vczcl.3	|- Z = ( GId ` G )
Assertion	vc0rid	|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G Z ) = A )

Proof

Step	Hyp	Ref	Expression
1		vczcl.1	|- G = ( 1st ` W )
2		vczcl.2	|- X = ran G
3		vczcl.3	|- Z = ( GId ` G )
4	1	vcgrp	|- ( W e. CVecOLD -> G e. GrpOp )
5	2 3	grporid	|- ( ( G e. GrpOp /\ A e. X ) -> ( A G Z ) = A )
6	4 5	sylan	|- ( ( W e. CVecOLD /\ A e. X ) -> ( A G Z ) = A )