P. 144 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14301-14400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rhmrcl2 14301	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> S e. Ring )
Theorem	rhmex 14302	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 14303	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 14304	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 14305	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 14306	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 14307	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 14308	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 14309	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 14310*	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 14311*	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 14312	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 14313	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 14314	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 14315	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 14316	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 14317	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 14318	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 14319	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 14320	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 14321	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 14322	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 14323	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 14324	The class of nonzero rings.
class NzRing
Definition	df-nzr 14325	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 14326	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 14327	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 14328	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 14329	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 14330	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14331. (Contributed by SN, 20-Jun-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. NzRing <-> O e. NzRing ) )
Theorem	opprnzr 14331	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 14332	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 14333	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 14334	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 14335	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 14336*	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 14337*	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 14338	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|- ( R e. LRing -> R e. NzRing )
Theorem	lringring 14339	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 14340	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 14341	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 14342	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 14343*	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 14344	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 14345	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRng ` R ) -> A C_ B )
Theorem	subrngid 14346	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 14347	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 14348	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> R e. Rng )
Theorem	subrngsubg 14349	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrngringnsg 14350	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (NrmSGrp ` R ) )
Theorem	subrngbas 14351	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 14352	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 14353	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 14354	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14378. (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 14355*	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 14356	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 14357*	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 14358	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 14359	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 14360	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 14361*	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 14362	Extend class notation with all subrings of a ring.
class SubRing
Syntax	crgspn 14363	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-subrg 14364*	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 14365*	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 14366	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 14367	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 14368	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 14369	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 14370	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 14371	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> R e. Ring )
Theorem	subrgsubg 14372	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrg0 14373	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 14374	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 14375	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 14376	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 14377	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 14378	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 14379	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 14380	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 14381	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 14382	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 14383	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 14384	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 14385	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 14386*	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 14387	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 14388*	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 14389	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 ) )
Theorem	subsubrg 14390	A subring of a subring is a subring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> ( B e. (SubRing ` S ) <-> ( B e. (SubRing ` R ) /\ B C_ A ) ) )
Theorem	subsubrg2 14391	The set of subrings of a subring are the smaller subrings. (Contributed by Stefan O'Rear, 9-Mar-2015.)
|- S = ( R ↾s A )   =>    |- ( A e. (SubRing ` R ) -> (SubRing ` S ) = ( (SubRing ` R ) i^i ~P A ) )
Theorem	issubrg3 14392	A subring is an additive subgroup which is also a multiplicative submonoid. (Contributed by Mario Carneiro, 7-Mar-2015.)
|- M = (mulGrp ` R )   =>    |- ( R e. Ring -> ( S e. (SubRing ` R ) <-> ( S e. (SubGrp ` R ) /\ S e. (SubMnd ` M ) ) ) )
Theorem	resrhm 14393	Restriction of a ring homomorphism to a subring is a homomorphism. (Contributed by Mario Carneiro, 12-Mar-2015.)
|- U = ( S ↾s X )   =>    |- ( ( F e. ( S RingHom T ) /\ X e. (SubRing ` S ) ) -> ( F |` X ) e. ( U RingHom T ) )
Theorem	resrhm2b 14394	Restriction of the codomain of a (ring) homomorphism. resghm2b 13979 analog. (Contributed by SN, 7-Feb-2025.)
|- U = ( T ↾s X )   =>    |- ( ( X e. (SubRing ` T ) /\ ran F C_ X ) -> ( F e. ( S RingHom T ) <-> F e. ( S RingHom U ) ) )
Theorem	rhmeql 14395	The equalizer of two ring homomorphisms is a subring. (Contributed by Stefan O'Rear, 7-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( S RingHom T ) /\ G e. ( S RingHom T ) ) -> dom ( F i^i G ) e. (SubRing ` S ) )
Theorem	rhmima 14396	The homomorphic image of a subring is a subring. (Contributed by Stefan O'Rear, 10-Mar-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- ( ( F e. ( M RingHom N ) /\ X e. (SubRing ` M ) ) -> ( F " X ) e. (SubRing ` N ) )
Theorem	rnrhmsubrg 14397	The range of a ring homomorphism is a subring. (Contributed by SN, 18-Nov-2023.)
|- ( F e. ( M RingHom N ) -> ran F e. (SubRing ` N ) )
Theorem	subrgpropd 14398*	If two structures have the same group components (properties), they have the same set of subrings. (Contributed by Mario Carneiro, 9-Feb-2015.)
|- ( 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 -> (SubRing ` K ) = (SubRing ` L ) )
Theorem	rhmpropd 14399*	Ring homomorphism depends only on the ring attributes of structures. (Contributed by Mario Carneiro, 12-Jun-2015.)
|- ( ph -> B = ( Base ` J ) )   &    |- ( ph -> C = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> C = ( Base ` M ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( +g ` J ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` M ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` J ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ( ph /\ ( x e. C /\ y e. C ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` M ) y ) )   =>    |- ( ph -> ( J RingHom K ) = ( L RingHom M ) )
7.3.12  Left regular elements and domains
Syntax	crlreg 14400	Set of left-regular elements in a ring.
class RLReg