P. 145 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14401-14500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	crngunit 14401	Property of being a unit in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( R e. CRing -> ( X e. U <-> X .|| .1. ) )
Theorem	dvdsunit 14402	A divisor of a unit is a unit. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. CRing /\ Y .|| X /\ X e. U ) -> Y e. U )
Theorem	unitmulcl 14403	The product of units is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X .x. Y ) e. U )
Theorem	unitmulclb 14404	Reversal of unitmulcl 14403 in a commutative ring. (Contributed by Mario Carneiro, 18-Apr-2016.)
|- U = (Unit ` R )   &    |- .x. = ( .r ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) e. U <-> ( X e. U /\ Y e. U ) ) )
Theorem	unitgrpbasd 14405	The base set of the group of units. (Contributed by Mario Carneiro, 25-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> G = ( (mulGrp ` R ) ↾s U ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> U = ( Base ` G ) )
Theorem	unitgrp 14406	The group of units is a group under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. Ring -> G e. Grp )
Theorem	unitabl 14407	The group of units of a commutative ring is abelian. (Contributed by Mario Carneiro, 19-Apr-2016.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   =>    |- ( R e. CRing -> G e. Abel )
Theorem	unitgrpid 14408	The identity of the group of units of a ring is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- G = ( (mulGrp ` R ) ↾s U )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. = ( 0g ` G ) )
Theorem	unitsubm 14409	The group of units is a submonoid of the multiplicative monoid of the ring. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- M = (mulGrp ` R )   =>    |- ( R e. Ring -> U e. (SubMnd ` M ) )
Syntax	cinvr 14410	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 14411	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
Theorem	invrfvald 14412	Multiplicative inverse function for a ring. (Contributed by NM, 21-Sep-2011.) (Revised by Mario Carneiro, 25-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> G = ( (mulGrp ` R ) ↾s U ) )   &    |- ( ph -> I = ( invr ` R ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> I = ( invg ` G ) )
Theorem	unitinvcl 14413	The inverse of a unit exists and is a unit. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. U )
Theorem	unitinvinv 14414	The inverse of the inverse of a unit is the same element. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` ( I ` X ) ) = X )
Theorem	ringinvcl 14415	The inverse of a unit is an element of the ring. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( I ` X ) e. B )
Theorem	unitlinv 14416	A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( ( I ` X ) .x. X ) = .1. )
Theorem	unitrinv 14417	A unit times its inverse is the ring unity. (Contributed by Mario Carneiro, 2-Dec-2014.)
|- U = (Unit ` R )   &    |- I = ( invr ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( X .x. ( I ` X ) ) = .1. )
Theorem	1rinv 14418	The inverse of the ring unity is the ring unity. (Contributed by Mario Carneiro, 18-Jun-2015.)
|- I = ( invr ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( I ` .1. ) = .1. )
Theorem	0unit 14419	The additive identity is a unit if and only if 1 = 0, i.e. we are in the zero ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( .0. e. U <-> .1. = .0. ) )
Theorem	unitnegcl 14420	The negative of a unit is a unit. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- U = (Unit ` R )   &    |- N = ( invg ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( N ` X ) e. U )
Syntax	cdvr 14421	Extend class notation with ring division.
class /r
Definition	df-dvr 14422*	Define ring division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- /r = ( r e. _V |-> ( x e. ( Base ` r ) , y e. (Unit ` r ) |-> ( x ( .r ` r ) ( ( invr ` r ) ` y ) ) ) )
Theorem	dvrfvald 14423*	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.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> I = ( invr ` R ) )   &    |- ( ph -> ./ = (/r ` R ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> ./ = ( x e. B , y e. U |-> ( x .x. ( I ` y ) ) ) )
Theorem	dvrvald 14424	Division operation in a ring. (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> I = ( invr ` R ) )   &    |- ( ph -> ./ = (/r ` R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. U )   =>    |- ( ph -> ( X ./ Y ) = ( X .x. ( I ` Y ) ) )
Theorem	dvrcl 14425	Closure of division operation. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( X ./ Y ) e. B )
Theorem	unitdvcl 14426	The units are closed under division. (Contributed by Mario Carneiro, 2-Jul-2014.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   =>    |- ( ( R e. Ring /\ X e. U /\ Y e. U ) -> ( X ./ Y ) e. U )
Theorem	dvrid 14427	A ring element divided by itself is the ring unity. (dividap 9025 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. U ) -> ( X ./ X ) = .1. )
Theorem	dvr1 14428	A ring element divided by the ring unity is itself. (div1 9027 analog.) (Contributed by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( X ./ .1. ) = X )
Theorem	dvrass 14429	An associative law for division. (divassap 9014 analog.) (Contributed by Mario Carneiro, 4-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( X e. B /\ Y e. B /\ Z e. U ) ) -> ( ( X .x. Y ) ./ Z ) = ( X .x. ( Y ./ Z ) ) )
Theorem	dvrcan1 14430	A cancellation law for division. (divcanap1 9005 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 2-Dec-2014.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) .x. Y ) = X )
Theorem	dvrcan3 14431	A cancellation law for division. (divcanap3 9022 analog.) (Contributed by Mario Carneiro, 2-Jul-2014.) (Revised by Mario Carneiro, 18-Jun-2015.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X .x. Y ) ./ Y ) = X )
Theorem	dvreq1 14432	Equality in terms of ratio equal to ring unity. (diveqap1 9029 analog.) (Contributed by Mario Carneiro, 28-Apr-2016.)
|- B = ( Base ` R )   &    |- U = (Unit ` R )   &    |- ./ = (/r ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ X e. B /\ Y e. U ) -> ( ( X ./ Y ) = .1. <-> X = Y ) )
Theorem	dvrdir 14433	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 14434	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 14435	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 14436*	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 14437*	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 14438*	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 14439*	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 14440	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 14441	Extend class notation with the ring isomorphisms.
class RingIso
Definition	df-rhm 14442*	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 14443*	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 14444*	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 14445	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> R e. Ring )
Theorem	rhmrcl2 14446	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> S e. Ring )
Theorem	rhmex 14447	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 14448	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 14449	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 14450	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 14451	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 14452	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 14453	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 14454	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 14455*	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 14456*	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 14457	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 14458	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 14459	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 14460	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 14461	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 14462	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 14463	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 14464	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 14465	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 14466	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 14467	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 14468	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 14469	The class of nonzero rings.
class NzRing
Definition	df-nzr 14470	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 14471	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 14472	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 14473	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 14474	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 14475	The opposite of a nonzero ring is nonzero, bidirectional form of opprnzr 14476. (Contributed by SN, 20-Jun-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. NzRing <-> O e. NzRing ) )
Theorem	opprnzr 14476	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 14477	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 14478	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 14479	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 14480	Extend class notation with class of all local rings.
class LRing
Definition	df-lring 14481*	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 14482*	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 14483	A local ring is a nonzero ring. (Contributed by SN, 23-Feb-2025.)
|- ( R e. LRing -> R e. NzRing )
Theorem	lringring 14484	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 14485	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 14486	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 ) )
Theorem	opprlring 14487	The opposite of a local ring is also a local ring. (Contributed by NM, 18-Oct-2014.)
|- O = (oppr ` R )   =>    |- ( R e. LRing <-> O e. LRing )
7.3.11  Subrings
7.3.11.1  Subrings of non-unital rings
Syntax	csubrng 14488	Extend class notation with all subrings of a non-unital ring.
class SubRng
Definition	df-subrng 14489*	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 14490	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 14491	A subring is a subset. (Contributed by AV, 14-Feb-2025.)
|- B = ( Base ` R )   =>    |- ( A e. (SubRng ` R ) -> A C_ B )
Theorem	subrngid 14492	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 14493	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 14494	Reverse closure for a subring predicate. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> R e. Rng )
Theorem	subrngsubg 14495	A subring is a subgroup. (Contributed by AV, 14-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (SubGrp ` R ) )
Theorem	subrngringnsg 14496	A subring is a normal subgroup. (Contributed by AV, 25-Feb-2025.)
|- ( A e. (SubRng ` R ) -> A e. (NrmSGrp ` R ) )
Theorem	subrngbas 14497	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 14498	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 14499	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 14500	A subgroup is closed under multiplication. (Contributed by Mario Carneiro, 2-Dec-2014.) Generalization of subrgmcl 14524. (Revised by AV, 14-Feb-2025.)
|- .x. = ( .r ` R )   =>    |- ( ( A e. (SubRng ` R ) /\ X e. A /\ Y e. A ) -> ( X .x. Y ) e. A )