Metamath Proof Explorer


Theorem ring0cl

Description: The zero element of a ring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014)

Ref Expression
Hypotheses ring0cl.b B=BaseR
ring0cl.z 0˙=0R
Assertion ring0cl RRing0˙B

Proof

Step Hyp Ref Expression
1 ring0cl.b B=BaseR
2 ring0cl.z 0˙=0R
3 ringgrp RRingRGrp
4 1 2 grpidcl RGrp0˙B
5 3 4 syl RRing0˙B