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 V I NrmGrp

Proof

Step Hyp Ref Expression
1 eqid I = I
2 eqid Base I = Base I
3 1 2 rrxcph I V I CPreHil
4 cphngp I CPreHil I NrmGrp
5 3 4 syl I V I NrmGrp