Metamath Proof Explorer

Theorem rrxngp

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

Ref Expression
Assertion rrxngp 
|- ( I e. V -> ( RR^ ` I ) e. NrmGrp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( RR^ ` I ) = ( RR^ ` I )
2 eqid 
 |-  ( Base ` ( RR^ ` I ) ) = ( Base ` ( RR^ ` I ) )
3 1 2 rrxcph 
 |-  ( I e. V -> ( RR^ ` I ) e. CPreHil )
4 cphngp 
 |-  ( ( RR^ ` I ) e. CPreHil -> ( RR^ ` I ) e. NrmGrp )
5 3 4 syl 
 |-  ( I e. V -> ( RR^ ` I ) e. NrmGrp )