Definition df-2idl

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)

	Ref	Expression
Assertion	df-2idl	⊢ 2Ideal = ( 𝑟 ∈ V ↦ ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c2idl	⊢ 2Ideal
1		vr	⊢ 𝑟
2		cvv	⊢ V
3		clidl	⊢ LIdeal
4	1	cv	⊢ 𝑟
5	4 3	cfv	⊢ ( LIdeal ‘ 𝑟 )
6		coppr	⊢ oppr
7	4 6	cfv	⊢ ( oppr ‘ 𝑟 )
8	7 3	cfv	⊢ ( LIdeal ‘ ( oppr ‘ 𝑟 ) )
9	5 8	cin	⊢ ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) )
10	1 2 9	cmpt	⊢ ( 𝑟 ∈ V ↦ ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) ) )
11	0 10	wceq	⊢ 2Ideal = ( 𝑟 ∈ V ↦ ( ( LIdeal ‘ 𝑟 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑟 ) ) ) )