Metamath Proof Explorer

Theorem 2idlelbas

Description: The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025)

Ref Expression
Hypotheses 2idlbas.i ⊢ φ → I ∈ 2Ideal ⁡ R
2idlbas.j ⊢ J = R ↾ 𝑠 I
2idlbas.b ⊢ B = Base J
Assertion 2idlelbas ⊢ φ → B ∈ LIdeal ⁡ R ∧ B ∈ LIdeal ⁡ opp r ⁡ R

Proof

Step Hyp Ref Expression
1 2idlbas.i ⊢ φ → I ∈ 2Ideal ⁡ R
2 2idlbas.j ⊢ J = R ↾ 𝑠 I
3 2idlbas.b ⊢ B = Base J
4 1 2 3 2idlbas ⊢ φ → B = I
5 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
6 eqid ⊢ opp r ⁡ R = opp r ⁡ R
7 eqid ⊢ LIdeal ⁡ opp r ⁡ R = LIdeal ⁡ opp r ⁡ R
8 eqid ⊢ 2Ideal ⁡ R = 2Ideal ⁡ R
9 5 6 7 8 2idlelb ⊢ I ∈ 2Ideal ⁡ R ↔ I ∈ LIdeal ⁡ R ∧ I ∈ LIdeal ⁡ opp r ⁡ R
10 9 simplbi ⊢ I ∈ 2Ideal ⁡ R → I ∈ LIdeal ⁡ R
11 1 10 syl ⊢ φ → I ∈ LIdeal ⁡ R
12 4 11 eqeltrd ⊢ φ → B ∈ LIdeal ⁡ R
13 9 simprbi ⊢ I ∈ 2Ideal ⁡ R → I ∈ LIdeal ⁡ opp r ⁡ R
14 1 13 syl ⊢ φ → I ∈ LIdeal ⁡ opp r ⁡ R
15 4 14 eqeltrd ⊢ φ → B ∈ LIdeal ⁡ opp r ⁡ R
16 12 15 jca ⊢ φ → B ∈ LIdeal ⁡ R ∧ B ∈ LIdeal ⁡ opp r ⁡ R