Metamath Proof Explorer


Theorem lidl0

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

Ref Expression
Hypotheses rnglidl0.u U = LIdeal R
rnglidl0.z 0 ˙ = 0 R
Assertion lidl0 R Ring 0 ˙ U

Proof

Step Hyp Ref Expression
1 rnglidl0.u U = LIdeal R
2 rnglidl0.z 0 ˙ = 0 R
3 ringrng R Ring R Rng
4 1 2 rnglidl0 R Rng 0 ˙ U
5 3 4 syl R Ring 0 ˙ U