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 ) ) )