Metamath Proof Explorer


Theorem drngunit

Description: Elementhood in the set of units when R is a division ring. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypotheses isdrng.b B = Base R
isdrng.u U = Unit R
isdrng.z 0 ˙ = 0 R
Assertion drngunit R DivRing X U X B X 0 ˙

Proof

Step Hyp Ref Expression
1 isdrng.b B = Base R
2 isdrng.u U = Unit R
3 isdrng.z 0 ˙ = 0 R
4 1 2 3 isdrng R DivRing R Ring U = B 0 ˙
5 4 simprbi R DivRing U = B 0 ˙
6 5 eleq2d R DivRing X U X B 0 ˙
7 eldifsn X B 0 ˙ X B X 0 ˙
8 6 7 bitrdi R DivRing X U X B X 0 ˙