Metamath Proof Explorer

Theorem nvmval2

Description: Value of vector subtraction on a normed complex vector space. (Contributed by Mario Carneiro, 19-Nov-2013) (New usage is discouraged.)

Ref Expression
Hypotheses nvmval.1 ⊢ X = BaseSet ⁡ U
nvmval.2 ⊢ G = + v ⁡ U
nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
nvmval.3 ⊢ M = - v ⁡ U
Assertion nvmval2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = -1 S B G A

Proof

Step Hyp Ref Expression
1 nvmval.1 ⊢ X = BaseSet ⁡ U
2 nvmval.2 ⊢ G = + v ⁡ U
3 nvmval.4 ⊢ S = ⋅ 𝑠OLD ⁡ U
4 nvmval.3 ⊢ M = - v ⁡ U
5 1 2 3 4 nvmval ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = A G -1 S B
6 neg1cn ⊢ − 1 ∈ ℂ
7 1 3 nvscl ⊢ U ∈ NrmCVec ∧ − 1 ∈ ℂ ∧ B ∈ X → -1 S B ∈ X
8 6 7 mp3an2 ⊢ U ∈ NrmCVec ∧ B ∈ X → -1 S B ∈ X
9 8 3adant2 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → -1 S B ∈ X
10 1 2 nvcom ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ -1 S B ∈ X → A G -1 S B = -1 S B G A
11 9 10 syld3an3 ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A G -1 S B = -1 S B G A
12 5 11 eqtrd ⊢ U ∈ NrmCVec ∧ A ∈ X ∧ B ∈ X → A M B = -1 S B G A