Theorem hvsubeq0i

Description: If the difference between two vectors is zero, they are equal. (Contributed by NM, 18-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	⊢ 𝐴 ∈ ℋ
	hvnegdi.2	⊢ 𝐵 ∈ ℋ
Assertion	hvsubeq0i	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	⊢ 𝐴 ∈ ℋ
2		hvnegdi.2	⊢ 𝐵 ∈ ℋ
3	1 2	hvsubvali	⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
4	3	eqeq1i	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ ↔ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ )
5		oveq1	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ 𝐵 ) = ( 0ℎ +ℎ 𝐵 ) )
6	4 5	sylbi	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ → ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ 𝐵 ) = ( 0ℎ +ℎ 𝐵 ) )
7		neg1cn	⊢ - 1 ∈ ℂ
8	7 2	hvmulcli	⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
9	1 8 2	hvadd32i	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ 𝐵 ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) )
10	1 2 8	hvassi	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) = ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
11	2	hvnegidi	⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ
12	11	oveq2i	⊢ ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 𝐴 +ℎ 0ℎ )
13		ax-hvaddid	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 +ℎ 0ℎ ) = 𝐴 )
14	1 13	ax-mp	⊢ ( 𝐴 +ℎ 0ℎ ) = 𝐴
15	12 14	eqtri	⊢ ( 𝐴 +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = 𝐴
16	10 15	eqtri	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( - 1 ·ℎ 𝐵 ) ) = 𝐴
17	9 16	eqtri	⊢ ( ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) +ℎ 𝐵 ) = 𝐴
18	2	hvaddlidi	⊢ ( 0ℎ +ℎ 𝐵 ) = 𝐵
19	6 17 18	3eqtr3g	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ → 𝐴 = 𝐵 )
20		oveq1	⊢ ( 𝐴 = 𝐵 → ( 𝐴 −ℎ 𝐵 ) = ( 𝐵 −ℎ 𝐵 ) )
21		hvsubid	⊢ ( 𝐵 ∈ ℋ → ( 𝐵 −ℎ 𝐵 ) = 0ℎ )
22	2 21	ax-mp	⊢ ( 𝐵 −ℎ 𝐵 ) = 0ℎ
23	20 22	eqtrdi	⊢ ( 𝐴 = 𝐵 → ( 𝐴 −ℎ 𝐵 ) = 0ℎ )
24	19 23	impbii	⊢ ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = 𝐵 )