Theorem List for Intuitionistic Logic Explorer - 13601-13700 *Has distinct variable
group(s)
Type | Label | Description |
Statement |
|
Theorem | dvdsr02 13601 |
Only zero is divisible by zero. (Contributed by Stefan O'Rear,
29-Mar-2015.)
|
     r 
      
  |
|
Theorem | isunitd 13602 |
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 13603 |
The multiplicative identity is a unit. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
Unit      
  |
|
Theorem | unitcld 13604 |
A unit is an element of the base set. (Contributed by Mario Carneiro,
1-Dec-2014.)
|
       Unit    SRing      |
|
Theorem | unitssd 13605 |
The set of units is contained in the base set. (Contributed by Mario
Carneiro, 5-Oct-2015.)
|
       Unit    SRing    |
|
Theorem | opprunitd 13606 |
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 13607 |
Property of being a unit in a commutative ring. (Contributed by Mario
Carneiro, 18-Apr-2016.)
|
Unit       r      |
|
Theorem | dvdsunit 13608 |
A divisor of a unit is a unit. (Contributed by Mario Carneiro,
18-Apr-2016.)
|
Unit   r   
   |
|
Theorem | unitmulcl 13609 |
The product of units is a unit. (Contributed by Mario Carneiro,
2-Dec-2014.)
|
Unit 
     
     |
|
Theorem | unitmulclb 13610 |
Reversal of unitmulcl 13609 in a commutative ring. (Contributed by
Mario
Carneiro, 18-Apr-2016.)
|
Unit 
         
         |
|
Theorem | unitgrpbasd 13611 |
The base set of the group of units. (Contributed by Mario Carneiro,
25-Dec-2014.)
|
 Unit     mulGrp  ↾s    SRing        |
|
Theorem | unitgrp 13612 |
The group of units is a group under multiplication. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitabl 13613 |
The group of units of a commutative ring is abelian. (Contributed by
Mario Carneiro, 19-Apr-2016.)
|
Unit   mulGrp  ↾s  
  |
|
Theorem | unitgrpid 13614 |
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 13615 |
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 13616 |
Extend class notation with multiplicative inverse.
|
 |
|
Definition | df-invr 13617 |
Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|
      mulGrp  ↾s Unit      |
