Metamath Proof Explorer

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 = 1^{st} (W)$
	vclcan.2	$⊢ X = ran G$
Assertion	vclcan	$⊢ (W \in {CVec}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (C G A = C G B \leftrightarrow A = B)$

Step	Hyp	Ref	Expression
1		vclcan.1	$⊢ G = 1^{st} (W)$
2		vclcan.2	$⊢ X = ran G$
3	1	vcgrp	$⊢ W \in {CVec}_{OLD} \to G \in GrpOp$
4	2	grpolcan	$⊢ (G \in GrpOp \land (A \in X \land B \in X \land C \in X)) \to (C G A = C G B \leftrightarrow A = B)$
5	3 4	sylan	$⊢ (W \in {CVec}_{OLD} \land (A \in X \land B \in X \land C \in X)) \to (C G A = C G B \leftrightarrow A = B)$