Theorem hvaddcani

Description: Cancellation law for vector 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	hvaddcani	|- ( ( A +h B ) = ( A +h C ) <-> B = C )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	|- A e. ~H
2		hvnegdi.2	|- B e. ~H
3		hvaddcan.3	|- C e. ~H
4		oveq1	|- ( ( A +h B ) = ( A +h C ) -> ( ( A +h B ) +h ( -u 1 .h A ) ) = ( ( A +h C ) +h ( -u 1 .h A ) ) )
5		neg1cn	|- -u 1 e. CC
6	5 1	hvmulcli	|- ( -u 1 .h A ) e. ~H
7	1 2 6	hvadd32i	|- ( ( A +h B ) +h ( -u 1 .h A ) ) = ( ( A +h ( -u 1 .h A ) ) +h B )
8	1	hvnegidi	|- ( A +h ( -u 1 .h A ) ) = 0h
9	8	oveq1i	|- ( ( A +h ( -u 1 .h A ) ) +h B ) = ( 0h +h B )
10	2	hvaddid2i	|- ( 0h +h B ) = B
11	7 9 10	3eqtri	|- ( ( A +h B ) +h ( -u 1 .h A ) ) = B
12	1 3 6	hvadd32i	|- ( ( A +h C ) +h ( -u 1 .h A ) ) = ( ( A +h ( -u 1 .h A ) ) +h C )
13	8	oveq1i	|- ( ( A +h ( -u 1 .h A ) ) +h C ) = ( 0h +h C )
14	3	hvaddid2i	|- ( 0h +h C ) = C
15	12 13 14	3eqtri	|- ( ( A +h C ) +h ( -u 1 .h A ) ) = C
16	4 11 15	3eqtr3g	|- ( ( A +h B ) = ( A +h C ) -> B = C )
17		oveq2	|- ( B = C -> ( A +h B ) = ( A +h C ) )
18	16 17	impbii	|- ( ( A +h B ) = ( A +h C ) <-> B = C )