Type | Label | Description |
Statement |
|
Theorem | ringsubdi 13301 |
Ring multiplication distributes over subtraction. (subdi 8355 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | ringsubdir 13302 |
Ring multiplication distributes over subtraction. (subdir 8356 analog.)
(Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro,
2-Jul-2014.)
|
   
        
              
     |
|
Theorem | mulgass2 13303 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
.g 
     
     
       |
|
Theorem | ring1 13304 |
The (smallest) structure representing a zero ring. (Contributed by
AV, 28-Apr-2019.)
|
               
                   
         |
|
Theorem | ringn0 13305 |
The class of rings is not empty (it is also inhabited, as shown at
ring1 13304). (Contributed by AV, 29-Apr-2019.)
|
 |
|
Theorem | ringressid 13306 |
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 12544. (Contributed by Jim Kingdon,
28-Feb-2025.)
|
     
↾s    |
|
Theorem | imasring 13307* |
The image structure of a ring is a ring. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
  s
          
                
                 
        
            
                 
        
             
         |
|
Theorem | imasringf1 13308 |
The image of a ring under an injection is a ring. (Contributed by AV,
27-Feb-2025.)
|
 s           

  |
|
Theorem | qusring2 13309* |
The quotient structure of a ring is a ring. (Contributed by Mario
Carneiro, 14-Jun-2015.)
|
  s
 
       
            
  
    
 
 
     
  
       |
|
7.3.6 Opposite ring
|
|
Syntax | coppr 13310 |
The opposite ring operation.
|
oppr |
|
Definition | df-oppr 13311 |
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 13312 |
Value of the opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
   
    oppr    sSet      
tpos    |
|
Theorem | opprmulfvalg 13313 |
Value of the multiplication operation of an opposite ring. (Contributed
by Mario Carneiro, 1-Dec-2014.)
|
   
    oppr 
     tpos
 |
|
Theorem | opprmulg 13314 |
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 13315 |
In a commutative ring, the opposite ring is equivalent to the original
ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
    oppr 
     
       |
|
Theorem | opprex 13316 |
Existence of the opposite ring. If you know that is a ring, see
opprring 13322. (Contributed by Jim Kingdon, 10-Jan-2025.)
|
oppr     |
|
Theorem | opprsllem 13317 |
Lemma for opprbasg 13318 and oppraddg 13319. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|
oppr   Slot             
        
      |
|
Theorem | opprbasg 13318 |
Base set of an opposite ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr             |
|
Theorem | oppraddg 13319 |
Addition operation of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|
oppr           |
|
Theorem | opprrng 13320 |
An opposite non-unital ring is a non-unital ring. (Contributed by AV,
15-Feb-2025.)
|
oppr   Rng Rng |
|
Theorem | opprrngbg 13321 |
A set is a non-unital ring if and only if its opposite is a non-unital
ring. Bidirectional form of opprrng 13320. (Contributed by AV,
15-Feb-2025.)
|
oppr    Rng
Rng  |
|
Theorem | opprring 13322 |
An opposite ring is a ring. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|
oppr  
  |
|
Theorem | opprringbg 13323 |
Bidirectional form of opprring 13322. (Contributed by Mario Carneiro,
6-Dec-2014.)
|
oppr       |
|
Theorem | oppr0g 13324 |
Additive identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |
|
Theorem | oppr1g 13325 |
Multiplicative identity of an opposite ring. (Contributed by Mario
Carneiro, 1-Dec-2014.)
|
oppr 
           |
|
Theorem | opprnegg 13326 |
The negative function in an opposite ring. (Contributed by Mario
Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|
oppr       
       |
|
Theorem | opprsubgg 13327 |
Being a subgroup is a symmetric property. (Contributed by Mario
Carneiro, 6-Dec-2014.)
|
oppr   SubGrp  SubGrp    |
|
Theorem | mulgass3 13328 |
An associative property between group multiple and ring multiplication.
(Contributed by Mario Carneiro, 14-Jun-2015.)
|
   
.g 
     
   
         |
|
7.3.7 Divisibility
|
|
Syntax | cdsr 13329 |
Ring divisibility relation.
|
r |
|
Syntax | cui 13330 |
Units in a ring.
|
Unit |
|
Syntax | cir 13331 |
Ring irreducibles.
|
Irred |
|
Definition | df-dvdsr 13332* |
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 13333 |
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 13334* |
Define the set of irreducible elements in a ring. (Contributed by Mario
Carneiro, 4-Dec-2014.)
|
Irred        Unit  
 ![]_ ]_](_urbrack.gif)   
           |
