Theorem rrxngp

Description: Generalized Euclidean real spaces are normed groups. (Contributed by Glauco Siliprandi, 24-Dec-2020)

	Ref	Expression
Assertion	rrxngp	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ NrmGrp )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ℝ^ ‘ 𝐼 ) = ( ℝ^ ‘ 𝐼 )
2		eqid	⊢ ( Base ‘ ( ℝ^ ‘ 𝐼 ) ) = ( Base ‘ ( ℝ^ ‘ 𝐼 ) )
3	1 2	rrxcph	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ ℂPreHil )
4		cphngp	⊢ ( ( ℝ^ ‘ 𝐼 ) ∈ ℂPreHil → ( ℝ^ ‘ 𝐼 ) ∈ NrmGrp )
5	3 4	syl	⊢ ( 𝐼 ∈ 𝑉 → ( ℝ^ ‘ 𝐼 ) ∈ NrmGrp )