This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ A ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ A ⋅ ℎ B = − A ⋅ ℎ B

Proof

Step Hyp Ref Expression
1 neg1cn ⊢ − 1 ∈ ℂ
2 ax-hvmulass ⊢ − 1 ∈ ℂ ∧ A ∈ ℂ ∧ B ∈ ℋ → -1 ⁢ A ⋅ ℎ B = -1 ⋅ ℎ A ⋅ ℎ B
3 1 2 mp3an1 ⊢ A ∈ ℂ ∧ B ∈ ℋ → -1 ⁢ A ⋅ ℎ B = -1 ⋅ ℎ A ⋅ ℎ B
4 mulm1 ⊢ A ∈ ℂ → -1 ⁢ A = − A
5 4 adantr ⊢ A ∈ ℂ ∧ B ∈ ℋ → -1 ⁢ A = − A
6 5 oveq1d ⊢ A ∈ ℂ ∧ B ∈ ℋ → -1 ⁢ A ⋅ ℎ B = − A ⋅ ℎ B
7 3 6 eqtr3d ⊢ A ∈ ℂ ∧ B ∈ ℋ → -1 ⋅ ℎ A ⋅ ℎ B = − A ⋅ ℎ B