Metamath Proof Explorer


Theorem srg0cl

Description: The zero element of a semiring belongs to its base set. (Contributed by Mario Carneiro, 12-Jan-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Hypotheses srg0cl.b
|- B = ( Base ` R )
srg0cl.z
|- .0. = ( 0g ` R )
Assertion srg0cl
|- ( R e. SRing -> .0. e. B )

Proof

Step Hyp Ref Expression
1 srg0cl.b
 |-  B = ( Base ` R )
2 srg0cl.z
 |-  .0. = ( 0g ` R )
3 srgmnd
 |-  ( R e. SRing -> R e. Mnd )
4 1 2 mndidcl
 |-  ( R e. Mnd -> .0. e. B )
5 3 4 syl
 |-  ( R e. SRing -> .0. e. B )