Definition df-drngo 26134

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

Assertion

Ref	Expression
df-drngo	|- DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp ) }

Distinct variable group:   g, h

Detailed syntax breakdown of Definition df-drngo

Step	Hyp	Ref	Expression
1		cdrng 26133	. 2 class DivRingOps
2		vg	. . . . . . 7 setvar g
3	2	cv 1443	. . . . . 6 class g
4		vh	. . . . . . 7 setvar h
5	4	cv 1443	. . . . . 6 class h
6	3, 5	cop 3974	. . . . 5 class <. g , h >.
7		crngo 26103	. . . . 5 class RingOps
8	6, 7	wcel 1887	. . . 4 wff <. g , h >. e. RingOps
9	3	crn 4835	. . . . . . . 8 class ran g
10		cgi 25915	. . . . . . . . . 10 class GId
11	3, 10	cfv 5582	. . . . . . . . 9 class (GId ` g )
12	11	csn 3968	. . . . . . . 8 class { (GId ` g ) }
13	9, 12	cdif 3401	. . . . . . 7 class ( ran g \ { (GId ` g ) } )
14	13, 13	cxp 4832	. . . . . 6 class ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) )
15	5, 14	cres 4836	. . . . 5 class ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) )
16		cgr 25914	. . . . 5 class GrpOp
17	15, 16	wcel 1887	. . . 4 wff ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp
18	8, 17	wa 371	. . 3 wff ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp )
19	18, 2, 4	copab 4460	. 2 class { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp ) }
20	1, 19	wceq 1444	1 wff DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { (GId ` g ) } ) X. ( ran g \ { (GId ` g ) } ) ) ) e. GrpOp ) }

This definition is referenced by:  drngoi  26135  isdivrngo  26159  isdrngo1  32195