P. 138 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 13701-13800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringinvdv 13701	Write the inverse function in terms of division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) = ( .1. ./ X ) )
Theorem	rngidpropdg 13702*	The ring unity depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. V )   &    |- ( ph -> L e. W )   =>    |- ( ph -> ( 1r ` K ) = ( 1r ` L ) )
Theorem	dvdsrpropdg 13703*	The divisibility relation depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. SRing )   &    |- ( ph -> L e. SRing )   =>    |- ( ph -> ( ||r ` K ) = ( ||r ` L ) )
Theorem	unitpropdg 13704*	The set of units depends only on the ring's base set and multiplication operation. (Contributed by Mario Carneiro, 26-Dec-2014.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. Ring )   &    |- ( ph -> L e. Ring )   =>    |- ( ph -> (Unit ` K ) = (Unit ` L ) )
Theorem	invrpropdg 13705*	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.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. Ring )   &    |- ( ph -> L e. Ring )   =>    |- ( ph -> ( invr ` K ) = ( invr ` L ) )
7.3.8  Ring homomorphisms
Syntax	crh 13706	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 13707	Extend class notation with the ring isomorphisms.
class RingIso
Definition	df-rhm 13708*	Define the set of ring homomorphisms from r to s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- RingHom = ( r e. Ring , s e. Ring |-> [_ ( Base ` r ) / v ]_ [_ ( Base ` s ) / w ]_ { f e. ( w ^m v ) | ( ( f ` ( 1r ` r ) ) = ( 1r ` s ) /\ A. x e. v A. y e. v ( ( f ` ( x ( +g ` r ) y ) ) = ( ( f ` x ) ( +g ` s ) ( f ` y ) ) /\ ( f ` ( x ( .r ` r ) y ) ) = ( ( f ` x ) ( .r ` s ) ( f ` y ) ) ) ) } )
Definition	df-rim 13709*	Define the set of ring isomorphisms from r to s. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- RingIso = ( r e. _V , s e. _V |-> { f e. ( r RingHom s ) | `' f e. ( s RingHom r ) } )
Theorem	dfrhm2 13710*	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 = ( r e. Ring , s e. Ring |-> ( ( r GrpHom s ) i^i ( (mulGrp ` r ) MndHom (mulGrp ` s ) ) ) )
Theorem	rhmrcl1 13711	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> R e. Ring )
Theorem	rhmrcl2 13712	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> S e. Ring )
Theorem	rhmex 13713	Set existence for ring homomorphism. (Contributed by Jim Kingdon, 16-May-2025.)
|- ( ( R e. V /\ S e. W ) -> ( R RingHom S ) e. _V )
Theorem	isrhm 13714	A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RingHom S ) <-> ( ( R e. Ring /\ S e. Ring ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MndHom N ) ) ) )
Theorem	rhmmhm 13715	A ring homomorphism is a homomorphism of multiplicative monoids. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- M = (mulGrp ` R )   &    |- N = (mulGrp ` S )   =>    |- ( F e. ( R RingHom S ) -> F e. ( M MndHom N ) )
Theorem	rimrcl 13716	Reverse closure for an isomorphism of rings. (Contributed by AV, 22-Oct-2019.)
|- ( F e. ( R RingIso S ) -> ( R e. _V /\ S e. _V ) )
Theorem	isrim0 13717	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.)
|- ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ `' F e. ( S RingHom R ) ) )
Theorem	rhmghm 13718	A ring homomorphism is an additive group homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
Theorem	rhmf 13719	A ring homomorphism is a function. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RingHom S ) -> F : B --> C )
Theorem	rhmmul 13720	A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- X = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   =>    |- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )
Theorem	isrhm2d 13721*	Demonstration of ring homomorphism. (Contributed by Mario Carneiro, 13-Jun-2015.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> S e. Ring )   &    |- ( ph -> ( F ` .1. ) = N )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- ( ph -> F e. ( R GrpHom S ) )   =>    |- ( ph -> F e. ( R RingHom S ) )
Theorem	isrhmd 13722*	Demonstration of ring homomorphism. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` S )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> S e. Ring )   &    |- ( ph -> ( F ` .1. ) = N )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .x. y ) ) = ( ( F ` x ) .X. ( F ` y ) ) )   &    |- C = ( Base ` S )   &    |- .+ = ( +g ` R )   &    |- .+^ = ( +g ` S )   &    |- ( ph -> F : B --> C )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( F ` ( x .+ y ) ) = ( ( F ` x ) .+^ ( F ` y ) ) )   =>    |- ( ph -> F e. ( R RingHom S ) )
Theorem	rhm1 13723	Ring homomorphisms are required to fix 1. (Contributed by Stefan O'Rear, 8-Mar-2015.)
|- .1. = ( 1r ` R )   &    |- N = ( 1r ` S )   =>    |- ( F e. ( R RingHom S ) -> ( F ` .1. ) = N )
Theorem	rhmf1o 13724	A ring homomorphism is bijective iff its converse is also a ring homomorphism. (Contributed by AV, 22-Oct-2019.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RingHom S ) -> ( F : B -1-1-onto-> C <-> `' F e. ( S RingHom R ) ) )
Theorem	isrim 13725	An isomorphism of rings is a bijective homomorphism. (Contributed by AV, 22-Oct-2019.) Remove sethood antecedent. (Revised by SN, 12-Jan-2025.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RingIso S ) <-> ( F e. ( R RingHom S ) /\ F : B -1-1-onto-> C ) )
Theorem	rimf1o 13726	An isomorphism of rings is a bijection. (Contributed by AV, 22-Oct-2019.)
|- B = ( Base ` R )   &    |- C = ( Base ` S )   =>    |- ( F e. ( R RingIso S ) -> F : B -1-1-onto-> C )
Theorem	rimrhm 13727	A ring isomorphism is a homomorphism. (Contributed by AV, 22-Oct-2019.) Remove hypotheses. (Revised by SN, 10-Jan-2025.)
|- ( F e. ( R RingIso S ) -> F e. ( R RingHom S ) )
Theorem	rhmfn 13728	The mapping of two rings to the ring homomorphisms between them is a function. (Contributed by AV, 1-Mar-2020.)
|- RingHom Fn ( Ring X. Ring )
Theorem	rhmval 13729	The ring homomorphisms between two rings. (Contributed by AV, 1-Mar-2020.)
|- ( ( R e. Ring /\ S e. Ring ) -> ( R RingHom S ) = ( ( R GrpHom S ) i^i ( (mulGrp ` R ) MndHom (mulGrp ` S ) ) ) )
Theorem	rhmco 13730	The composition of ring homomorphisms is a homomorphism. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ( F e. ( T RingHom U ) /\ G e. ( S RingHom T ) ) -> ( F o. G ) e. ( S RingHom U ) )
Theorem	rhmdvdsr 13731	A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- X = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- ./ = ( ||r ` S )   =>    |- ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) )
Theorem	rhmopp 13732	A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.)
|- ( F e. ( R RingHom S ) -> F e. ( (oppr ` R ) RingHom (oppr ` S ) ) )
Theorem	elrhmunit 13733	Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
|- ( ( F e. ( R RingHom S ) /\ A e. (Unit ` R ) ) -> ( F ` A ) e. (Unit ` S ) )
Theorem	rhmunitinv 13734	Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
|- ( ( F e. ( R RingHom S ) /\ A e. (Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) )
7.3.9  Nonzero rings and zero rings
Syntax	cnzr 13735	The class of nonzero rings.
class NzRing
Definition	df-nzr 13736	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 = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
Theorem	isnzr 13737	Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )
Theorem	nzrnz 13738	One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. NzRing -> .1. =/= .0. )
Theorem	nzrring 13739	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) (Proof shortened by SN, 23-Feb-2025.)
|- ( R e. NzRing -> R e. Ring )
Theorem	isnzr2 13740	Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- B = ( Base ` R )   =>    |- ( R e. NzRing <-> ( R e. Ring /\ 2o ~<_ B ) )
Theorem	opprnzrbg 13741	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 13742. (Contributed by SN, 20-Jun-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. NzRing <-> O e. NzRing ) )
Theorem	opprnzr 13742	The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. NzRing -> O e. NzRing )
Theorem	ringelnzr 13743	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.)
|- .0. = ( 0g ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )
Theorem	nzrunit 13744	A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. NzRing /\ A e. U ) -> A =/= .0. )
Theorem	01eq0ring 13745	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.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )
7.3.10  Local rings
Syntax	clring 13746	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 13747*	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 = { r e. NzRing | A. x e. ( Base ` r ) A. y e. ( Base ` r ) ( ( x ( +g ` r ) y ) = ( 1r ` r ) -> ( x e. (Unit ` r ) \/ y e. (Unit ` r ) ) ) }
Theorem	islring 13748*	The predicate "is a local ring". (Contributed by SN, 23-Feb-2025.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .1. = ( 1r ` R )   &    |- U = (Unit ` R )   =>    |- ( R e. LRing <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .+ y ) = .1. -> ( x e. U \/ y e. U ) ) ) )
Theorem	lringnzr 13749	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|- ( R e. LRing -> R e. NzRing )
Theorem	lringring 13750	A local ring is a ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|- ( R e. LRing -> R e. Ring )
Theorem	lringnz 13751	A local ring is a nonzero ring. (Contributed by Jim Kingdon, 20-Feb-2025.) (Revised by SN, 23-Feb-2025.)
|- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. LRing -> .1. =/= .0. )
Theorem	lringuplu 13752	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.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> .+ = ( +g ` R ) )   &    |- ( ph -> R e. LRing )   &    |- ( ph -> ( X .+ Y ) e. U )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( X e. U \/ Y e. U ) )
7.3.11  Subrings
7.3.11.1  Subrings of non-unital rings
Syntax	csubrng 13753	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 13754*	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 = ( w e. Rng |-> { s e. ~P ( Base ` w ) | ( w ↾s s ) e. Rng } )
Theorem	issubrng 13755	The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRng ` R ) <-> ( R e. Rng /\ ( R ↾s A ) e. Rng /\ A C_ B ) )
Theorem	subrngss 13756	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRng ` R ) -> A C_ B )
Theorem	subrngid 13757	Every non-unital ring is a subring of itself. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( R e. Rng -> B e. (SubRng ` R ) )
Theorem	subrngrng 13758	A subring is a non-unital ring. (Contributed by AV, 14-Feb-2025.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRng ` R ) -> S e. Rng )
Theorem	subrngrcl 13759	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> R e. Rng )
Theorem	subrngsubg 13760	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrngringnsg 13761	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (NrmSGrp ` R ) )
Theorem	subrngbas 13762	Base set of a subring structure. (Contributed by AV, 14-Feb-2025.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRng ` R ) -> A = ( Base ` S ) )
Theorem	subrng0 13763	A subring always has the same additive identity. (Contributed by AV, 14-Feb-2025.)
|- S = ( R ↾s A )   &    |- .0. = ( 0g ` R )   =>    |- ( A e. (SubRng ` R ) -> .0. = ( 0g ` S ) )
Theorem	subrngacl 13764	A subring is closed under addition. (Contributed by AV, 14-Feb-2025.)
|- .+ = ( +g ` R )   =>    |- ( ( A e. (SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )
Theorem	subrngmcl 13765	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 13789. (Revised by AV, 14-Feb-2025.)
|- .x. = ( .r ` R )   =>    |- ( ( A e. (SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )
Theorem	issubrng2 13766*	Characterize the subrings of a ring by closure properties. (Contributed by AV, 15-Feb-2025.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Rng -> ( A e. (SubRng ` R ) <-> ( A e. (SubGrp ` R ) /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )
Theorem	opprsubrngg 13767	Being a subring is a symmetric property. (Contributed by AV, 15-Feb-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> (SubRng ` R ) = (SubRng ` O ) )
Theorem	subrngintm 13768*	The intersection of a nonempty collection of subrings is a subring. (Contributed by AV, 15-Feb-2025.)
|- ( ( S C_ (SubRng ` R ) /\ E. j j e. S ) -> |^| S e. (SubRng ` R ) )
Theorem	subrngin 13769	The intersection of two subrings is a subring. (Contributed by AV, 15-Feb-2025.)
|- ( ( A e. (SubRng ` R ) /\ B e. (SubRng ` R ) ) -> ( A i^i B ) e. (SubRng ` R ) )
Theorem	subsubrng 13770	A subring of a subring is a subring. (Contributed by AV, 15-Feb-2025.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRng ` R ) -> ( B e. (SubRng ` S ) <-> ( B e. (SubRng ` R ) /\ B C_ A ) ) )
Theorem	subsubrng2 13771	The set of subrings of a subring are the smaller subrings. (Contributed by AV, 15-Feb-2025.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRng ` R ) -> (SubRng ` S ) = ( (SubRng ` R ) i^i ~P A ) )
Theorem	subrngpropd 13772*	If two structures have the same ring components (properties), they have the same set of subrings. (Contributed by AV, 17-Feb-2025.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   =>    |- ( ph -> (SubRng ` K ) = (SubRng ` L ) )
7.3.11.2  Subrings of unital rings
Syntax	csubrg 13773	Extend class notation with all subrings of a ring.
class SubRing
Syntax	crgspn 13774	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-subrg 13775*	Define a subring of a ring as a set of elements that is a ring in its own right and contains the multiplicative identity. The additional constraint is necessary because the multiplicative identity of a ring, unlike the additive identity of a ring/group or the multiplicative identity of a field, cannot be identified by a local property. Thus, it is possible for a subset of a ring to be a ring while not containing the true identity if it contains a false identity. For instance, the subset ( ZZ X. { 0 } ) of ( ZZ X. ZZ ) (where multiplication is componentwise) contains the false identity <. 1 , 0 >. which preserves every element of the subset and thus appears to be the identity of the subset, but is not the identity of the larger ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- SubRing = ( w e. Ring |-> { s e. ~P ( Base ` w ) | ( ( w ↾s s ) e. Ring /\ ( 1r ` w ) e. s ) } )
Definition	df-rgspn 13776*	The ring-span of a set of elements in a ring is the smallest subring which contains all of them. (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- RingSpan = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> |^| { t e. (SubRing ` w ) | s C_ t } ) )
Theorem	issubrg 13777	The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Proof shortened by AV, 12-Oct-2020.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) <-> ( ( R e. Ring /\ ( R ↾s A ) e. Ring ) /\ ( A C_ B /\ .1. e. A ) ) )
Theorem	subrgss 13778	A subring is a subset. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRing ` R ) -> A C_ B )
Theorem	subrgid 13779	Every ring is a subring of itself. (Contributed by Stefan O'Rear, 30-Nov-2014.)
|- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. (SubRing ` R ) )
Theorem	subrgring 13780	A subring is a ring. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> S e. Ring )
Theorem	subrgcrng 13781	A subring of a commutative ring is a commutative ring. (Contributed by Mario Carneiro, 10-Jan-2015.)
|- S = ( R ↾s A )   =>    |- ( ( R e. CRing /\ A e. (SubRing ` R ) ) -> S e. CRing )
Theorem	subrgrcl 13782	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> R e. Ring )
Theorem	subrgsubg 13783	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrg0 13784	A subring always has the same additive identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .0. = ( 0g ` R )   =>    |- ( A e. (SubRing ` R ) -> .0. = ( 0g ` S ) )
Theorem	subrg1cl 13785	A subring contains the multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) -> .1. e. A )
Theorem	subrgbas 13786	Base set of a subring structure. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> A = ( Base ` S ) )
Theorem	subrg1 13787	A subring always has the same multiplicative identity. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- S = ( R ↾s A )   &    |- .1. = ( 1r ` R )   =>    |- ( A e. (SubRing ` R ) -> .1. = ( 1r ` S ) )
Theorem	subrgacl 13788	A subring is closed under addition. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .+ = ( +g ` R )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .+ Y ) e. A )
Theorem	subrgmcl 13789	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- .x. = ( .r ` R )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )
Theorem	subrgsubm 13790	A subring is a submonoid of the multiplicative monoid. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- M = (mulGrp ` R )   =>    |- ( A e. (SubRing ` R ) -> A e. (SubMnd ` M ) )
Theorem	subrgdvds 13791	If an element divides another in a subring, then it also divides the other in the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- .|| = ( ||r ` R )   &    |- E = ( ||r ` S )   =>    |- ( A e. (SubRing ` R ) -> E C_ .|| )
Theorem	subrguss 13792	A unit of a subring is a unit of the parent ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   =>    |- ( A e. (SubRing ` R ) -> V C_ U )
Theorem	subrginv 13793	A subring always has the same inversion function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- I = ( invr ` R )   &    |- U = (Unit ` S )   &    |- J = ( invr ` S )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. U ) -> ( I ` X ) = ( J ` X ) )
Theorem	subrgdv 13794	A subring always has the same division function, for elements that are invertible. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- ./ = (/r ` R )   &    |- U = (Unit ` S )   &    |- E = (/r ` S )   =>    |- ( ( A e. (SubRing ` R ) /\ X e. A /\ Y e. U ) -> ( X ./ Y ) = ( X E Y ) )
Theorem	subrgunit 13795	An element of a ring is a unit of a subring iff it is a unit of the parent ring and both it and its inverse are in the subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   &    |- I = ( invr ` R )   =>    |- ( A e. (SubRing ` R ) -> ( X e. V <-> ( X e. U /\ X e. A /\ ( I ` X ) e. A ) ) )
Theorem	subrgugrp 13796	The units of a subring form a subgroup of the unit group of the original ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   &    |- U = (Unit ` R )   &    |- V = (Unit ` S )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( A e. (SubRing ` R ) -> V e. (SubGrp ` G ) )
Theorem	issubrg2 13797*	Characterize the subrings of a ring by closure properties. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( A e. (SubRing ` R ) <-> ( A e. (SubGrp ` R ) /\ .1. e. A /\ A. x e. A A. y e. A ( x .x. y ) e. A ) ) )
Theorem	subrgnzr 13798	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- S = ( R ↾s A )   =>    |- ( ( R e. NzRing /\ A e. (SubRing ` R ) ) -> S e. NzRing )
Theorem	subrgintm 13799*	The intersection of an inhabited collection of subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( S C_ (SubRing ` R ) /\ E. w w e. S ) -> |^| S e. (SubRing ` R ) )
Theorem	subrgin 13800	The intersection of two subrings is a subring. (Contributed by Stefan O'Rear, 30-Nov-2014.) (Revised by Mario Carneiro, 7-Dec-2014.)
|- ( ( A e. (SubRing ` R ) /\ B e. (SubRing ` R ) ) -> ( A i^i B ) e. (SubRing ` R ) )