Theorem drngmgp

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

	Ref	Expression
Hypotheses	drngmgp.b	$$⊢B={\mathrm{Base}}_R$$
	drngmgp.z	$$⊢\underset{\dot{}}{0}=0_R$$
	drngmgp.g	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
Assertion	drngmgp	$$⊢R\in \mathrm{DivRing}\to G\in \mathrm{Grp}$$

Proof

Step	Hyp	Ref	Expression
1		drngmgp.b	$$⊢B={\mathrm{Base}}_R$$
2		drngmgp.z	$$⊢\underset{\dot{}}{0}=0_R$$
3		drngmgp.g	$$⊢G={\mathrm{mulGrp}}_R{\upharpoonright }_{𝑠}\left(B\setminus \left\{\underset{\dot{}}{0}\right\}\right)$$
4	1 2 3	isdrng2	$$⊢R\in \mathrm{DivRing}\leftrightarrow \left(R\in \mathrm{Ring}\wedge G\in \mathrm{Grp}\right)$$
5	4	simprbi	$$⊢R\in \mathrm{DivRing}\to G\in \mathrm{Grp}$$