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