Metamath Proof Explorer

Theorem hvsubcan

Description: Cancellation law for vector addition. (Contributed by NM, 18-May-2005) (New usage is discouraged.)

Ref Expression
Assertion hvsubcan ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=A-ℎC↔B=C

Proof

Step Hyp Ref Expression
1 hvsubval ⊢A∈ℋ∧B∈ℋ→A-ℎB=A+ℎ-1⋅ℎB
2 1 3adant3 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=A+ℎ-1⋅ℎB
3 hvsubval ⊢A∈ℋ∧C∈ℋ→A-ℎC=A+ℎ-1⋅ℎC
4 3 3adant2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎC=A+ℎ-1⋅ℎC
5 2 4 eqeq12d ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=A-ℎC↔A+ℎ-1⋅ℎB=A+ℎ-1⋅ℎC
6 neg1cn ⊢−1∈ℂ
7 hvmulcl ⊢−1∈ℂ∧B∈ℋ→-1⋅ℎB∈ℋ
8 6 7 mpan ⊢B∈ℋ→-1⋅ℎB∈ℋ
9 hvmulcl ⊢−1∈ℂ∧C∈ℋ→-1⋅ℎC∈ℋ
10 6 9 mpan ⊢C∈ℋ→-1⋅ℎC∈ℋ
11 hvaddcan ⊢A∈ℋ∧-1⋅ℎB∈ℋ∧-1⋅ℎC∈ℋ→A+ℎ-1⋅ℎB=A+ℎ-1⋅ℎC↔-1⋅ℎB=-1⋅ℎC
12 10 11 syl3an3 ⊢A∈ℋ∧-1⋅ℎB∈ℋ∧C∈ℋ→A+ℎ-1⋅ℎB=A+ℎ-1⋅ℎC↔-1⋅ℎB=-1⋅ℎC
13 8 12 syl3an2 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A+ℎ-1⋅ℎB=A+ℎ-1⋅ℎC↔-1⋅ℎB=-1⋅ℎC
14 neg1ne0 ⊢−1≠0
15 6 14 pm3.2i ⊢−1∈ℂ∧−1≠0
16 hvmulcan ⊢−1∈ℂ∧−1≠0∧B∈ℋ∧C∈ℋ→-1⋅ℎB=-1⋅ℎC↔B=C
17 15 16 mp3an1 ⊢B∈ℋ∧C∈ℋ→-1⋅ℎB=-1⋅ℎC↔B=C
18 17 3adant1 ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→-1⋅ℎB=-1⋅ℎC↔B=C
19 5 13 18 3bitrd ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎB=A-ℎC↔B=C