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 NrmCVec A X B X A G B X


Step Hyp Ref Expression
1 nvgcl.1 X = BaseSet U
2 nvgcl.2 G = + v U
3 2 nvgrp U NrmCVec G GrpOp
4 1 2 bafval X = ran G
5 4 grpocl G GrpOp A X B X A G B X
6 3 5 syl3an1 U NrmCVec A X B X A G B X