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 )