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 e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) e. X )

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	|- X = ( BaseSet ` U )
2		nvmf.3	|- M = ( -v ` U )
3	1 2	nvmf	|- ( U e. NrmCVec -> M : ( X X. X ) --> X )
4		fovrn	|- ( ( M : ( X X. X ) --> X /\ A e. X /\ B e. X ) -> ( A M B ) e. X )
5	3 4	syl3an1	|- ( ( U e. NrmCVec /\ A e. X /\ B e. X ) -> ( A M B ) e. X )