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⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in 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⟩ \in 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)\}) \times (ran g ∖ \{GId (g)\}))$
14	4 13	cres	$class ({h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))})$
15		cgr	$class GrpOp$
16	14 15	wcel	$wff {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp$
17	7 16	wa	$wff (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)$
18	17 1 2	copab	$class \{⟨g, h⟩ \| (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)\}$
19	0 18	wceq	$wff DivRingOps = \{⟨g, h⟩ \| (⟨g, h⟩ \in RingOps \land {h ↾}_{((ran g ∖ \{GId (g)\}) \times (ran g ∖ \{GId (g)\}))} \in GrpOp)\}$

Metamath Proof Explorer

Definition df-drngo

Detailed syntax breakdown