Metamath Proof Explorer


Theorem nvgrp

Description: The vector addition operation of a normed complex vector space is a group. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypothesis nvabl.1 𝐺 = ( +𝑣𝑈 )
Assertion nvgrp ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )

Proof

Step Hyp Ref Expression
1 nvabl.1 𝐺 = ( +𝑣𝑈 )
2 1 nvablo ( 𝑈 ∈ NrmCVec → 𝐺 ∈ AbelOp )
3 ablogrpo ( 𝐺 ∈ AbelOp → 𝐺 ∈ GrpOp )
4 2 3 syl ( 𝑈 ∈ NrmCVec → 𝐺 ∈ GrpOp )