Theorem drngmgp

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

	Ref	Expression
Hypotheses	drngmgp.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngmgp.z	⊢ 0 = ( 0g ‘ 𝑅 )
	drngmgp.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
Assertion	drngmgp	⊢ ( 𝑅 ∈ DivRing → 𝐺 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		drngmgp.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngmgp.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngmgp.g	⊢ 𝐺 = ( ( mulGrp ‘ 𝑅 ) ↾s ( 𝐵 ∖ { 0 } ) )
4	1 2 3	isdrng2	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝐺 ∈ Grp ) )
5	4	simprbi	⊢ ( 𝑅 ∈ DivRing → 𝐺 ∈ Grp )