Definition df-drngo 38803

Description: Obsolete defintion, use df-drng 20943 instead. 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 = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}

Distinct variable group:   𝑔,ℎ

Detailed syntax breakdown of Definition df-drngo

Step	Hyp	Ref	Expression
1		cdrng 38802	. 2 class DivRingOps
2		vg	. . . . . . 7 setvar 𝑔
3	2	cv 1569	. . . . . 6 class 𝑔
4		vh	. . . . . . 7 setvar ℎ
5	4	cv 1569	. . . . . 6 class ℎ
6	3, 5	cop 4589	. . . . 5 class ⟨𝑔, ℎ⟩
7		crngo 38748	. . . . 5 class RingOps
8	6, 7	wcel 2145	. . . 4 wff ⟨𝑔, ℎ⟩ ∈ RingOps
9	3	crn 5648	. . . . . . . 8 class ran 𝑔
10		cgi 31025	. . . . . . . . . 10 class GId
11	3, 10	cfv 6527	. . . . . . . . 9 class (GId‘𝑔)
12	11	csn 4583	. . . . . . . 8 class {(GId‘𝑔)}
13	9, 12	cdif 3895	. . . . . . 7 class (ran 𝑔 ∖ {(GId‘𝑔)})
14	13, 13	cxp 5645	. . . . . 6 class ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))
15	5, 14	cres 5649	. . . . 5 class (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)})))
16		cgr 31024	. . . . 5 class GrpOp
17	15, 16	wcel 2145	. . . 4 wff (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp
18	8, 17	wa 401	. . 3 wff (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)
19	18, 2, 4	copab 5166	. 2 class {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}
20	1, 19	wceq 1570	1 wff DivRingOps = {⟨𝑔, ℎ⟩ ∣ (⟨𝑔, ℎ⟩ ∈ RingOps ∧ (ℎ ↾ ((ran 𝑔 ∖ {(GId‘𝑔)}) × (ran 𝑔 ∖ {(GId‘𝑔)}))) ∈ GrpOp)}

This definition is used by:  isdivrngo  38804  drngoi  38805  isdrngo1  38810