Theorem vclcan

Description: Left cancellation law for vector addition. (Contributed by NM, 4-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	vclcan.1	|- G = ( 1st ` W )
	vclcan.2	|- X = ran G
Assertion	vclcan	|- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )

Proof

Step	Hyp	Ref	Expression
1		vclcan.1	|- G = ( 1st ` W )
2		vclcan.2	|- X = ran G
3	1	vcgrp	|- ( W e. CVecOLD -> G e. GrpOp )
4	2	grpolcan	|- ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )
5	3 4	sylan	|- ( ( W e. CVecOLD /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( C G A ) = ( C G B ) <-> A = B ) )