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

Metamath Proof Explorer

Theorem nvmcl

Description: Closure law for the vector subtraction operation of a normed complex vector space. (Contributed by NM, 11-Sep-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvmf.1	$⊢ X = BaseSet (U)$
	nvmf.3	$⊢ M = -_{v} (U)$
Assertion	nvmcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M B \in X$

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	$⊢ X = BaseSet (U)$
2		nvmf.3	$⊢ M = -_{v} (U)$
3	1 2	nvmf	$⊢ U \in NrmCVec \to M : X \times X ⟶ X$
4		fovcdm	$⊢ (M : X \times X ⟶ X \land A \in X \land B \in X) \to A M B \in X$
5	3 4	syl3an1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A M B \in X$