Metamath Proof Explorer

Theorem nvgcl

Description: Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvgcl.1	$⊢ X = BaseSet (U)$
	nvgcl.2	$⊢ G = +_{v} (U)$
Assertion	nvgcl	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$

Proof

Step	Hyp	Ref	Expression
1		nvgcl.1	$⊢ X = BaseSet (U)$
2		nvgcl.2	$⊢ G = +_{v} (U)$
3	2	nvgrp	$⊢ U \in NrmCVec \to G \in GrpOp$
4	1 2	bafval	$⊢ X = ran G$
5	4	grpocl	$⊢ (G \in GrpOp \land A \in X \land B \in X) \to A G B \in X$
6	3 5	syl3an1	$⊢ (U \in NrmCVec \land A \in X \land B \in X) \to A G B \in X$