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 𝐵 = ( Base ‘ 𝑅 )
isdrng.u 𝑈 = ( Unit ‘ 𝑅 )
isdrng.z 0 = ( 0g𝑅 )
Assertion drngunit ( 𝑅 ∈ DivRing → ( 𝑋𝑈 ↔ ( 𝑋𝐵𝑋0 ) ) )

Proof

Step Hyp Ref Expression
1 isdrng.b 𝐵 = ( Base ‘ 𝑅 )
2 isdrng.u 𝑈 = ( Unit ‘ 𝑅 )
3 isdrng.z 0 = ( 0g𝑅 )
4 1 2 3 isdrng ( 𝑅 ∈ DivRing ↔ ( 𝑅 ∈ Ring ∧ 𝑈 = ( 𝐵 ∖ { 0 } ) ) )
5 4 simprbi ( 𝑅 ∈ DivRing → 𝑈 = ( 𝐵 ∖ { 0 } ) )
6 5 eleq2d ( 𝑅 ∈ DivRing → ( 𝑋𝑈𝑋 ∈ ( 𝐵 ∖ { 0 } ) ) )
7 eldifsn ( 𝑋 ∈ ( 𝐵 ∖ { 0 } ) ↔ ( 𝑋𝐵𝑋0 ) )
8 6 7 bitrdi ( 𝑅 ∈ DivRing → ( 𝑋𝑈 ↔ ( 𝑋𝐵𝑋0 ) ) )