Theorem hvsubaddi

Description: Relationship between vector subtraction and addition. (Contributed by NM, 11-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	|- A e. ~H
	hvnegdi.2	|- B e. ~H
	hvaddcan.3	|- C e. ~H
Assertion	hvsubaddi	|- ( ( A -h B ) = C <-> ( B +h C ) = A )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	|- A e. ~H
2		hvnegdi.2	|- B e. ~H
3		hvaddcan.3	|- C e. ~H
4	1 2	hvsubvali	|- ( A -h B ) = ( A +h ( -u 1 .h B ) )
5	4	eqeq1i	|- ( ( A -h B ) = C <-> ( A +h ( -u 1 .h B ) ) = C )
6		neg1cn	|- -u 1 e. CC
7	6 2	hvmulcli	|- ( -u 1 .h B ) e. ~H
8	2 1 7	hvadd12i	|- ( B +h ( A +h ( -u 1 .h B ) ) ) = ( A +h ( B +h ( -u 1 .h B ) ) )
9	2	hvnegidi	|- ( B +h ( -u 1 .h B ) ) = 0h
10	9	oveq2i	|- ( A +h ( B +h ( -u 1 .h B ) ) ) = ( A +h 0h )
11		ax-hvaddid	|- ( A e. ~H -> ( A +h 0h ) = A )
12	1 11	ax-mp	|- ( A +h 0h ) = A
13	8 10 12	3eqtri	|- ( B +h ( A +h ( -u 1 .h B ) ) ) = A
14	13	eqeq1i	|- ( ( B +h ( A +h ( -u 1 .h B ) ) ) = ( B +h C ) <-> A = ( B +h C ) )
15	1 7	hvaddcli	|- ( A +h ( -u 1 .h B ) ) e. ~H
16	2 15 3	hvaddcani	|- ( ( B +h ( A +h ( -u 1 .h B ) ) ) = ( B +h C ) <-> ( A +h ( -u 1 .h B ) ) = C )
17		eqcom	|- ( A = ( B +h C ) <-> ( B +h C ) = A )
18	14 16 17	3bitr3i	|- ( ( A +h ( -u 1 .h B ) ) = C <-> ( B +h C ) = A )
19	5 18	bitri	|- ( ( A -h B ) = C <-> ( B +h C ) = A )