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 )