MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-2idl Structured version   Visualization version   GIF version

Definition df-2idl 18999
Description: Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.)
Assertion
Ref Expression
df-2idl 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))

Detailed syntax breakdown of Definition df-2idl
StepHypRef Expression
1 c2idl 18998 . 2 class 2Ideal
2 vr . . 3 setvar 𝑟
3 cvv 3172 . . 3 class V
42cv 1473 . . . . 5 class 𝑟
5 clidl 18937 . . . . 5 class LIdeal
64, 5cfv 5790 . . . 4 class (LIdeal‘𝑟)
7 coppr 18391 . . . . . 6 class oppr
84, 7cfv 5790 . . . . 5 class (oppr𝑟)
98, 5cfv 5790 . . . 4 class (LIdeal‘(oppr𝑟))
106, 9cin 3538 . . 3 class ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟)))
112, 3, 10cmpt 4637 . 2 class (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
121, 11wceq 1474 1 wff 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
Colors of variables: wff setvar class
This definition is referenced by:  2idlval  19000
  Copyright terms: Public domain W3C validator