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

Metamath Proof Explorer

Theorem lidl1

Description: Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015) (Proof shortened by AV, 18-Apr-2025)

Ref Expression
Hypotheses rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
rnglidl1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
Assertion lidl1 ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )

Proof

Step Hyp Ref Expression
1 rnglidl0.u ⊢ 𝑈 = ( LIdeal ‘ 𝑅 )
2 rnglidl1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 ringrng ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Rng )
4 1 2 rnglidl1 ⊢ ( 𝑅 ∈ Rng → 𝐵 ∈ 𝑈 )
5 3 4 syl ⊢ ( 𝑅 ∈ Ring → 𝐵 ∈ 𝑈 )