Metamath Proof Explorer


Theorem srglz

Description: The zero of a semiring is a left-absorbing element. (Contributed by AV, 23-Aug-2019)

Ref Expression
Hypotheses srgz.b
|- B = ( Base ` R )
srgz.t
|- .x. = ( .r ` R )
srgz.z
|- .0. = ( 0g ` R )
Assertion srglz
|- ( ( R e. SRing /\ X e. B ) -> ( .0. .x. X ) = .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 eqid
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 eqid
 |-  ( +g ` R ) = ( +g ` R )
6 1 4 5 2 3 issrg
 |-  ( R e. SRing <-> ( R e. CMnd /\ ( mulGrp ` R ) e. Mnd /\ A. x e. B ( A. y e. B A. z e. B ( ( x .x. ( y ( +g ` R ) z ) ) = ( ( x .x. y ) ( +g ` R ) ( x .x. z ) ) /\ ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` R ) ( y .x. z ) ) ) /\ ( ( .0. .x. x ) = .0. /\ ( x .x. .0. ) = .0. ) ) ) )
7 6 simp3bi
 |-  ( R e. SRing -> A. x e. B ( A. y e. B A. z e. B ( ( x .x. ( y ( +g ` R ) z ) ) = ( ( x .x. y ) ( +g ` R ) ( x .x. z ) ) /\ ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` R ) ( y .x. z ) ) ) /\ ( ( .0. .x. x ) = .0. /\ ( x .x. .0. ) = .0. ) ) )
8 7 r19.21bi
 |-  ( ( R e. SRing /\ x e. B ) -> ( A. y e. B A. z e. B ( ( x .x. ( y ( +g ` R ) z ) ) = ( ( x .x. y ) ( +g ` R ) ( x .x. z ) ) /\ ( ( x ( +g ` R ) y ) .x. z ) = ( ( x .x. z ) ( +g ` R ) ( y .x. z ) ) ) /\ ( ( .0. .x. x ) = .0. /\ ( x .x. .0. ) = .0. ) ) )
9 8 simprld
 |-  ( ( R e. SRing /\ x e. B ) -> ( .0. .x. x ) = .0. )
10 9 ralrimiva
 |-  ( R e. SRing -> A. x e. B ( .0. .x. x ) = .0. )
11 oveq2
 |-  ( x = X -> ( .0. .x. x ) = ( .0. .x. X ) )
12 11 eqeq1d
 |-  ( x = X -> ( ( .0. .x. x ) = .0. <-> ( .0. .x. X ) = .0. ) )
13 12 rspcv
 |-  ( X e. B -> ( A. x e. B ( .0. .x. x ) = .0. -> ( .0. .x. X ) = .0. ) )
14 10 13 mpan9
 |-  ( ( R e. SRing /\ X e. B ) -> ( .0. .x. X ) = .0. )