Metamath Proof Explorer

Theorem nvablo

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

		Ref	Expression
	Hypothesis	nvabl.1	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
	Assertion	nvablo	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ AbelOp )

Proof

Step	Hyp	Ref	Expression
1		nvabl.1	⊢ 𝐺 = ( +_𝑣 ‘ 𝑈 )
2		eqid	⊢ ( 1^st ‘ 𝑈 ) = ( 1^st ‘ 𝑈 )
3	2	nvvc	⊢ ( 𝑈 ∈ NrmCVec → ( 1^st ‘ 𝑈 ) ∈ CVec_OLD )
4	1	vafval	⊢ 𝐺 = ( 1^st ‘ ( 1^st ‘ 𝑈 ) )
5	4	vcablo	⊢ ( ( 1^st ‘ 𝑈 ) ∈ CVec_OLD → 𝐺 ∈ AbelOp )
6	3 5	syl	⊢ ( 𝑈 ∈ NrmCVec → 𝐺 ∈ AbelOp )