This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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