Theorem hvsubid

Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubid	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = 0ℎ )

Proof

Step	Hyp	Ref	Expression
1		ax-hvmulid	⊢ ( 𝐴 ∈ ℋ → ( 1 ·ℎ 𝐴 ) = 𝐴 )
2	1	oveq1d	⊢ ( 𝐴 ∈ ℋ → ( ( 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) )
3		ax-1cn	⊢ 1 ∈ ℂ
4		neg1cn	⊢ - 1 ∈ ℂ
5		ax-hvdistr2	⊢ ( ( 1 ∈ ℂ ∧ - 1 ∈ ℂ ∧ 𝐴 ∈ ℋ ) → ( ( 1 + - 1 ) ·ℎ 𝐴 ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) )
6	3 4 5	mp3an12	⊢ ( 𝐴 ∈ ℋ → ( ( 1 + - 1 ) ·ℎ 𝐴 ) = ( ( 1 ·ℎ 𝐴 ) +ℎ ( - 1 ·ℎ 𝐴 ) ) )
7		hvsubval	⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ ) → ( 𝐴 −ℎ 𝐴 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) )
8	7	anidms	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = ( 𝐴 +ℎ ( - 1 ·ℎ 𝐴 ) ) )
9	2 6 8	3eqtr4rd	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = ( ( 1 + - 1 ) ·ℎ 𝐴 ) )
10		1pneg1e0	⊢ ( 1 + - 1 ) = 0
11	10	oveq1i	⊢ ( ( 1 + - 1 ) ·ℎ 𝐴 ) = ( 0 ·ℎ 𝐴 )
12	9 11	eqtrdi	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = ( 0 ·ℎ 𝐴 ) )
13		ax-hvmul0	⊢ ( 𝐴 ∈ ℋ → ( 0 ·ℎ 𝐴 ) = 0ℎ )
14	12 13	eqtrd	⊢ ( 𝐴 ∈ ℋ → ( 𝐴 −ℎ 𝐴 ) = 0ℎ )