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 = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 cdrng 
 |-  DivRingOps
1 vg 
 |-  g
2 vh 
 |-  h
3 1 cv 
 |-  g
4 2 cv 
 |-  h
5 3 4 cop 
 |-  <. g , h >.
6 crngo 
 |-  RingOps
7 5 6 wcel 
 |-  <. g , h >. e. RingOps
8 3 crn 
 |-  ran g
9 cgi 
 |-  GId
10 3 9 cfv 
 |-  ( GId ` g )
11 10 csn 
 |-  { ( GId ` g ) }
12 8 11 cdif 
 |-  ( ran g \ { ( GId ` g ) } )
13 12 12 cxp 
 |-  ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) )
14 4 13 cres 
 |-  ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) )
15 cgr 
 |-  GrpOp
16 14 15 wcel 
 |-  ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp
17 7 16 wa 
 |-  ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp )
18 17 1 2 copab 
 |-  { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }
19 0 18 wceq 
 |-  DivRingOps = { <. g , h >. | ( <. g , h >. e. RingOps /\ ( h |` ( ( ran g \ { ( GId ` g ) } ) X. ( ran g \ { ( GId ` g ) } ) ) ) e. GrpOp ) }