Metamath Proof Explorer

Theorem hvsubcan2

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

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

Proof

Step Hyp Ref Expression
1 hvsubcl ⊢C∈ℋ∧A∈ℋ→C-ℎA∈ℋ
2 1 3adant3 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C-ℎA∈ℋ
3 hvsubcl ⊢C∈ℋ∧B∈ℋ→C-ℎB∈ℋ
4 3 3adant2 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C-ℎB∈ℋ
5 neg1cn ⊢−1∈ℂ
6 neg1ne0 ⊢−1≠0
7 5 6 pm3.2i ⊢−1∈ℂ∧−1≠0
8 hvmulcan ⊢−1∈ℂ∧−1≠0∧C-ℎA∈ℋ∧C-ℎB∈ℋ→-1⋅ℎC-ℎA=-1⋅ℎC-ℎB↔C-ℎA=C-ℎB
9 7 8 mp3an1 ⊢C-ℎA∈ℋ∧C-ℎB∈ℋ→-1⋅ℎC-ℎA=-1⋅ℎC-ℎB↔C-ℎA=C-ℎB
10 2 4 9 syl2anc ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→-1⋅ℎC-ℎA=-1⋅ℎC-ℎB↔C-ℎA=C-ℎB
11 hvnegdi ⊢C∈ℋ∧A∈ℋ→-1⋅ℎC-ℎA=A-ℎC
12 11 3adant3 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→-1⋅ℎC-ℎA=A-ℎC
13 hvnegdi ⊢C∈ℋ∧B∈ℋ→-1⋅ℎC-ℎB=B-ℎC
14 13 3adant2 ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→-1⋅ℎC-ℎB=B-ℎC
15 12 14 eqeq12d ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→-1⋅ℎC-ℎA=-1⋅ℎC-ℎB↔A-ℎC=B-ℎC
16 hvsubcan ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→C-ℎA=C-ℎB↔A=B
17 10 15 16 3bitr3d ⊢C∈ℋ∧A∈ℋ∧B∈ℋ→A-ℎC=B-ℎC↔A=B
18 17 3coml ⊢A∈ℋ∧B∈ℋ∧C∈ℋ→A-ℎC=B-ℎC↔A=B