|
Theorem | invrfvald 13618 |
Multiplicative inverse function for a ring. (Contributed by NM,
21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|
 Unit     mulGrp  ↾s         
         |
|
Theorem | unitinvcl 13619 |
The inverse of a unit exists and is a unit. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit       

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

          |
|
Theorem | ringinvcl 13621 |
The inverse of a unit is an element of the ring. (Contributed by
Mario Carneiro, 2-Dec-2014.)
|
Unit                
  |
|
Theorem | unitlinv 13622 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                     
  |
|
Theorem | unitrinv 13623 |
A unit times its inverse is the ring unity. (Contributed by Mario
Carneiro, 2-Dec-2014.)
|
Unit                        |
|
Theorem | 1rinv 13624 |
The inverse of the ring unity is the ring unity. (Contributed by Mario
Carneiro, 18-Jun-2015.)
|
        
   |
|
Theorem | 0unit 13625 |
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 13626 |
The negative of a unit is a unit. (Contributed by Mario Carneiro,
4-Dec-2014.)
|
Unit             
  |
|
Syntax | cdvr 13627 |
Extend class notation with ring division.
|
/r |
|
Definition | df-dvr 13628* |
Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|
/r  
     Unit 
                   |
|
Theorem | dvrfvald 13629* |
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 13630 |
Division operation in a ring. (Contributed by Mario Carneiro,
2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|
             Unit          /r   
      
         |
|
Theorem | dvrcl 13631 |
Closure of division operation. (Contributed by Mario Carneiro,
2-Jul-2014.)
|
    Unit 
/r   
  
  |
|
Theorem | unitdvcl 13632 |
The units are closed under division. (Contributed by Mario Carneiro,
2-Jul-2014.)
|
Unit 
/r   
  
  |
|
Theorem | dvrid 13633 |
A ring element divided by itself is the ring unity. (dividap 8720
analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|
Unit 
/r          
 |
|
Theorem | dvr1 13634 |
A ring element divided by the ring unity is itself. (div1 8722
analog.)
(Contributed by Mario Carneiro, 18-Jun-2015.)
|
   
/r         
  |
|
Theorem | dvrass 13635 |
An associative law for division. (divassap 8709 analog.) (Contributed by
Mario Carneiro, 4-Dec-2014.)
|
    Unit 
/r 
     
     
       |
|
Theorem | dvrcan1 13636 |
A cancellation law for division. (divcanap1 8700 analog.) (Contributed
by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro,
2-Dec-2014.)
|
    Unit 
/r 
     
       |
|
Theorem | dvrcan3 13637 |
A cancellation law for division. (divcanap3 8717 analog.) (Contributed
by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro,
18-Jun-2015.)
|
    Unit 
/r 
     
    
  |
|
Theorem | dvreq1 13638 |
Equality in terms of ratio equal to ring unity. (diveqap1 8724 analog.)
(Contributed by Mario Carneiro, 28-Apr-2016.)
|
    Unit 
/r       
   
   |
|
Theorem | dvrdir 13639 |
Distributive law for the division operation of a ring. (Contributed by
Thierry Arnoux, 30-Oct-2017.)
|
    Unit 
   /r    
 
   
        |
|
Theorem | rdivmuldivd 13640 |
Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18.
(Contributed by Thierry Arnoux, 30-Oct-2017.)
|
    Unit 
   /r 
      
                
     |
|
Theorem | ringinvdv 13641 |
Write the inverse function in terms of division. (Contributed by Mario
Carneiro, 2-Jul-2014.)
|
    Unit 
/r     
          
   |
|
Theorem | rngidpropdg 13642* |
The ring unity depends only on the ring's base set and multiplication
operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|
              
 
                                |
|
Theorem | dvdsrpropdg 13643* |
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 13644* |
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 13645* |
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 13646 |
Extend class notation with the ring homomorphisms.
|
RingHom |
|
Syntax | crs 13647 |
Extend class notation with the ring isomorphisms.
|
RingIso |
|
Definition | df-rhm 13648* |
Define the set of ring homomorphisms from to .
(Contributed
by Stefan O'Rear, 7-Mar-2015.)
|
RingHom         ![]_ ]_](_urbrack.gif)       ![]_ ]_](_urbrack.gif)                  
                                                            |
|
Definition | df-rim 13649* |
Define the set of ring isomorphisms from to .
(Contributed
by Stefan O'Rear, 7-Mar-2015.)
|
RingIso  
  RingHom 

 RingHom     |
|
Theorem | dfrhm2 13650* |
The property of a ring homomorphism can be decomposed into separate
homomorphic conditions for addition and multiplication. (Contributed by
Stefan O'Rear, 7-Mar-2015.)
|
RingHom       mulGrp  MndHom mulGrp      |
|
Theorem | rhmrcl1 13651 |
Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear,
7-Mar-2015.)
|
  RingHom    |
|
Theorem | rhmrcl2 13652 |
Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear,
7-Mar-2015.)
|
  RingHom    |
|
Theorem | rhmex 13653 |
Set existence for ring homomorphism. (Contributed by Jim Kingdon,
16-May-2025.)
|
    RingHom    |
|
Theorem | isrhm 13654 |
A function is a ring homomorphism iff it preserves both addition and
multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|
mulGrp  mulGrp    RingHom   

    MndHom      |
