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 )