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


Step Hyp Ref Expression
1 nvmf.1 X = BaseSet U
2 nvmf.3 M = - v U
3 1 2 nvmf U NrmCVec M : X × X X
4 fovrn M : X × X X A X B X A M B X
5 3 4 syl3an1 U NrmCVec A X B X A M B X