Type | Label | Description |
Statement |
|
Theorem | ringdi 13201 |
Distributive law for the multiplication operation of a ring
(left-distributivity). (Contributed by Steve Rodriguez, 9-Sep-2007.)
|
   
         
 
   
        |
|
Theorem | ringdir 13202 |
Distributive law for the multiplication operation of a ring
(right-distributivity). (Contributed by Steve Rodriguez,
9-Sep-2007.)
|
   
         
 
     
      |
|
Theorem | ringidcl 13203 |
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 13204 |
The zero element of a ring belongs to its base set. (Contributed by
Mario Carneiro, 12-Jan-2014.)
|
        
  |
|
Theorem | ringidmlem 13205 |
Lemma for ringlidm 13206 and ringridm 13207. (Contributed by NM, 15-Sep-2011.)
(Revised by Mario Carneiro, 27-Dec-2014.)
|
   
             
   |
|
Theorem | ringlidm 13206 |
The unity element of a ring is a left multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
   
          

  |
|
Theorem | ringridm 13207 |
The unity element of a ring is a right multiplicative identity.
(Contributed by NM, 15-Sep-2011.)
|
   
           
  |
|
Theorem | isringid 13208* |
Properties showing that an element is the unity element of a ring.
(Contributed by NM, 7-Aug-2013.)
|
   
                      |
|
Theorem | ringid 13209* |
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 13210* |
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 13211 |
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 13212 |
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 13213 |
Closure of the addition operation of a ring. (Contributed by Mario
Carneiro, 14-Jan-2014.)
|
   
    
  
  |
|
Theorem | ringcom 13214 |
Commutativity of the additive group of a ring. (Contributed by
Gérard Lang, 4-Dec-2014.)
|
   
    
  
    |
|
Theorem | ringabl 13215 |
A ring is an Abelian group. (Contributed by NM, 26-Aug-2011.)
|

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

CMnd |
|
Theorem | ringpropd 13217* |
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 13218* |
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 13219 |
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 13220* |
Properties that determine a ring. (Contributed by NM, 2-Aug-2013.)
|
                    
      
 
 
  
      
 
      
      
 
   
  
    
   

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

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

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

