Metamath Proof Explorer


Theorem drngui

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

Ref Expression
Hypotheses drngui.b B=BaseR
drngui.z 0˙=0R
drngui.r RDivRing
Assertion drngui B0˙=UnitR

Proof

Step Hyp Ref Expression
1 drngui.b B=BaseR
2 drngui.z 0˙=0R
3 drngui.r RDivRing
4 eqid UnitR=UnitR
5 1 4 2 isdrng RDivRingRRingUnitR=B0˙
6 3 5 mpbi RRingUnitR=B0˙
7 6 simpri UnitR=B0˙
8 7 eqcomi B0˙=UnitR