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 = \cdot_{𝑠OLD} (U)$
		nvmval.3	$⊢ M = -_{v} (U)$
	Assertion	nvmval2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to 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 = \cdot_{𝑠OLD} (U)$
4		nvmval.3	$⊢ M = -_{v} (U)$
5	1 2 3 4	nvmval	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M B = A G (-1 S B)$
6		neg1cn	$⊢ - 1 \in ℂ$
7	1 3	nvscl	$⊢ (U \in NrmCVec \land - 1 \in ℂ \land B \in X) \to -1 S B \in X$
8	6 7	mp3an2	$⊢ (U \in NrmCVec \land B \in X) \to -1 S B \in X$
9	8	3adant2	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to -1 S B \in X$
10	1 2	nvcom	$⊢ (U \in NrmCVec \land A \in X \land -1 S B \in X) \to A G (-1 S B) = (-1 S B) G A$
11	9 10	syld3an3	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G (-1 S B) = (-1 S B) G A$
12	5 11	eqtrd	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M B = (-1 S B) G A$