Metamath Proof Explorer

Theorem nvrcan

Description: Right cancellation law for vector addition. (Contributed by NM, 4-Dec-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvgcl.1 ⊢ X = BaseSet ⁡ U
nvgcl.2 ⊢ G = + v ⁡ U
Assertion nvrcan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B

Proof

Step Hyp Ref Expression
1 nvgcl.1 ⊢ X = BaseSet ⁡ U
2 nvgcl.2 ⊢ G = + v ⁡ U
3 2 nvgrp ⊢ U ∈ NrmCVec → G ∈ GrpOp
4 1 2 bafval ⊢ X = ran ⁡ G
5 4 grporcan ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B
6 3 5 sylan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C = B G C ↔ A = B