Metamath Proof Explorer


Theorem drngmgp

Description: A division ring contains a multiplicative group. (Contributed by NM, 8-Sep-2011)

Ref Expression
Hypotheses drngmgp.b
|- B = ( Base ` R )
drngmgp.z
|- .0. = ( 0g ` R )
drngmgp.g
|- G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
Assertion drngmgp
|- ( R e. DivRing -> G e. Grp )

Proof

Step Hyp Ref Expression
1 drngmgp.b
 |-  B = ( Base ` R )
2 drngmgp.z
 |-  .0. = ( 0g ` R )
3 drngmgp.g
 |-  G = ( ( mulGrp ` R ) |`s ( B \ { .0. } ) )
4 1 2 3 isdrng2
 |-  ( R e. DivRing <-> ( R e. Ring /\ G e. Grp ) )
5 4 simprbi
 |-  ( R e. DivRing -> G e. Grp )