Metamath Proof Explorer


Theorem trggrp

Description: A topological ring is a group. (Contributed by Mario Carneiro, 5-Oct-2015)

Ref Expression
Assertion trggrp
|- ( R e. TopRing -> R e. Grp )

Proof

Step Hyp Ref Expression
1 trgring
 |-  ( R e. TopRing -> R e. Ring )
2 ringgrp
 |-  ( R e. Ring -> R e. Grp )
3 1 2 syl
 |-  ( R e. TopRing -> R e. Grp )