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=\mathrm{BaseSet}\left(U\right)$$
	nvmf.3	$$⊢M={-}_v\left(U\right)$$
Assertion	nvmcl	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to AMB\in X$$

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvmf.3	$$⊢M={-}_v\left(U\right)$$
3	1 2	nvmf	$$⊢U\in \mathrm{NrmCVec}\to M:X\times X⟶X$$
4		fovcdm	$$⊢\left(M:X\times X⟶X\wedge A\in X\wedge B\in X\right)\to AMB\in X$$
5	3 4	syl3an1	$$⊢\left(U\in \mathrm{NrmCVec}\wedge A\in X\wedge B\in X\right)\to AMB\in X$$