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

Metamath Proof Explorer

Theorem ridl1

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

Ref Expression
Hypotheses ridl0.u ⊢ U = LIdeal ⁡ opp r ⁡ R
ridl1.b ⊢ B = Base R
Assertion ridl1 ⊢ R ∈ Ring → B ∈ U

Proof

Step Hyp Ref Expression
1 ridl0.u ⊢ U = LIdeal ⁡ opp r ⁡ R
2 ridl1.b ⊢ B = Base R
3 eqid ⊢ opp r ⁡ R = opp r ⁡ R
4 3 opprring ⊢ R ∈ Ring → opp r ⁡ R ∈ Ring
5 3 2 opprbas ⊢ B = Base opp r ⁡ R
6 1 5 lidl1 ⊢ opp r ⁡ R ∈ Ring → B ∈ U
7 4 6 syl ⊢ R ∈ Ring → B ∈ U