Theorem drngui

Description: The set of units of a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)

	Ref	Expression
Hypotheses	drngui.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	drngui.z	⊢ 0 = ( 0g ‘ 𝑅 )
	drngui.r	⊢ 𝑅 ∈ DivRing
Assertion	drngui	⊢ ( 𝐵 ∖ { 0 } ) = ( Unit ‘ 𝑅 )

Proof

Step	Hyp	Ref	Expression
1		drngui.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		drngui.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		drngui.r	⊢ 𝑅 ∈ DivRing
4		eqid	⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
5	1 4 2	isdrng	⊢ ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) ) )
6	3 5	mpbi	⊢ ( 𝑅 ∈ Ring ∧ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } ) )
7	6	simpri	⊢ ( Unit ‘ 𝑅 ) = ( 𝐵 ∖ { 0 } )
8	7	eqcomi	⊢ ( 𝐵 ∖ { 0 } ) = ( Unit ‘ 𝑅 )