Type | Label | Description |
Statement |
|
Theorem | srglidm 13301 |
The unity element of a semiring is a left multiplicative identity.
(Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux,
1-Apr-2018.)
|
   
          SRing 

  |
|
Theorem | srgridm 13302 |
The unity element of a semiring is a right multiplicative identity.
(Contributed by NM, 15-Sep-2011.) (Revised by Thierry Arnoux,
1-Apr-2018.)
|
   
          SRing  
  |
|
Theorem | issrgid 13303* |
Properties showing that an element is the unity element of a
semiring. (Contributed by NM, 7-Aug-2013.) (Revised by Thierry Arnoux,
1-Apr-2018.)
|
   
         SRing      
       |
|
Theorem | srgacl 13304 |
Closure of the addition operation of a semiring. (Contributed by Mario
Carneiro, 14-Jan-2014.) (Revised by Thierry Arnoux, 1-Apr-2018.)
|
   
     SRing   
  |
|
Theorem | srgcom 13305 |
Commutativity of the additive group of a semiring. (Contributed by
Thierry Arnoux, 1-Apr-2018.)
|
   
     SRing   
    |
|
Theorem | srgrz 13306 |
The zero of a semiring is a right-absorbing element. (Contributed by
Thierry Arnoux, 1-Apr-2018.)
|
   
          SRing  
 |
|
Theorem | srglz 13307 |
The zero of a semiring is a left-absorbing element. (Contributed by AV,
23-Aug-2019.)
|
   
          SRing 

 |
|
Theorem | srgisid 13308* |
In a semiring, the only left-absorbing element is the additive identity.
Remark in [Golan] p. 1. (Contributed by
Thierry Arnoux, 1-May-2018.)
|
   
         SRing    
      |
|
Theorem | srg1zr 13309 |
The only semiring with a base set consisting of one element is the zero
ring (at least if its operations are internal binary operations).
(Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|
   
          SRing
    
   
                    |
|
Theorem | srgen1zr 13310 |
The only semiring with one element is the zero ring (at least if its
operations are internal binary operations). (Contributed by FL,
14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|
   
             SRing
     
                    |
|
Theorem | srgmulgass 13311 |
An associative property between group multiple and ring multiplication
for semirings. (Contributed by AV, 23-Aug-2019.)
|
   
.g 
      SRing 
 
          |
|
Theorem | srgpcomp 13312 |
If two elements of a semiring commute, they also commute if one of the
elements is raised to a higher power. (Contributed by AV,
23-Aug-2019.)
|
   
    mulGrp  .g   SRing        
               |
|
Theorem | srgpcompp 13313 |
If two elements of a semiring commute, they also commute if the elements
are raised to a higher power. (Contributed by AV, 23-Aug-2019.)
|
   
    mulGrp  .g   SRing        
          
       
      |
|
Theorem | srgpcomppsc 13314 |
If two elements of a semiring commute, they also commute if the elements
are raised to a higher power and a scalar multiplication is involved.
(Contributed by AV, 23-Aug-2019.)
|
   
    mulGrp  .g   SRing        
     
.g               
   
       |
|
Theorem | srglmhm 13315* |
Left-multiplication in a semiring by a fixed element of the ring is a
monoid homomorphism. (Contributed by AV, 23-Aug-2019.)
|
   
      SRing       MndHom
   |
|
Theorem | srgrmhm 13316* |
Right-multiplication in a semiring by a fixed element of the ring is a
monoid homomorphism. (Contributed by AV, 23-Aug-2019.)
|
   
      SRing       MndHom    |
|
Theorem | srg1expzeq1 13317 |
The exponentiation (by a nonnegative integer) of the multiplicative
identity of a semiring, analogous to mulgnn0z 13062. (Contributed by AV,
25-Nov-2019.)
|
mulGrp 
.g 
      SRing  
 |
|
7.3.5 Definition and basic properties of unital
rings
|
|
Syntax | crg 13318 |
Extend class notation with class of all (unital) rings.
|
 |
|
Syntax | ccrg 13319 |
Extend class notation with class of all (unital) commutative rings.
|
 |
|
Definition | df-ring 13320* |
Define class of all (unital) rings. A unital ring is a set equipped
with two everywhere-defined internal operations, whose first one is an
additive group structure and the second one is a multiplicative monoid
structure, and where the addition is left- and right-distributive for
the multiplication. Definition 1 in [BourbakiAlg1] p. 92 or definition
of a ring with identity in part Preliminaries of [Roman] p. 19. So that
the additive structure must be abelian (see ringcom 13353), care must be
taken that in the case of a non-unital ring, the commutativity of
addition must be postulated and cannot be proved from the other
conditions. (Contributed by NM, 18-Oct-2012.) (Revised by Mario
Carneiro, 27-Dec-2014.)
|
  mulGrp        ![]. ].](_drbrack.gif)      ![]. ].](_drbrack.gif)       ![]. ].](_drbrack.gif)                                                 |
