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 ) |
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 ) |