Theorem 2idllidld

Description: A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025)

	Ref	Expression
Hypothesis	2idllidld.1	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
Assertion	2idllidld	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		2idllidld.1	⊢ ( 𝜑 → 𝐼 ∈ ( 2Ideal ‘ 𝑅 ) )
2		eqid	⊢ ( LIdeal ‘ 𝑅 ) = ( LIdeal ‘ 𝑅 )
3		eqid	⊢ ( oppr ‘ 𝑅 ) = ( oppr ‘ 𝑅 )
4		eqid	⊢ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) = ( LIdeal ‘ ( oppr ‘ 𝑅 ) )
5		eqid	⊢ ( 2Ideal ‘ 𝑅 ) = ( 2Ideal ‘ 𝑅 )
6	2 3 4 5	2idlval	⊢ ( 2Ideal ‘ 𝑅 ) = ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) )
7	1 6	eleqtrdi	⊢ ( 𝜑 → 𝐼 ∈ ( ( LIdeal ‘ 𝑅 ) ∩ ( LIdeal ‘ ( oppr ‘ 𝑅 ) ) ) )
8	7	elin1d	⊢ ( 𝜑 → 𝐼 ∈ ( LIdeal ‘ 𝑅 ) )