Theorem hvsubcan2i

Description: Vector cancellation law. (Contributed by NM, 3-Sep-1999) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hvnegdi.1	|- A e. ~H
	hvnegdi.2	|- B e. ~H
Assertion	hvsubcan2i	|- ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )

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	oveq2i	|- ( ( A +h B ) +h ( A -h B ) ) = ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) )
5		neg1cn	|- -u 1 e. CC
6	5 2	hvmulcli	|- ( -u 1 .h B ) e. ~H
7	1 2 1 6	hvadd4i	|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) )
8		hv2times	|- ( A e. ~H -> ( 2 .h A ) = ( A +h A ) )
9	1 8	ax-mp	|- ( 2 .h A ) = ( A +h A )
10	9	eqcomi	|- ( A +h A ) = ( 2 .h A )
11	2	hvnegidi	|- ( B +h ( -u 1 .h B ) ) = 0h
12	10 11	oveq12i	|- ( ( A +h A ) +h ( B +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h )
13	7 12	eqtri	|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( ( 2 .h A ) +h 0h )
14		2cn	|- 2 e. CC
15	14 1	hvmulcli	|- ( 2 .h A ) e. ~H
16		ax-hvaddid	|- ( ( 2 .h A ) e. ~H -> ( ( 2 .h A ) +h 0h ) = ( 2 .h A ) )
17	15 16	ax-mp	|- ( ( 2 .h A ) +h 0h ) = ( 2 .h A )
18	13 17	eqtri	|- ( ( A +h B ) +h ( A +h ( -u 1 .h B ) ) ) = ( 2 .h A )
19	4 18	eqtri	|- ( ( A +h B ) +h ( A -h B ) ) = ( 2 .h A )