Theorem hvsubcan2

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

	Ref	Expression
Assertion	hvsubcan2	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐶 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐶 ) = ( 𝐵 −ℎ 𝐶 ) ↔ 𝐴 = 𝐵 ) )

Proof

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