Theorem hvm1neg

Description: Convert minus one times a scalar product to the negative of the scalar. (Contributed by NM, 4-Jun-2004) (New usage is discouraged.)

	Ref	Expression
Assertion	hvm1neg	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) = ( - 𝐴 ·ℎ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		neg1cn	⊢ - 1 ∈ ℂ
2		ax-hvmulass	⊢ ( ( - 1 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( - 1 · 𝐴 ) ·ℎ 𝐵 ) = ( - 1 ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) )
3	1 2	mp3an1	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( - 1 · 𝐴 ) ·ℎ 𝐵 ) = ( - 1 ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) )
4		mulm1	⊢ ( 𝐴 ∈ ℂ → ( - 1 · 𝐴 ) = - 𝐴 )
5	4	adantr	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 · 𝐴 ) = - 𝐴 )
6	5	oveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( - 1 · 𝐴 ) ·ℎ 𝐵 ) = ( - 𝐴 ·ℎ 𝐵 ) )
7	3 6	eqtr3d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ ) → ( - 1 ·ℎ ( 𝐴 ·ℎ 𝐵 ) ) = ( - 𝐴 ·ℎ 𝐵 ) )