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

Metamath Proof Explorer

Theorem nvgcl

Description: Closure law for the vector addition (group) operation of a normed complex vector space. (Contributed by NM, 23-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypotheses nvgcl.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
nvgcl.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
Assertion nvgcl ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )

Proof

Step Hyp Ref Expression
1 nvgcl.1 ⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2 nvgcl.2 ⊢ 𝐺 = ( +𝑣 ‘ 𝑈 )
3 2 nvgrp ⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )
4 1 2 bafval ⊢ 𝑋 = ran 𝐺
5 4 grpocl ⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )
6 3 5 syl3an1 ⊢ ( ( 𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐺 𝐵 ) ∈ 𝑋 )