|
Theorem | reldvdsrsrg 13335 |
The divides relation is a relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|
 SRing  r    |
|
Theorem | dvdsrvald 13336* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|
        r    SRing 
     
      
     |
|
Theorem | dvdsrd 13337* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
        r    SRing 
     
   
     |
|
Theorem | dvdsr2d 13338* |
Value of the divides relation. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
        r    SRing 
     
    
    |
|
Theorem | dvdsrmuld 13339 |
A left-multiple of is
divisible by .
(Contributed by
Mario Carneiro, 1-Dec-2014.)
|
        r    SRing 
     
        |
|
Theorem | dvdsrcld 13340 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
        r    SRing   
  |
|
Theorem | dvdsrex 13341 |
Existence of the divisibility relation. (Contributed by Jim Kingdon,
28-Jan-2025.)
|
 SRing  r    |
|
Theorem | dvdsrcl2 13342 |
Closure of a dividing element. (Contributed by Mario Carneiro,
5-Dec-2014.)
|
     r   
   |
|
Theorem | dvdsrid 13343 |
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 13344 |
Divisibility is transitive. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
     r   
   |
|
Theorem | dvdsrmul1 13345 |
The divisibility relation is preserved under right-multiplication.
(Contributed by Mario Carneiro, 1-Dec-2014.)
|
     r 
       
     |
|
Theorem | dvdsrneg 13346 |
An element divides its negative. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
     r         
      |
