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

Metamath Proof Explorer

Theorem 2idl1

Description: Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025)

Ref Expression
Hypotheses 2idl0.u ⊢ I = 2Ideal ⁡ R
2idl1.b ⊢ B = Base R
Assertion 2idl1 ⊢ R ∈ Ring → B ∈ I

Proof

Step Hyp Ref Expression
1 2idl0.u ⊢ I = 2Ideal ⁡ R
2 2idl1.b ⊢ B = Base R
3 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
4 3 2 lidl1 ⊢ R ∈ Ring → B ∈ LIdeal ⁡ R
5 eqid ⊢ LIdeal ⁡ opp r ⁡ R = LIdeal ⁡ opp r ⁡ R
6 5 2 ridl1 ⊢ R ∈ Ring → B ∈ LIdeal ⁡ opp r ⁡ R
7 4 6 elind ⊢ R ∈ Ring → B ∈ LIdeal ⁡ R ∩ LIdeal ⁡ opp r ⁡ R
8 eqid ⊢ opp r ⁡ R = opp r ⁡ R
9 3 8 5 1 2idlval ⊢ I = LIdeal ⁡ R ∩ LIdeal ⁡ opp r ⁡ R
10 7 9 eleqtrrdi ⊢ R ∈ Ring → B ∈ I