|
Theorem | rhmmhm 13655 |
A ring homomorphism is a homomorphism of multiplicative monoids.
(Contributed by Stefan O'Rear, 7-Mar-2015.)
|
mulGrp  mulGrp    RingHom   MndHom
   |
|
Theorem | rimrcl 13656 |
Reverse closure for an isomorphism of rings. (Contributed by AV,
22-Oct-2019.)
|
  RingIso  
   |
|
Theorem | isrim0 13657 |
A ring isomorphism is a homomorphism whose converse is also a
homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood
antecedent. (Revised by SN, 10-Jan-2025.)
|
  RingIso   
RingHom    RingHom     |
|
Theorem | rhmghm 13658 |
A ring homomorphism is an additive group homomorphism. (Contributed by
Stefan O'Rear, 7-Mar-2015.)
|
  RingHom      |
|
Theorem | rhmf 13659 |
A ring homomorphism is a function. (Contributed by Stefan O'Rear,
8-Mar-2015.)
|
         
RingHom        |
|
Theorem | rhmmul 13660 |
A homomorphism of rings preserves multiplication. (Contributed by Mario
Carneiro, 12-Jun-2015.)
|
   
          
RingHom 
                   |
|
Theorem | isrhm2d 13661* |
Demonstration of ring homomorphism. (Contributed by Mario Carneiro,
13-Jun-2015.)
|
       
   
        
         
 
          
            RingHom
   |
|
Theorem | isrhmd 13662* |
Demonstration of ring homomorphism. (Contributed by Stefan O'Rear,
8-Mar-2015.)
|
       
   
        
         
 
          
                        
 
          
        RingHom
   |
|
Theorem | rhm1 13663 |
Ring homomorphisms are required to fix 1. (Contributed by Stefan
O'Rear, 8-Mar-2015.)
|
        
 RingHom      |
|
Theorem | rhmf1o 13664 |
A ring homomorphism is bijective iff its converse is also a ring
homomorphism. (Contributed by AV, 22-Oct-2019.)
|
         
RingHom       
 RingHom     |
|
Theorem | isrim 13665 |
An isomorphism of rings is a bijective homomorphism. (Contributed by
AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN,
12-Jan-2025.)
|
         
RingIso   
RingHom         |
|
Theorem | rimf1o 13666 |
An isomorphism of rings is a bijection. (Contributed by AV,
22-Oct-2019.)
|
         
RingIso        |
|
Theorem | rimrhm 13667 |
A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.)
Remove hypotheses. (Revised by SN, 10-Jan-2025.)
|
  RingIso   RingHom
   |
|
Theorem | rhmfn 13668 |
The mapping of two rings to the ring homomorphisms between them is a
function. (Contributed by AV, 1-Mar-2020.)
|
RingHom 
  |
|
Theorem | rhmval 13669 |
The ring homomorphisms between two rings. (Contributed by AV,
1-Mar-2020.)
|
    RingHom
     mulGrp  MndHom mulGrp      |
|
Theorem | rhmco 13670 |
The composition of ring homomorphisms is a homomorphism. (Contributed by
Mario Carneiro, 12-Jun-2015.)
|
  
RingHom 
 RingHom      RingHom
   |
|
Theorem | rhmdvdsr 13671 |
A ring homomorphism preserves the divisibility relation. (Contributed
by Thierry Arnoux, 22-Oct-2017.)
|
     r 
 r      RingHom              |
|
Theorem | rhmopp 13672 |
A ring homomorphism is also a ring homomorphism for the opposite rings.
(Contributed by Thierry Arnoux, 27-Oct-2017.)
|
  RingHom   oppr  RingHom oppr     |
|
Theorem | elrhmunit 13673 |
Ring homomorphisms preserve unit elements. (Contributed by Thierry
Arnoux, 23-Oct-2017.)
|
  
RingHom 
Unit  
    Unit    |
|
Theorem | rhmunitinv 13674 |
Ring homomorphisms preserve the inverse of unit elements. (Contributed by
Thierry Arnoux, 23-Oct-2017.)
|
  
RingHom 
Unit  
           
              |
|
7.3.9 Nonzero rings and zero rings
|
|
Syntax | cnzr 13675 |
The class of nonzero rings.
|
NzRing |
|
Definition | df-nzr 13676 |
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 13677 |
Property of a nonzero ring. (Contributed by Stefan O'Rear,
24-Feb-2015.)
|
        
NzRing    |
|
Theorem | nzrnz 13678 |
One and zero are different in a nonzero ring. (Contributed by Stefan
O'Rear, 24-Feb-2015.)
|
        
NzRing  |
|
Theorem | nzrring 13679 |
A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
(Proof shortened by SN, 23-Feb-2025.)
|
 NzRing   |
|
Theorem | isnzr2 13680 |
Equivalent characterization of nonzero rings: they have at least two
elements. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|
     NzRing     |
|
Theorem | opprnzrbg 13681 |
The opposite of a nonzero ring is nonzero, bidirectional form of
opprnzr 13682. (Contributed by SN, 20-Jun-2025.)
|
oppr    NzRing
NzRing  |
|
Theorem | opprnzr 13682 |
The opposite of a nonzero ring is nonzero. (Contributed by Mario
Carneiro, 17-Jun-2015.)
|
oppr   NzRing NzRing |
|
Theorem | ringelnzr 13683 |
A ring is nonzero if it has a nonzero element. (Contributed by Stefan
O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.)
|
         

  NzRing |
|
Theorem | nzrunit 13684 |
A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro,
6-Oct-2015.)
|
Unit        NzRing   |
|
Theorem | 01eq0ring 13685 |
If the zero and the identity element of a ring are the same, the ring is
the zero ring. (Contributed by AV, 16-Apr-2019.) (Proof shortened by
SN, 23-Feb-2025.)
|
                |
|
7.3.10 Local rings
|
|
Syntax | clring 13686 |
Extend class notation with class of all local rings.
|
LRing |
|
Definition | df-lring 13687* |
A local ring is a nonzero ring where for any two elements summing to
one, at least one is invertible. Any field is a local ring; the ring of
integers is an example of a ring which is not a local ring.
(Contributed by Jim Kingdon, 18-Feb-2025.) (Revised by SN,
23-Feb-2025.)
|
LRing  NzRing 
                        Unit  Unit      |
|
Theorem | islring 13688* |
The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
|
   
       Unit   LRing  NzRing      
     |
|
Theorem | lringnzr 13689 |
A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|
 LRing NzRing |
|
Theorem | lringring 13690 |
A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.)
(Revised by SN, 23-Feb-2025.)
|
 LRing   |
|
Theorem | lringnz 13691 |
A local ring is a nonzero ring. (Contributed by Jim Kingdon,
20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|
        
LRing  |
|
Theorem | lringuplu 13692 |
If the sum of two elements of a local ring is invertible, then at least
one of the summands must be invertible. (Contributed by Jim Kingdon,
18-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|
       Unit         LRing          
   |
|
7.3.11 Subrings
|
|
7.3.11.1 Subrings of non-unital
rings
|
|
Syntax | csubrng 13693 |
Extend class notation with all subrings of a non-unital ring.
|
SubRng |
|
Definition | df-subrng 13694* |
Define a subring of a non-unital ring as a set of elements that is a
non-unital ring in its own right. In this section, a subring of a
non-unital ring is simply called "subring", unless it causes
any
ambiguity with SubRing. (Contributed by AV, 14-Feb-2025.)
|
SubRng  Rng      
 ↾s 
Rng  |
|
Theorem | issubrng 13695 |
The subring of non-unital ring predicate. (Contributed by AV,
14-Feb-2025.)
|
     SubRng   Rng 
↾s  Rng    |
|
Theorem | subrngss 13696 |
A subring is a subset. (Contributed by AV, 14-Feb-2025.)
|
     SubRng    |
|
Theorem | subrngid 13697 |
Every non-unital ring is a subring of itself. (Contributed by AV,
14-Feb-2025.)
|
     Rng SubRng    |
|
Theorem | subrngrng 13698 |
A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
|
 ↾s   SubRng  Rng |
|
Theorem | subrngrcl 13699 |
Reverse closure for a subring predicate. (Contributed by AV,
14-Feb-2025.)
|
 SubRng  Rng |
|
Theorem | subrngsubg 13700 |
A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
|
 SubRng  SubGrp    |