This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2idlridld

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

Ref Expression
Hypotheses 2idllidld.1 ⊢ φ → I ∈ 2Ideal ⁡ R
2idlridld.o ⊢ O = opp r ⁡ R
Assertion 2idlridld ⊢ φ → I ∈ LIdeal ⁡ O

Proof

Step Hyp Ref Expression
1 2idllidld.1 ⊢ φ → I ∈ 2Ideal ⁡ R
2 2idlridld.o ⊢ O = opp r ⁡ R
3 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
4 eqid ⊢ LIdeal ⁡ O = LIdeal ⁡ O
5 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
6 3 2 4 5 2idlval ⊢ 2Ideal ⁡ R = LIdeal ⁡ R ∩ LIdeal ⁡ O
7 1 6 eleqtrdi ⊢ φ → I ∈ LIdeal ⁡ R ∩ LIdeal ⁡ O
8 7 elin2d ⊢ φ → I ∈ LIdeal ⁡ O