|
Theorem | dvdsr01 13347 |
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 13348 |
Only zero is divisible by zero. (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
     r 
      
  |
|
Theorem | isunitd 13349 |
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 13350 |
The multiplicative identity is a unit. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
Unit      
  |
|
Theorem | unitcld 13351 |
A unit is an element of the base set. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
       Unit    SRing      |
|
Theorem | unitssd 13352 |
The set of units is contained in the base set. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
       Unit    SRing    |
|
Theorem | opprunitd 13353 |
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 13354 |
Property of being a unit in a commutative ring. (Contributed by Mario
Carneiro, 18-Apr-2016.)
|
Unit       r      |
|
Theorem | dvdsunit 13355 |
A divisor of a unit is a unit. (Contributed by Mario Carneiro,
18-Apr-2016.)
|
Unit   r   
   |
|
Theorem | unitmulcl 13356 |
The product of units is a unit. (Contributed by Mario Carneiro,
2-Dec-2014.)
|
Unit 
     
     |
|
Theorem | unitmulclb 13357 |
Reversal of unitmulcl 13356 in a commutative ring. (Contributed by
Mario
Carneiro, 18-Apr-2016.)
|
Unit 
         
         |
|
Theorem | unitgrpbasd 13358 |
The base set of the group of units. (Contributed by Mario Carneiro,
25-Dec-2014.)
|
 Unit     mulGrp  ↾s    SRing        |
|
Theorem | unitgrp 13359 |
The group of units is a group under multiplication. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitabl 13360 |
The group of units of a commutative ring is abelian. (Contributed by
Mario Carneiro, 19-Apr-2016.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitgrpid 13361 |
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 13362 |
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 13363 |
Extend class notation with multiplicative inverse.
|
 |
|
Definition | df-invr 13364 |
Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|
      mulGrp  ↾s Unit      |
|
Theorem | invrfvald 13365 |
Multiplicative inverse function for a ring. (Contributed by NM,
21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|
 Unit     mulGrp  ↾s         
         |
|
Theorem | unitinvcl 13366 |
The inverse of a unit exists and is a unit. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit       

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

          |
|
Theorem | ringinvcl 13368 |
The inverse of a unit is an element of the ring. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit                
  |
|
Theorem | unitlinv 13369 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                     
  |
|
Theorem | unitrinv 13370 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                        |
|
Theorem | 1rinv 13371 |
The inverse of the ring unity is the ring unity. (Contributed by Mario
Carneiro, 18-Jun-2015.)
|
        
   |
|
Theorem | 0unit 13372 |
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 13373 |
The negative of a unit is a unit. (Contributed by Mario Carneiro,
4-Dec-2014.)
|
Unit             
  |
|
Syntax | cdvr 13374 |
Extend class notation with ring division.
|
/r |
|
Definition | df-dvr 13375* |
Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|
/r  
     Unit 
                   |
|
Theorem | dvrfvald 13376* |
Division operation in a ring. (Contributed by Mario Carneiro,
2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.) (Proof shortened
by AV, 2-Mar-2024.)
|
             Unit          /r   
SRing 
 
         |
|
Theorem | dvrvald 13377 |
Division operation in a ring. (Contributed by Mario Carneiro,
2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|
             Unit          /r   
      
         |
|
Theorem | dvrcl 13378 |
Closure of division operation. (Contributed by Mario Carneiro,
2-Jul-2014.)
|
    Unit 
/r   
  
  |
|
Theorem | unitdvcl 13379 |
The units are closed under division. (Contributed by Mario Carneiro,
2-Jul-2014.)
|
Unit 
/r   
  
  |
|
Theorem | dvrid 13380 |
A ring element divided by itself is the ring unity. (dividap 8671
analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|
Unit 
/r          
 |
|
Theorem | dvr1 13381 |
A ring element divided by the ring unity is itself. (div1 8673
analog.)
(Contributed by Mario Carneiro, 18-Jun-2015.)
|
   
/r         
  |
|
Theorem | dvrass 13382 |
An associative law for division. (divassap 8660 analog.) (Contributed by
Mario Carneiro, 4-Dec-2014.)
|
    Unit 
/r 
     
     
       |
|
Theorem | dvrcan1 13383 |
A cancellation law for division. (divcanap1 8651 analog.) (Contributed
by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro,
2-Dec-2014.)
|
    Unit 
/r 
     
       |
|
Theorem | dvrcan3 13384 |
A cancellation law for division. (divcanap3 8668 analog.) (Contributed
by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro,
18-Jun-2015.)
|
    Unit 
/r 
     
    
  |
|
Theorem | dvreq1 13385 |
Equality in terms of ratio equal to ring unity. (diveqap1 8675 analog.)
(Contributed by Mario Carneiro, 28-Apr-2016.)
|
    Unit 
/r       
   
   |
|
Theorem | dvrdir 13386 |
Distributive law for the division operation of a ring. (Contributed by
Thierry Arnoux, 30-Oct-2017.)
|
    Unit 
   /r    
 
   
        |
|
Theorem | rdivmuldivd 13387 |
Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
(Contributed by Thierry Arnoux, 30-Oct-2017.)
|
    Unit 
   /r 
      
                
     |
|
Theorem | ringinvdv 13388 |
Write the inverse function in terms of division. (Contributed by Mario
Carneiro, 2-Jul-2014.)
|
    Unit 
/r     
          
   |
|
Theorem | rngidpropdg 13389* |
The ring unity depends only on the ring's base set and multiplication
operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|
              
 
                                |
|
Theorem | dvdsrpropdg 13390* |
The divisibility relation depends only on the ring's base set and
multiplication operation. (Contributed by Mario Carneiro,
26-Dec-2014.)
|
              
 
                  SRing  SRing   r   r    |
|
Theorem | unitpropdg 13391* |
The set of units depends only on the ring's base set and multiplication
operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|
              
 
                      Unit  Unit    |
|
Theorem | invrpropdg 13392* |
The ring inverse function depends only on the ring's base set and
multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
(Revised by Mario Carneiro, 5-Oct-2015.)
|
              
 
                                |
|
7.3.8 Ring homomorphisms
|
|
Syntax | crh 13393 |
Extend class notation with the ring homomorphisms.
|
RingHom |
|
Syntax | crs 13394 |
Extend class notation with the ring isomorphisms.
|
RingIso |
|
Definition | df-rnghom 13395* |
Define the set of ring homomorphisms from to .
(Contributed
by Stefan O'Rear, 7-Mar-2015.)
|
RingHom         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                  
                                                            |
|
Definition | df-rngiso 13396* |
Define the set of ring isomorphisms from to .
(Contributed
by Stefan O'Rear, 7-Mar-2015.)
|
RingIso  
  RingHom 

 RingHom     |
|
7.3.9 Nonzero rings and zero rings
|
|
Syntax | cnzr 13397 |
The class of nonzero rings.
|
NzRing |
|
Definition | df-nzr 13398 |
A nonzero or nontrivial ring is a ring with at least two values, or
equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear,
24-Feb-2015.)
|
NzRing     
      |
|
Theorem | isnzr 13399 |
Property of a nonzero ring. (Contributed by Stefan O'Rear,
24-Feb-2015.)
|
        
NzRing    |
|
Theorem | nzrnz 13400 |
One and zero are different in a nonzero ring. (Contributed by Stefan
O'Rear, 24-Feb-2015.)
|
        
NzRing  |