Metamath Proof Explorer

Theorem nvpncan2

Description: Cancellation law for vector subtraction. (Contributed by NM, 27-Dec-2007) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 nvpncan2.1 ⊢ X = BaseSet ⁡ U
2 nvpncan2.2 ⊢ G = + v ⁡ U
3 nvpncan2.3 ⊢ M = - v ⁡ U
4 simp1 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → U ∈ NrmCVec
5 1 2 nvgcl ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B ∈ X
6 simp2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A ∈ X
7 eqid ⊢ ⋅ 𝑠OLD ⁡ U = ⋅ 𝑠OLD ⁡ U
8 1 2 7 3 nvmval ⊢ U ∈ NrmCVec ∧ A G B ∈ X ∧ A ∈ X → A G B M A = A G B G -1 ⋅ 𝑠OLD ⁡ U A
9 4 5 6 8 syl3anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M A = A G B G -1 ⋅ 𝑠OLD ⁡ U A
10 simp3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → B ∈ X
11 neg1cn ⊢ − 1 ∈ ℂ
12 1 7 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ A ∈ X → -1 ⋅ 𝑠OLD ⁡ U A ∈ X
13 11 12 mp3an2 ⊢ U ∈ NrmCVec ∧ A ∈ X → -1 ⋅ 𝑠OLD ⁡ U A ∈ X
14 13 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 ⋅ 𝑠OLD ⁡ U A ∈ X
15 1 2 nvadd32 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X ∧ -1 ⋅ 𝑠OLD ⁡ U A ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U A = A G -1 ⋅ 𝑠OLD ⁡ U A G B
16 4 6 10 14 15 syl13anc ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U A = A G -1 ⋅ 𝑠OLD ⁡ U A G B
17 eqid ⊢ 0 vec ⁡ U = 0 vec ⁡ U
18 1 2 7 17 nvrinv ⊢ U ∈ NrmCVec ∧ A ∈ X → A G -1 ⋅ 𝑠OLD ⁡ U A = 0 vec ⁡ U
19 18 3adant3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G -1 ⋅ 𝑠OLD ⁡ U A = 0 vec ⁡ U
20 19 oveq1d ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G -1 ⋅ 𝑠OLD ⁡ U A G B = 0 vec ⁡ U G B
21 1 2 17 nv0lid ⊢ U ∈ NrmCVec ∧ B ∈ X → 0 vec ⁡ U G B = B
22 21 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → 0 vec ⁡ U G B = B
23 20 22 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G -1 ⋅ 𝑠OLD ⁡ U A G B = B
24 16 23 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B G -1 ⋅ 𝑠OLD ⁡ U A = B
25 9 24 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G B M A = B