Metamath Proof Explorer

Definition df-drngo

Description: Define the class of all division rings (sometimes called skew fields). A division ring is a unital ring where every element except the additive identity has a multiplicative inverse. (Contributed by NM, 4-Apr-2009) (New usage is discouraged.)

Ref Expression
Assertion df-drngo ⊢ DivRingOps = g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdrng class DivRingOps
1 vg setvar g
2 vh setvar h
3 1 cv setvar g
4 2 cv setvar h
5 3 4 cop class g h
6 crngo class RingOps
7 5 6 wcel wff g h ∈ RingOps
8 3 crn class ran ⁡ g
9 cgi class GId
10 3 9 cfv class GId ⁡ g
11 10 csn class GId ⁡ g
12 8 11 cdif class ran ⁡ g ∖ GId ⁡ g
13 12 12 cxp class ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g
14 4 13 cres class h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g
15 cgr class GrpOp
16 14 15 wcel wff h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp
17 7 16 wa wff g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp
18 17 1 2 copab class g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp
19 0 18 wceq wff DivRingOps = g h | g h ∈ RingOps ∧ h ↾ ran ⁡ g ∖ GId ⁡ g × ran ⁡ g ∖ GId ⁡ g ∈ GrpOp