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

Definition df-2idl 19280
 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 19279 . 2 class 2Ideal
2 vr . . 3 setvar 𝑟
3 cvv 3231 . . 3 class V
42cv 1522 . . . . 5 class 𝑟
5 clidl 19218 . . . . 5 class LIdeal
64, 5cfv 5926 . . . 4 class (LIdeal‘𝑟)
7 coppr 18668 . . . . . 6 class oppr
84, 7cfv 5926 . . . . 5 class (oppr𝑟)
98, 5cfv 5926 . . . 4 class (LIdeal‘(oppr𝑟))
106, 9cin 3606 . . 3 class ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟)))
112, 3, 10cmpt 4762 . 2 class (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
121, 11wceq 1523 1 wff 2Ideal = (𝑟 ∈ V ↦ ((LIdeal‘𝑟) ∩ (LIdeal‘(oppr𝑟))))
 Colors of variables: wff setvar class This definition is referenced by:  2idlval  19281
 Copyright terms: Public domain W3C validator