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 21104
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 21103 . 2 class 2Ideal
2 vr . . 3 setvar 𝑟
3 cvv 3468 . . 3 class V
42cv 1532 . . . . 5 class 𝑟
5 clidl 21062 . . . . 5 class LIdeal
64, 5cfv 6536 . . . 4 class (LIdeal‘𝑟)
7 coppr 20232 . . . . . 6 class oppr
84, 7cfv 6536 . . . . 5 class (oppr𝑟)
98, 5cfv 6536 . . . 4 class (LIdeal‘(oppr𝑟))
106, 9cin 3942 . . 3 class ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟)))
112, 3, 10cmpt 5224 . 2 class (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
121, 11wceq 1533 1 wff 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
Colors of variables: wff setvar class
This definition is referenced by:  2idlval  21105
  Copyright terms: Public domain W3C validator