Theorem hvsubcan2i

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

	Ref	Expression
Hypotheses	hvnegdi.1	⊢ 𝐴 ∈ ℋ
	hvnegdi.2	⊢ 𝐵 ∈ ℋ
Assertion	hvsubcan2i	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 2 ·ℎ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		hvnegdi.1	⊢ 𝐴 ∈ ℋ
2		hvnegdi.2	⊢ 𝐵 ∈ ℋ
3	1 2	hvsubvali	⊢ ( 𝐴 −ℎ 𝐵 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) )
4	3	oveq2i	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
5		neg1cn	⊢ - 1 ∈ ℂ
6	5 2	hvmulcli	⊢ ( - 1 ·ℎ 𝐵 ) ∈ ℋ
7	1 2 1 6	hvadd4i	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 𝐴 +ℎ 𝐴 ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) )
8		hv2times	⊢ ( 𝐴 ∈ ℋ → ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 ) )
9	1 8	ax-mp	⊢ ( 2 ·ℎ 𝐴 ) = ( 𝐴 +ℎ 𝐴 )
10	9	eqcomi	⊢ ( 𝐴 +ℎ 𝐴 ) = ( 2 ·ℎ 𝐴 )
11	2	hvnegidi	⊢ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) = 0ℎ
12	10 11	oveq12i	⊢ ( ( 𝐴 +ℎ 𝐴 ) +ℎ ( 𝐵 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ )
13	7 12	eqtri	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ )
14		2cn	⊢ 2 ∈ ℂ
15	14 1	hvmulcli	⊢ ( 2 ·ℎ 𝐴 ) ∈ ℋ
16		ax-hvaddid	⊢ ( ( 2 ·ℎ 𝐴 ) ∈ ℋ → ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ ) = ( 2 ·ℎ 𝐴 ) )
17	15 16	ax-mp	⊢ ( ( 2 ·ℎ 𝐴 ) +ℎ 0ℎ ) = ( 2 ·ℎ 𝐴 )
18	13 17	eqtri	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 +ℎ ( - 1 ·ℎ 𝐵 ) ) ) = ( 2 ·ℎ 𝐴 )
19	4 18	eqtri	⊢ ( ( 𝐴 +ℎ 𝐵 ) +ℎ ( 𝐴 −ℎ 𝐵 ) ) = ( 2 ·ℎ 𝐴 )