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	|- A e. ~H
	hvnegdi.2	|- B e. ~H
Assertion	hvsubeq0i	|- ( ( A -h B ) = 0h <-> A = B )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	|- A e. ~H
2		hvnegdi.2	|- B e. ~H
3	1 2	hvsubvali	|- ( A -h B ) = ( A +h ( -u 1 .h B ) )
4	3	eqeq1i	|- ( ( A -h B ) = 0h <-> ( A +h ( -u 1 .h B ) ) = 0h )
5		oveq1	|- ( ( A +h ( -u 1 .h B ) ) = 0h -> ( ( A +h ( -u 1 .h B ) ) +h B ) = ( 0h +h B ) )
6	4 5	sylbi	|- ( ( A -h B ) = 0h -> ( ( A +h ( -u 1 .h B ) ) +h B ) = ( 0h +h B ) )
7		neg1cn	|- -u 1 e. CC
8	7 2	hvmulcli	|- ( -u 1 .h B ) e. ~H
9	1 8 2	hvadd32i	|- ( ( A +h ( -u 1 .h B ) ) +h B ) = ( ( A +h B ) +h ( -u 1 .h B ) )
10	1 2 8	hvassi	|- ( ( A +h B ) +h ( -u 1 .h B ) ) = ( A +h ( B +h ( -u 1 .h B ) ) )
11	2	hvnegidi	|- ( B +h ( -u 1 .h B ) ) = 0h
12	11	oveq2i	|- ( A +h ( B +h ( -u 1 .h B ) ) ) = ( A +h 0h )
13		ax-hvaddid	|- ( A e. ~H -> ( A +h 0h ) = A )
14	1 13	ax-mp	|- ( A +h 0h ) = A
15	12 14	eqtri	|- ( A +h ( B +h ( -u 1 .h B ) ) ) = A
16	10 15	eqtri	|- ( ( A +h B ) +h ( -u 1 .h B ) ) = A
17	9 16	eqtri	|- ( ( A +h ( -u 1 .h B ) ) +h B ) = A
18	2	hvaddid2i	|- ( 0h +h B ) = B
19	6 17 18	3eqtr3g	|- ( ( A -h B ) = 0h -> A = B )
20		oveq1	|- ( A = B -> ( A -h B ) = ( B -h B ) )
21		hvsubid	|- ( B e. ~H -> ( B -h B ) = 0h )
22	2 21	ax-mp	|- ( B -h B ) = 0h
23	20 22	eqtrdi	|- ( A = B -> ( A -h B ) = 0h )
24	19 23	impbii	|- ( ( A -h B ) = 0h <-> A = B )