P. 142 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14101-14200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dvrdir 14101	Distributive law for the division operation of a ring. (Contributed by Thierry Arnoux, 30-Oct-2017.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .+ = ( +g ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .+ Y ) ./ Z ) = ( ( X ./ Z ) .+ ( Y ./ Z ) ) )
Theorem	rdivmuldivd 14102	Multiplication of two ratios. Theorem I.14 of [Apostol] p. 18. (Contributed by Thierry Arnoux, 30-Oct-2017.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- .+ = ( +g ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. U )   &    |- ( ph -> Z e. B )   &    |- ( ph -> W e. U )   =>    |- ( ph -> ( ( X ./ Y ) .x. ( Z ./ W ) ) = ( ( X .x. Z ) ./ ( Y .x. W ) ) )
Theorem	ringinvdv 14103	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 14104*	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 14105*	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 14106*	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 14107*	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 14108	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 14109	Extend class notation with the ring isomorphisms.
class RingIso
Definition	df-rhm 14110*	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 14111*	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 14112*	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 14113	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> R e. Ring )
Theorem	rhmrcl2 14114	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> S e. Ring )
Theorem	rhmex 14115	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 14116	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 14117	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 14118	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 14119	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 14120	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 14121	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 14122	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 14123*	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 14124*	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 14125	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 14126	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 14127	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 14128	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 14129	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 14130	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 14131	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 14132	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 14133	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 14134	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 14135	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 14136	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 14137	The class of nonzero rings.
class NzRing
Definition	df-nzr 14138	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 14139	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 14140	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 14141	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 14142	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 14143	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14144. (Contributed by SN, 20-Jun-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. NzRing <-> O e. NzRing ) )
Theorem	opprnzr 14144	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 14145	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 14146	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 14147	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 14148	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 14149*	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 14150*	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 14151	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|- ( R e. LRing -> R e. NzRing )
Theorem	lringring 14152	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 14153	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 14154	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 14155	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 14156*	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 14157	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 14158	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRng ` R ) -> A C_ B )
Theorem	subrngid 14159	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 14160	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 14161	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> R e. Rng )
Theorem	subrngsubg 14162	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrngringnsg 14163	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (NrmSGrp ` R ) )
Theorem	subrngbas 14164	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 14165	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 14166	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 14167	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14191. (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 14168*	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 14169	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 14170*	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 14171	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 14172	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 14173	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 14174*	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 14175	Extend class notation with all subrings of a ring.
class SubRing
Syntax	crgspn 14176	Extend class notation with span of a set of elements over a ring.
class RingSpan
Definition	df-subrg 14177*	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 14178*	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 14179	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 14180	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 14181	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 14182	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 14183	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 14184	Reverse closure for a subring predicate. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> R e. Ring )
Theorem	subrgsubg 14185	A subring is a subgroup. (Contributed by Mario Carneiro, 3-Dec-2014.)
|- ( A e. (SubRing ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrg0 14186	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 14187	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 14188	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 14189	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 14190	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 14191	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 14192	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 14193	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 14194	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 14195	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 14196	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 14197	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 14198	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 14199*	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 14200	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 )