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