|
Definition | df-cring 13321 |
Define class of all commutative rings. (Contributed by Mario Carneiro,
7-Jan-2015.)
|
 mulGrp 
CMnd |
|
Theorem | isring 13322* |
The predicate "is a (unital) ring". Definition of "ring with
unit" in
[Schechter] p. 187. (Contributed by
NM, 18-Oct-2012.) (Revised by
Mario Carneiro, 6-Jan-2015.)
|
    mulGrp 
       
  
        
      
  
       |
|
Theorem | ringgrp 13323 |
A ring is a group. (Contributed by NM, 15-Sep-2011.)
|

  |
|
Theorem | ringmgp 13324 |
A ring is a monoid under multiplication. (Contributed by Mario
Carneiro, 6-Jan-2015.)
|
mulGrp  
  |
|
Theorem | iscrng 13325 |
A commutative ring is a ring whose multiplication is a commutative
monoid. (Contributed by Mario Carneiro, 7-Jan-2015.)
|
mulGrp   
CMnd  |
|
Theorem | crngmgp 13326 |
A commutative ring's multiplication operation is commutative.
(Contributed by Mario Carneiro, 7-Jan-2015.)
|
mulGrp  
CMnd |
|
Theorem | ringgrpd 13327 |
A ring is a group. (Contributed by SN, 16-May-2024.)
|
     |
|
Theorem | ringmnd 13328 |
A ring is a monoid under addition. (Contributed by Mario Carneiro,
7-Jan-2015.)
|

  |
|
Theorem | ringmgm 13329 |
A ring is a magma. (Contributed by AV, 31-Jan-2020.)
|

Mgm |
|
Theorem | crngring 13330 |
A commutative ring is a ring. (Contributed by Mario Carneiro,
7-Jan-2015.)
|

  |
|
Theorem | crngringd 13331 |
A commutative ring is a ring. (Contributed by SN, 16-May-2024.)
|
     |
|
Theorem | crnggrpd 13332 |
A commutative ring is a group. (Contributed by SN, 16-May-2024.)
|
     |
|
Theorem | mgpf 13333 |
Restricted functionality of the multiplicative group on rings.
(Contributed by Mario Carneiro, 11-Mar-2015.)
|
mulGrp       |
|
Theorem | ringdilem 13334 |
Properties of a unital ring. (Contributed by NM, 26-Aug-2011.)
(Revised by Mario Carneiro, 6-Jan-2015.)
|
   
         
 
             
          |
