This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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

Proof

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