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 = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cdrng	⊢ DivRingOps
1		vg	⊢ 𝑔
2		vh	⊢ ℎ
3	1	cv	⊢ 𝑔
4	2	cv	⊢ ℎ
5	3 4	cop	⊢ ⟨ 𝑔 , ℎ ⟩
6		crngo	⊢ RingOps
7	5 6	wcel	⊢ ⟨ 𝑔 , ℎ ⟩ ∈ RingOps
8	3	crn	⊢ ran 𝑔
9		cgi	⊢ GId
10	3 9	cfv	⊢ ( GId ‘ 𝑔 )
11	10	csn	⊢ { ( GId ‘ 𝑔 ) }
12	8 11	cdif	⊢ ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } )
13	12 12	cxp	⊢ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) )
14	4 13	cres	⊢ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) )
15		cgr	⊢ GrpOp
16	14 15	wcel	⊢ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp
17	7 16	wa	⊢ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp )
18	17 1 2	copab	⊢ { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }
19	0 18	wceq	⊢ DivRingOps = { ⟨ 𝑔 , ℎ ⟩ ∣ ( ⟨ 𝑔 , ℎ ⟩ ∈ RingOps ∧ ( ℎ ↾ ( ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) × ( ran 𝑔 ∖ { ( GId ‘ 𝑔 ) } ) ) ) ∈ GrpOp ) }