This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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. )