|
Theorem | ringcl 13335 |
Closure of the multiplication operation of a ring. (Contributed by NM,
26-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
   
     
     |
|
Theorem | crngcom 13336 |
A commutative ring's multiplication operation is commutative.
(Contributed by Mario Carneiro, 7-Jan-2015.)
|
   
     
       |
|
Theorem | iscrng2 13337* |
A commutative ring is a ring whose multiplication is a commutative
monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|
   
      
  

    |
|
Theorem | ringass 13338 |
Associative law for multiplication in a ring. (Contributed by NM,
27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
   
     
     
       |
|
Theorem | ringideu 13339* |
The unity element of a ring is unique. (Contributed by NM,
27-Aug-2011.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
   
         

    |
|
Theorem | ringdi 13340 |
Distributive law for the multiplication operation of a ring
(left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
|
   
         
 
   
        |
|
Theorem | ringdir 13341 |
Distributive law for the multiplication operation of a ring
(right-distributivity). (Contributed by Steve Rodriguez,
9-Sep-2007.)
|
   
         
 
     
      |
|
Theorem | ringidcl 13342 |
The unity element of a ring belongs to the base set of the ring.
(Contributed by NM, 27-Aug-2011.) (Revised by Mario Carneiro,
27-Dec-2014.)
|
        
  |
|
Theorem | ring0cl 13343 |
The zero element of a ring belongs to its base set. (Contributed by
Mario Carneiro, 12-Jan-2014.)
|
        
  |
|
Theorem | ringidmlem 13344 |
Lemma for ringlidm 13345 and ringridm 13346. (Contributed by NM, 15-Sep-2011.)
(Revised by Mario Carneiro, 27-Dec-2014.)
|
   
             
   |
|
Theorem | ringlidm 13345 |
The unity element of a ring is a left multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
   
          

  |
|
Theorem | ringridm 13346 |
The unity element of a ring is a right multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
   
           
  |
|
Theorem | isringid 13347* |
Properties showing that an element is the unity element of a ring.
(Contributed by NM, 7-Aug-2013.)
|
   
                      |
|
Theorem | ringid 13348* |
The multiplication operation of a unital ring has (one or more) identity
elements. (Contributed by Steve Rodriguez, 9-Sep-2007.) (Revised by
Mario Carneiro, 22-Dec-2013.) (Revised by AV, 24-Aug-2021.)
|
   
     

     
   |
|
Theorem | ringadd2 13349* |
A ring element plus itself is two times the element. (Contributed by
Steve Rodriguez, 9-Sep-2007.) (Revised by Mario Carneiro, 22-Dec-2013.)
(Revised by AV, 24-Aug-2021.)
|
   
           
       |
|
Theorem | ringo2times 13350 |
A ring element plus itself is two times the element. "Two" in an
arbitrary unital ring is the sum of the unity element with itself.
(Contributed by AV, 24-Aug-2021.)
|
   
               
    |
|
Theorem | ringidss 13351 |
A subset of the multiplicative group has the multiplicative identity as
its identity if the identity is in the subset. (Contributed by Mario
Carneiro, 27-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
 mulGrp 
↾s           
       |
|
Theorem | ringacl 13352 |
Closure of the addition operation of a ring. (Contributed by Mario
Carneiro, 14-Jan-2014.)
|
   
    
  
  |
|
Theorem | ringcom 13353 |
Commutativity of the additive group of a ring. (Contributed by
Gérard Lang, 4-Dec-2014.)
|
   
    
  
    |
|
Theorem | ringabl 13354 |
A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|

  |
|
Theorem | ringcmn 13355 |
A ring is a commutative monoid. (Contributed by Mario Carneiro,
7-Jan-2015.)
|

CMnd |
|
Theorem | ringabld 13356 |
A ring is an Abelian group. (Contributed by SN, 1-Jun-2024.)
|
     |
|
Theorem | ringcmnd 13357 |
A ring is a commutative monoid. (Contributed by SN, 1-Jun-2024.)
|
   CMnd |
|
Theorem | ringrng 13358 |
A unital ring is a non-unital ring. (Contributed by AV, 6-Jan-2020.)
|

Rng |
|
Theorem | ringssrng 13359 |
The unital rings are non-unital rings. (Contributed by AV,
20-Mar-2020.)
|
Rng |
|
Theorem | ringpropd 13360* |
If two structures have the same group components (properties), one is a
ring iff the other one is. (Contributed by Mario Carneiro, 6-Dec-2014.)
(Revised by Mario Carneiro, 6-Jan-2015.)
|
              
 
                 
 
                  
   |
|
Theorem | crngpropd 13361* |
If two structures have the same group components (properties), one is a
commutative ring iff the other one is. (Contributed by Mario Carneiro,
8-Feb-2015.)
|
              
 
                 
 
                  
   |
|
Theorem | ringprop 13362 |
If two structures have the same ring components (properties), one is a
ring iff the other one is. (Contributed by Mario Carneiro,
11-Oct-2013.)
|
                 
       |
|
Theorem | isringd 13363* |
Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
|
                    
      
 
 
  
      
 
      
      
 
   
  
    
   

  
      |
|
Theorem | iscrngd 13364* |
Properties that determine a commutative ring. (Contributed by Mario
Carneiro, 7-Jan-2015.)
|
                    
      
 
 
  
      
 
      
      
 
   
  
    
   

  
    
      
  |
|
Theorem | ringlz 13365 |
The zero of a unital ring is a left-absorbing element. (Contributed by
FL, 31-Aug-2009.)
|
   
          

 |
|
Theorem | ringrz 13366 |
The zero of a unital ring is a right-absorbing element. (Contributed by
FL, 31-Aug-2009.)
|
   
           
 |
|
Theorem | ringsrg 13367 |
Any ring is also a semiring. (Contributed by Thierry Arnoux,
1-Apr-2018.)
|

SRing |
|
Theorem | ring1eq0 13368 |
If one and zero are equal, then any two elements of a ring are equal.
Alternately, every ring has one distinct from zero except the zero ring
containing the single element   . (Contributed by Mario
Carneiro, 10-Sep-2014.)
|
             
    |
|
Theorem | ringinvnz1ne0 13369* |
In a unital ring, a left invertible element is different from zero iff
. (Contributed by FL, 18-Apr-2010.)
(Revised by AV,
24-Aug-2021.)
|
   
       
          
     |
|
Theorem | ringinvnzdiv 13370* |
In a unital ring, a left invertible element is not a zero divisor.
(Contributed by FL, 18-Apr-2010.) (Revised by Jeff Madsen,
18-Apr-2010.) (Revised by AV, 24-Aug-2021.)
|
   
       
          
      
  |
|
Theorem | ringnegl 13371 |
Negation in a ring is the same as left multiplication by -1.
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
             
              |
|
Theorem | ringnegr 13372 |
Negation in a ring is the same as right multiplication by -1.
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
             
              |
|
Theorem | ringmneg1 13373 |
Negation of a product in a ring. (mulneg1 8372 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
   
                              |
|
Theorem | ringmneg2 13374 |
Negation of a product in a ring. (mulneg2 8373 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
   
                              |
|
Theorem | ringm2neg 13375 |
Double negation of a product in a ring. (mul2neg 8375 analog.)
(Contributed by Mario Carneiro, 4-Dec-2014.)
|
   
                              |
|
Theorem | ringsubdi 13376 |
Ring multiplication distributes over subtraction. (subdi 8362 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | ringsubdir 13377 |
Ring multiplication distributes over subtraction. (subdir 8363 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | mulgass2 13378 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
.g 
     
     
       |
|
Theorem | ring1 13379 |
The (smallest) structure representing a zero ring. (Contributed by
AV, 28-Apr-2019.)
|
               
                   
         |
|
Theorem | ringn0 13380 |
The class of rings is not empty (it is also inhabited, as shown at
ring1 13379). (Contributed by AV, 29-Apr-2019.)
|
 |
|
Theorem | ringressid 13381 |
A ring restricted to its base set is a ring. It will usually be the
original ring exactly, of course, but to show that needs additional
conditions such as those in strressid 12556. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
     
↾s    |
|
Theorem | imasring 13382* |
The image structure of a ring is a ring. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
  s
          
                
                 
        
            
                 
        
             
         |
|
Theorem | imasringf1 13383 |
The image of a ring under an injection is a ring. (Contributed by AV,
27-Feb-2025.)
|
 s           

  |
|
Theorem | qusring2 13384* |
The quotient structure of a ring is a ring. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
  s
 
       
            
  
    
 
 
     
  
       |
|
7.3.6 Opposite ring
|
|
Syntax | coppr 13385 |
The opposite ring operation.
|
oppr |
|
Definition | df-oppr 13386 |
Define an opposite ring, which is the same as the original ring but with
multiplication written the other way around. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 

sSet       tpos         |
|
Theorem | opprvalg 13387 |
Value of the opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
   
    oppr    sSet      
tpos    |
|
Theorem | opprmulfvalg 13388 |
Value of the multiplication operation of an opposite ring. (Contributed
by Mario Carneiro, 1-Dec-2014.)
|
   
    oppr 
     tpos
 |
|
Theorem | opprmulg 13389 |
Value of the multiplication operation of an opposite ring. Hypotheses
eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed
by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro,
30-Aug-2015.)
|
   
    oppr 
      
  
   |
|
Theorem | crngoppr 13390 |
In a commutative ring, the opposite ring is equivalent to the original
ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
    oppr 
     
       |
|
Theorem | opprex 13391 |
Existence of the opposite ring. If you know that is a ring, see
opprring 13397. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
oppr     |
|
Theorem | opprsllem 13392 |
Lemma for opprbasg 13393 and oppraddg 13394. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
oppr   Slot             
        
      |
|
Theorem | opprbasg 13393 |
Base set of an opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr             |
|
Theorem | oppraddg 13394 |
Addition operation of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr           |
|
Theorem | opprrng 13395 |
An opposite non-unital ring is a non-unital ring. (Contributed by AV,
15-Feb-2025.)
|
oppr   Rng Rng |
|
Theorem | opprrngbg 13396 |
A set is a non-unital ring if and only if its opposite is a non-unital
ring. Bidirectional form of opprrng 13395. (Contributed by AV,
15-Feb-2025.)
|
oppr    Rng
Rng  |
|
Theorem | opprring 13397 |
An opposite ring is a ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
oppr  
  |
|
Theorem | opprringbg 13398 |
Bidirectional form of opprring 13397. (Contributed by Mario Carneiro,
6-Dec-2014.)
|
oppr       |
|
Theorem | oppr0g 13399 |
Additive identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |
|
Theorem | oppr1g 13400 |
Multiplicative identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |