Theorem srgisid

Description: In a semiring, the only left-absorbing element is the additive identity. Remark in Golan p. 1. (Contributed by Thierry Arnoux, 1-May-2018)

	Ref	Expression
Hypotheses	srgz.b	|- B = ( Base ` R )
	srgz.t	|- .x. = ( .r ` R )
	srgz.z	|- .0. = ( 0g ` R )
	srgisid.1	|- ( ph -> R e. SRing )
	srgisid.2	|- ( ph -> Z e. B )
	srgisid.3	|- ( ( ph /\ x e. B ) -> ( Z .x. x ) = Z )
Assertion	srgisid	|- ( ph -> Z = .0. )

Proof

Step	Hyp	Ref	Expression
1		srgz.b	|- B = ( Base ` R )
2		srgz.t	|- .x. = ( .r ` R )
3		srgz.z	|- .0. = ( 0g ` R )
4		srgisid.1	|- ( ph -> R e. SRing )
5		srgisid.2	|- ( ph -> Z e. B )
6		srgisid.3	|- ( ( ph /\ x e. B ) -> ( Z .x. x ) = Z )
7	6	ralrimiva	|- ( ph -> A. x e. B ( Z .x. x ) = Z )
8	1 3	srg0cl	|- ( R e. SRing -> .0. e. B )
9		oveq2	|- ( x = .0. -> ( Z .x. x ) = ( Z .x. .0. ) )
10	9	eqeq1d	|- ( x = .0. -> ( ( Z .x. x ) = Z <-> ( Z .x. .0. ) = Z ) )
11	10	rspcv	|- ( .0. e. B -> ( A. x e. B ( Z .x. x ) = Z -> ( Z .x. .0. ) = Z ) )
12	4 8 11	3syl	|- ( ph -> ( A. x e. B ( Z .x. x ) = Z -> ( Z .x. .0. ) = Z ) )
13	7 12	mpd	|- ( ph -> ( Z .x. .0. ) = Z )
14	1 2 3	srgrz	|- ( ( R e. SRing /\ Z e. B ) -> ( Z .x. .0. ) = .0. )
15	4 5 14	syl2anc	|- ( ph -> ( Z .x. .0. ) = .0. )
16	13 15	eqtr3d	|- ( ph -> Z = .0. )