SRing |
|
Theorem | ring1eq0 13225 |
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 13226* |
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 13227* |
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 13228 |
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 13229 |
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 13230 |
Negation of a product in a ring. (mulneg1 8352 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
   
                              |
|
Theorem | ringmneg2 13231 |
Negation of a product in a ring. (mulneg2 8353 analog.) (Contributed by
Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|
   
                              |
|
Theorem | ringm2neg 13232 |
Double negation of a product in a ring. (mul2neg 8355 analog.)
(Contributed by Mario Carneiro, 4-Dec-2014.)
|
   
                              |
|
Theorem | ringsubdi 13233 |
Ring multiplication distributes over subtraction. (subdi 8342 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | ringsubdir 13234 |
Ring multiplication distributes over subtraction. (subdir 8343 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | mulgass2 13235 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
.g 
     
     
       |
|
Theorem | ring1 13236 |
The (smallest) structure representing a zero ring. (Contributed by
AV, 28-Apr-2019.)
|
               
                   
         |
|
Theorem | ringn0 13237 |
The class of rings is not empty (it is also inhabited, as shown at
ring1 13236). (Contributed by AV, 29-Apr-2019.)
|
 |
|
Theorem | ringressid 13238 |
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 12530. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
     
↾s    |
|
7.3.5 Opposite ring
|
|
Syntax | coppr 13239 |
The opposite ring operation.
|
oppr |
|
Definition | df-oppr 13240 |
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 13241 |
Value of the opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
   
    oppr    sSet      
tpos    |
|
Theorem | opprmulfvalg 13242 |
Value of the multiplication operation of an opposite ring. (Contributed
by Mario Carneiro, 1-Dec-2014.)
|
   
    oppr 
     tpos
 |
|
Theorem | opprmulg 13243 |
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 13244 |
In a commutative ring, the opposite ring is equivalent to the original
ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
    oppr 
     
       |
|
Theorem | opprex 13245 |
Existence of the opposite ring. If you know that is a ring, see
opprring 13249. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
oppr     |
|
Theorem | opprsllem 13246 |
Lemma for opprbasg 13247 and oppraddg 13248. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
oppr   Slot             
        
      |
|
Theorem | opprbasg 13247 |
Base set of an opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr             |
|
Theorem | oppraddg 13248 |
Addition operation of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr           |
|
Theorem | opprring 13249 |
An opposite ring is a ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
oppr  
  |
|
Theorem | opprringbg 13250 |
Bidirectional form of opprring 13249. (Contributed by Mario Carneiro,
6-Dec-2014.)
|
oppr       |
|
Theorem | oppr0g 13251 |
Additive identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |
|
Theorem | oppr1g 13252 |
Multiplicative identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |
|
Theorem | opprnegg 13253 |
The negative function in an opposite ring. (Contributed by Mario
Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|
oppr       
       |
|
Theorem | mulgass3 13254 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
.g 
     
   
         |
|
7.3.6 Divisibility
|
|
Syntax | cdsr 13255 |
Ring divisibility relation.
|
r |
|
Syntax | cui 13256 |
Units in a ring.
|
Unit |
|
Syntax | cir 13257 |
Ring irreducibles.
|
Irred |
|
Definition | df-dvdsr 13258* |
Define the (right) divisibility relation in a ring. Access to the left
divisibility relation is available through
 r oppr   . (Contributed by Mario Carneiro,
1-Dec-2014.)
|
r                             |
|
Definition | df-unit 13259 |
Define the set of units in a ring, that is, all elements with a left and
right multiplicative inverse. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
Unit      r   r oppr               |
|
Definition | df-irred 13260* |
Define the set of irreducible elements in a ring. (Contributed by Mario
Carneiro, 4-Dec-2014.)
|
Irred        Unit  
 ![]_ ]_](_urbrack.gif)   
           |
|
Theorem | reldvdsrsrg 13261 |
The divides relation is a relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|
 SRing  r    |
|
Theorem | dvdsrvald 13262* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
        r    SRing 
     
      
     |
|
Theorem | dvdsrd 13263* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
        r    SRing 
     
   
     |
|
Theorem | dvdsr2d 13264* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
        r    SRing 
     
    
    |
|
Theorem | dvdsrmuld 13265 |
A left-multiple of is
divisible by .
(Contributed by
Mario Carneiro, 1-Dec-2014.)
|
        r    SRing 
     
        |
|
Theorem | dvdsrcld 13266 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
        r    SRing   
  |
|
Theorem | dvdsrex 13267 |
Existence of the divisibility relation. (Contributed by Jim Kingdon,
28-Jan-2025.)
|
 SRing  r    |
|
Theorem | dvdsrcl2 13268 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
     r   
   |
|
Theorem | dvdsrid 13269 |
An element in a (unital) ring divides itself. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|
     r    
  |
|
Theorem | dvdsrtr 13270 |
Divisibility is transitive. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
     r   
   |
|
Theorem | dvdsrmul1 13271 |
The divisibility relation is preserved under right-multiplication.
(Contributed by Mario Carneiro, 1-Dec-2014.)
|
     r 
       
     |
|
Theorem | dvdsrneg 13272 |
An element divides its negative. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
     r         
      |
|
Theorem | dvdsr01 13273 |
In a ring, zero is divisible by all elements. ("Zero divisor" as a
term
has a somewhat different meaning.) (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
     r 
      
 |
|
Theorem | dvdsr02 13274 |
Only zero is divisible by zero. (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
     r 
      
  |
|
Theorem | isunitd 13275 |
Property of being a unit of a ring. A unit is an element that left-
and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.)
(Revised by Mario Carneiro, 8-Dec-2015.)
|
 Unit           r   
oppr     r    SRing    
   |
|
Theorem | 1unit 13276 |
The multiplicative identity is a unit. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
Unit      
  |
|
Theorem | unitcld 13277 |
A unit is an element of the base set. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
       Unit    SRing      |
|
Theorem | unitssd 13278 |
The set of units is contained in the base set. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
       Unit    SRing    |
|
Theorem | opprunitd 13279 |
Being a unit is a symmetric property, so it transfers to the opposite
ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|
 Unit    oppr     
Unit    |
|
Theorem | crngunit 13280 |
Property of being a unit in a commutative ring. (Contributed by Mario
Carneiro, 18-Apr-2016.)
|
Unit       r      |
|
Theorem | dvdsunit 13281 |
A divisor of a unit is a unit. (Contributed by Mario Carneiro,
18-Apr-2016.)
|
Unit   r   
   |
|
Theorem | unitmulcl 13282 |
The product of units is a unit. (Contributed by Mario Carneiro,
2-Dec-2014.)
|
Unit 
     
     |
|
Theorem | unitmulclb 13283 |
Reversal of unitmulcl 13282 in a commutative ring. (Contributed by
Mario
Carneiro, 18-Apr-2016.)
|
Unit 
         
         |
|
Theorem | unitgrpbasd 13284 |
The base set of the group of units. (Contributed by Mario Carneiro,
25-Dec-2014.)
|
 Unit     mulGrp  ↾s    SRing        |
|
Theorem | unitgrp 13285 |
The group of units is a group under multiplication. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitabl 13286 |
The group of units of a commutative ring is abelian. (Contributed by
Mario Carneiro, 19-Apr-2016.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitgrpid 13287 |
The identity of the group of units of a ring is the ring unity.
(Contributed by Mario Carneiro, 2-Dec-2014.)
|
Unit   mulGrp  ↾s 
           |
|
Theorem | unitsubm 13288 |
The group of units is a submonoid of the multiplicative monoid of the
ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
|
Unit  mulGrp  
SubMnd    |
|
Syntax | cinvr 13289 |
Extend class notation with multiplicative inverse.
|
 |
|
Definition | df-invr 13290 |
Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|
      mulGrp  ↾s Unit      |
|
Theorem | invrfvald 13291 |
Multiplicative inverse function for a ring. (Contributed by NM,
21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|
 Unit     mulGrp  ↾s         
         |
|
Theorem | unitinvcl 13292 |
The inverse of a unit exists and is a unit. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit       

      |
|
Theorem | unitinvinv 13293 |
The inverse of the inverse of a unit is the same element. (Contributed
by Mario Carneiro, 4-Dec-2014.)
|
Unit       

          |
|
Theorem | ringinvcl 13294 |
The inverse of a unit is an element of the ring. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit                
  |
|
Theorem | unitlinv 13295 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                     
  |
|
Theorem | unitrinv 13296 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                        |
|
Theorem | 1rinv 13297 |
The inverse of the ring unity is the ring unity. (Contributed by Mario
Carneiro, 18-Jun-2015.)
|
        
   |
|
Theorem | 0unit 13298 |
The additive identity is a unit if and only if , i.e. we are
in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|
Unit             |
|
Theorem | unitnegcl 13299 |
The negative of a unit is a unit. (Contributed by Mario Carneiro,
4-Dec-2014.)
|
Unit             
  |
|
Syntax | cdvr 13300 |
Extend class notation with ring division.
|
/r |