Metamath Proof Explorer


Definition df-drng

Description: Define class of all division rings. A division ring is a ring in which the set of units is exactly the nonzero elements of the ring. (Contributed by NM, 18-Oct-2012)

Ref Expression
Assertion df-drng DivRing = { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g𝑟 ) } ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdr DivRing
1 vr 𝑟
2 crg Ring
3 cui Unit
4 1 cv 𝑟
5 4 3 cfv ( Unit ‘ 𝑟 )
6 cbs Base
7 4 6 cfv ( Base ‘ 𝑟 )
8 c0g 0g
9 4 8 cfv ( 0g𝑟 )
10 9 csn { ( 0g𝑟 ) }
11 7 10 cdif ( ( Base ‘ 𝑟 ) ∖ { ( 0g𝑟 ) } )
12 5 11 wceq ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g𝑟 ) } )
13 12 1 2 crab { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g𝑟 ) } ) }
14 0 13 wceq DivRing = { 𝑟 ∈ Ring ∣ ( Unit ‘ 𝑟 ) = ( ( Base ‘ 𝑟 ) ∖ { ( 0g𝑟 ) } ) }