Metamath Proof Explorer


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