Definition df-drng 9492

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.

Assertion

Ref	Expression
df-drng	|- DivRing = {<.g, h>. | (<.g, h>. e. Ring /\ (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp)}

Distinct variable group:   g,h

Detailed syntax breakdown of Definition df-drng

Step	Hyp	Ref	Expression
1		cdrng 9491	. 2 class DivRing
2		vg	. . . . . . 7 set g
3	2	cv 1297	. . . . . 6 class g
4		vh	. . . . . . 7 set h
5	4	cv 1297	. . . . . 6 class h
6	3, 5	cop 3046	. . . . 5 class <.g, h>.
7		cring 9463	. . . . 5 class Ring
8	6, 7	wcel 1300	. . . 4 wff <.g, h>. e. Ring
9	3	crn 3987	. . . . . . . 8 class ran g
10		cgi 9312	. . . . . . . . . 10 class Id
11	3, 10	cfv 3998	. . . . . . . . 9 class (Id` g)
12	11	csn 3044	. . . . . . . 8 class {(Id` g)}
13	9, 12	cdif 2590	. . . . . . 7 class (ran g \ {(Id` g)})
14	13, 13	cxp 3984	. . . . . 6 class ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))
15	5, 14	cres 3988	. . . . 5 class (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)})))
16		cgr 9311	. . . . 5 class Grp
17	15, 16	wcel 1300	. . . 4 wff (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp
18	8, 17	wa 240	. . 3 wff (<.g, h>. e. Ring /\ (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp)
19	18, 2, 4	copab 3395	. 2 class {<.g, h>. | (<.g, h>. e. Ring /\ (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp)}
20	1, 19	wceq 1298	1 wff DivRing = {<.g, h>. | (<.g, h>. e. Ring /\ (h |` ((ran g \ {(Id` g)}) X. (ran g \ {(Id` g)}))) e. Grp)}

This definition is referenced by:  drngi 9493  isdivrng 10417  isdivrng1 16109

Copyright terms: Public domain