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 ‘ 𝑟 ) } ) } |
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 ‘ 𝑟 ) } ) } |