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	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	nvmf.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
Assertion	nvmcl	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		nvmf.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		nvmf.3	⊢ 𝑀 = ( −𝑣 ‘ 𝑈 )
3	1 2	nvmf	⊢ ( 𝑈 ∈ NrmCVec → 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
4		fovrn	⊢ ( ( 𝑀 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 )
5	3 4	syl3an1	⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝑀 𝐵 ) ∈ 𝑋 )