Metamath Proof Explorer

Theorem nvpncan

Description: Cancellation law for vector subtraction. (Contributed by NM, 24-Jan-2008) (New usage is discouraged.)

Ref Expression
Hypotheses nvpncan2.1 ⊢ X = BaseSet ⁡ U
nvpncan2.2 ⊢ G = + v ⁡ U
nvpncan2.3 ⊢ M = - v ⁡ U
Assertion nvpncan ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M B = A

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ X = BaseSet ⁡ U
2 nvpncan2.2 ⊢ G = + v ⁡ U
3 nvpncan2.3 ⊢ M = - v ⁡ U
4 1 2 nvcom ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B G A = A G B
5 4 oveq1d ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B G A M B = A G B M B
6 1 2 3 nvpncan2 ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → B G A M B = A
7 5 6 eqtr3d ⊢ U ∈ NrmCVec ∧ B ∈ X ∧ A ∈ X → A G B M B = A
8 7 3com23 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M B = A