Metamath Proof Explorer


Theorem 2idl0

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

Ref Expression
Hypotheses 2idl0.u I=2IdealR
2idl0.z 0˙=0R
Assertion 2idl0 RRing0˙I

Proof

Step Hyp Ref Expression
1 2idl0.u I=2IdealR
2 2idl0.z 0˙=0R
3 eqid LIdealR=LIdealR
4 3 2 lidl0 RRing0˙LIdealR
5 eqid LIdealopprR=LIdealopprR
6 5 2 ridl0 RRing0˙LIdealopprR
7 4 6 elind RRing0˙LIdealRLIdealopprR
8 eqid opprR=opprR
9 3 8 5 1 2idlval I=LIdealRLIdealopprR
10 7 9 eleqtrrdi RRing0˙I