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 ∈ CVec OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B ↔ A = B

Proof

Step Hyp Ref Expression
1 vclcan.1 ⊢ G = 1 st ⁡ W
2 vclcan.2 ⊢ X = ran ⁡ G
3 1 vcgrp ⊢ W ∈ CVec OLD → G ∈ GrpOp
4 2 grpolcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B ↔ A = B
5 3 4 sylan ⊢ W ∈ CVec OLD ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → C G A = C G B ↔ A = B