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

Metamath Proof Explorer

Theorem ringsrg

Description: Any ring is also a semiring. (Contributed by Thierry Arnoux, 1-Apr-2018)

Ref Expression
Assertion ringsrg 
|- ( R e. Ring -> R e. SRing )

Proof

Step Hyp Ref Expression
1 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
2 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
3 2 ringmgp 
 |-  ( R e. Ring -> ( mulGrp ` R ) e. Mnd )
4 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 eqid 
 |-  ( .r ` R ) = ( .r ` R )
7 4 2 5 6 isring 
 |-  ( R e. Ring <-> ( R e. Grp /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) )
8 7 simp3bi 
 |-  ( R e. Ring -> A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) )
9 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
10 4 6 9 ringlz 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) )
11 4 6 9 ringrz 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
12 10 11 jca 
 |-  ( ( R e. Ring /\ x e. ( Base ` R ) ) -> ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
13 12 ralrimiva 
 |-  ( R e. Ring -> A. x e. ( Base ` R ) ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) )
14 r19.26 
 |-  ( A. x e. ( Base ` R ) ( A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) /\ ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) ) <-> ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) /\ A. x e. ( Base ` R ) ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) ) )
15 8 13 14 sylanbrc 
 |-  ( R e. Ring -> A. x e. ( Base ` R ) ( A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) /\ ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) ) )
16 4 2 5 6 9 issrg 
 |-  ( R e. SRing <-> ( R e. CMnd /\ ( mulGrp ` R ) e. Mnd /\ A. x e. ( Base ` R ) ( A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) /\ ( ( ( 0g ` R ) ( .r ` R ) x ) = ( 0g ` R ) /\ ( x ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) ) ) ) )
17 1 3 15 16 syl3anbrc 
 |-  ( R e. Ring -> R e. SRing )