Theorem hvsubcan

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

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

Proof

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