P. 143 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14201-14300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	ringsubdir 14201	Ring multiplication distributes over subtraction. (subdir 8659 analog.) (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Mario Carneiro, 2-Jul-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   =>    |- ( ph -> ( ( X .- Y ) .x. Z ) = ( ( X .x. Z ) .- ( Y .x. Z ) ) )
Theorem	mulgass2 14202	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( ( N .x. X ) .X. Y ) = ( N .x. ( X .X. Y ) ) )
Theorem	ring1 14203	The (smallest) structure representing a zero ring. (Contributed by AV, 28-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   =>    |- ( Z e. V -> M e. Ring )
Theorem	ringn0 14204	The class of rings is not empty (it is also inhabited, as shown at ring1 14203). (Contributed by AV, 29-Apr-2019.)
|- Ring =/= (/)
Theorem	ringlghm 14205*	Left-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( X .x. x ) ) e. ( R GrpHom R ) )
Theorem	ringrghm 14206*	Right-multiplication in a ring by a fixed element of the ring is a group homomorphism. (It is not usually a ring homomorphism.) (Contributed by Mario Carneiro, 4-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( x e. B |-> ( x .x. X ) ) e. ( R GrpHom R ) )
Theorem	ringressid 14207	A ring restricted to its base set is a ring. It will usually be the original ring exactly, of course, but to show that needs additional conditions such as those in strressid 13284. (Contributed by Jim Kingdon, 28-Feb-2025.)
|- B = ( Base ` G )   =>    |- ( G e. Ring -> ( G ↾s B ) e. Ring )
Theorem	imasring 14208*	The image structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( F "s R ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- ( ph -> F : V -onto-> B )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .+ b ) ) = ( F ` ( p .+ q ) ) ) )   &    |- ( ( ph /\ ( a e. V /\ b e. V ) /\ ( p e. V /\ q e. V ) ) -> ( ( ( F ` a ) = ( F ` p ) /\ ( F ` b ) = ( F ` q ) ) -> ( F ` ( a .x. b ) ) = ( F ` ( p .x. q ) ) ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( U e. Ring /\ ( F ` .1. ) = ( 1r ` U ) ) )
Theorem	imasringf1 14209	The image of a ring under an injection is a ring. (Contributed by AV, 27-Feb-2025.)
|- U = ( F "s R )   &    |- V = ( Base ` R )   =>    |- ( ( F : V -1-1-> B /\ R e. Ring ) -> U e. Ring )
Theorem	qusring2 14210*	The quotient structure of a ring is a ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> U = ( R /.s .~ ) )   &    |- ( ph -> V = ( Base ` R ) )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   &    |- .1. = ( 1r ` R )   &    |- ( ph -> .~ Er V )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .+ b ) .~ ( p .+ q ) ) )   &    |- ( ph -> ( ( a .~ p /\ b .~ q ) -> ( a .x. b ) .~ ( p .x. q ) ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( U e. Ring /\ [ .1. ] .~ = ( 1r ` U ) ) )
7.3.6  Opposite ring
Syntax	coppr 14211	The opposite ring operation.
class oppr
Definition	df-oppr 14212	Define an opposite ring, which is the same as the original ring but with multiplication written the other way around. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- oppr = ( f e. _V |-> ( f sSet <. ( .r ` ndx ) , tpos ( .r ` f ) >. ) )
Theorem	opprvalg 14213	Value of the opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   =>    |- ( R e. V -> O = ( R sSet <. ( .r ` ndx ) , tpos .x. >. ) )
Theorem	opprmulfvalg 14214	Value of the multiplication operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( R e. V -> .xb = tpos .x. )
Theorem	opprmulg 14215	Value of the multiplication operation of an opposite ring. Hypotheses eliminated by a suggestion of Stefan O'Rear, 30-Aug-2015. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( ( R e. V /\ X e. W /\ Y e. U ) -> ( X .xb Y ) = ( Y .x. X ) )
Theorem	crngoppr 14216	In a commutative ring, the opposite ring is equivalent to the original ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- O = (oppr ` R )   &    |- .xb = ( .r ` O )   =>    |- ( ( R e. CRing /\ X e. B /\ Y e. B ) -> ( X .x. Y ) = ( X .xb Y ) )
Theorem	opprex 14217	Existence of the opposite ring. If you know that R is a ring, see opprring 14223. (Contributed by Jim Kingdon, 10-Jan-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> O e. _V )
Theorem	opprsllem 14218	Lemma for opprbasg 14219 and oppraddg 14220. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- ( E ` ndx ) =/= ( .r ` ndx )   =>    |- ( R e. V -> ( E ` R ) = ( E ` O ) )
Theorem	opprbasg 14219	Base set of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. V -> B = ( Base ` O ) )
Theorem	oppraddg 14220	Addition operation of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Proof shortened by AV, 6-Nov-2024.)
|- O = (oppr ` R )   &    |- .+ = ( +g ` R )   =>    |- ( R e. V -> .+ = ( +g ` O ) )
Theorem	opprrng 14221	An opposite non-unital ring is a non-unital ring. (Contributed by AV, 15-Feb-2025.)
|- O = (oppr ` R )   =>    |- ( R e. Rng -> O e. Rng )
Theorem	opprrngbg 14222	A set is a non-unital ring if and only if its opposite is a non-unital ring. Bidirectional form of opprrng 14221. (Contributed by AV, 15-Feb-2025.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Rng <-> O e. Rng ) )
Theorem	opprring 14223	An opposite ring is a ring. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Aug-2015.)
|- O = (oppr ` R )   =>    |- ( R e. Ring -> O e. Ring )
Theorem	opprringbg 14224	Bidirectional form of opprring 14223. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. V -> ( R e. Ring <-> O e. Ring ) )
Theorem	oppr0g 14225	Additive identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. V -> .0. = ( 0g ` O ) )
Theorem	oppr1g 14226	Multiplicative identity of an opposite ring. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- O = (oppr ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. V -> .1. = ( 1r ` O ) )
Theorem	opprnegg 14227	The negative function in an opposite ring. (Contributed by Mario Carneiro, 5-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- O = (oppr ` R )   &    |- N = ( invg ` R )   =>    |- ( R e. V -> N = ( invg ` O ) )
Theorem	opprsubgg 14228	Being a subgroup is a symmetric property. (Contributed by Mario Carneiro, 6-Dec-2014.)
|- O = (oppr ` R )   =>    |- ( R e. V -> (SubGrp ` R ) = (SubGrp ` O ) )
Theorem	mulgass3 14229	An associative property between group multiple and ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- B = ( Base ` R )   &    |- .x. = (.g ` R )   &    |- .X. = ( .r ` R )   =>    |- ( ( R e. Ring /\ ( N e. ZZ /\ X e. B /\ Y e. B ) ) -> ( X .X. ( N .x. Y ) ) = ( N .x. ( X .X. Y ) ) )
7.3.7  Divisibility
Syntax	cdsr 14230	Ring divisibility relation.
class ||r
Syntax	cui 14231	Units in a ring.
class Unit
Syntax	cir 14232	Ring irreducibles.
class Irred
Definition	df-dvdsr 14233*	Define the (right) divisibility relation in a ring. Access to the left divisibility relation is available through ( ||r ` (oppr ` R ) ). (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ||r = ( w e. _V |-> { <. x , y >. | ( x e. ( Base ` w ) /\ E. z e. ( Base ` w ) ( z ( .r ` w ) x ) = y ) } )
Definition	df-unit 14234	Define the set of units in a ring, that is, all elements with a left and right multiplicative inverse. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- Unit = ( w e. _V |-> ( `' ( ( ||r ` w ) i^i ( ||r ` (oppr ` w ) ) ) " { ( 1r ` w ) } ) )
Definition	df-irred 14235*	Define the set of irreducible elements in a ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- Irred = ( w e. _V |-> [_ ( ( Base ` w ) \ (Unit ` w ) ) / b ]_ { z e. b | A. x e. b A. y e. b ( x ( .r ` w ) y ) =/= z } )
Theorem	reldvdsr 14236	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- .|| = ( ||r ` R )   =>    |- Rel .||
Theorem	reldvdsrsrg 14237	The divides relation is a relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Jim Kingdon, 24-Jan-2025.)
|- ( R e. SRing -> Rel ( ||r ` R ) )
Theorem	dvdsrvald 14238*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 6-Jan-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   =>    |- ( ph -> .|| = { <. x , y >. | ( x e. B /\ E. z e. B ( z .x. x ) = y ) } )
Theorem	dvdsrd 14239*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   =>    |- ( ph -> ( X .|| Y <-> ( X e. B /\ E. z e. B ( z .x. X ) = Y ) ) )
Theorem	dvdsr2d 14240*	Value of the divides relation. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> X e. B )   =>    |- ( ph -> ( X .|| Y <-> E. z e. B ( z .x. X ) = Y ) )
Theorem	dvdsrmuld 14241	A left-multiple of X is divisible by X. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> .x. = ( .r ` R ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> X .|| ( Y .x. X ) )
Theorem	dvdsrcld 14242	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> X .|| Y )   =>    |- ( ph -> X e. B )
Theorem	dvdsrex 14243	Existence of the divisibility relation. (Contributed by Jim Kingdon, 28-Jan-2025.)
|- ( R e. SRing -> ( ||r ` R ) e. _V )
Theorem	dvdsrcl2 14244	Closure of a dividing element. (Contributed by Mario Carneiro, 5-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X .|| Y ) -> Y e. B )
Theorem	dvdsrid 14245	An element in a (unital) ring divides itself. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 30-Apr-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| X )
Theorem	dvdsrtr 14246	Divisibility is transitive. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ Y .|| Z /\ Z .|| X ) -> Y .|| X )
Theorem	dvdsrmul1 14247	The divisibility relation is preserved under right-multiplication. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ Z e. B /\ X .|| Y ) -> ( X .x. Z ) .|| ( Y .x. Z ) )
Theorem	dvdsrneg 14248	An element divides its negative. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- N = ( invg ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| ( N ` X ) )
Theorem	dvdsr01 14249	In a ring, zero is divisible by all elements. ("Zero divisor" as a term has a somewhat different meaning.) (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> X .|| .0. )
Theorem	dvdsr02 14250	Only zero is divisible by zero. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- B = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. B ) -> ( .0. .|| X <-> X = .0. ) )
Theorem	isunitd 14251	Property of being a unit of a ring. A unit is an element that left- and right-divides one. (Contributed by Mario Carneiro, 1-Dec-2014.) (Revised by Mario Carneiro, 8-Dec-2015.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> .1. = ( 1r ` R ) )   &    |- ( ph -> .|| = ( ||r ` R ) )   &    |- ( ph -> S = (oppr ` R ) )   &    |- ( ph -> E = ( ||r ` S ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> ( X e. U <-> ( X .|| .1. /\ X E .1. ) ) )
Theorem	1unit 14252	The multiplicative identity is a unit. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- U = (Unit ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> .1. e. U )
Theorem	unitcld 14253	A unit is an element of the base set. (Contributed by Mario Carneiro, 1-Dec-2014.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> R e. SRing )   &    |- ( ph -> X e. U )   =>    |- ( ph -> X e. B )
Theorem	unitssd 14254	The set of units is contained in the base set. (Contributed by Mario Carneiro, 5-Oct-2015.)
|- ( ph -> B = ( Base ` R ) )   &    |- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> R e. SRing )   =>    |- ( ph -> U C_ B )
Theorem	opprunitd 14255	Being a unit is a symmetric property, so it transfers to the opposite ring. (Contributed by Mario Carneiro, 4-Dec-2014.)
|- ( ph -> U = (Unit ` R ) )   &    |- ( ph -> S = (oppr ` R ) )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> U = (Unit ` S ) )
Theorem	crngunit 14256	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 14257	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 14258	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 14259	Reversal of unitmulcl 14258 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 14260	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 14261	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 14262	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 14263	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 14264	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 14265	Extend class notation with multiplicative inverse.
class invr
Definition	df-invr 14266	Define multiplicative inverse. (Contributed by NM, 21-Sep-2011.)
|- invr = ( r e. _V |-> ( invg ` ( (mulGrp ` r ) ↾s (Unit ` r ) ) ) )
Theorem	invrfvald 14267	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 14268	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 14269	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 14270	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 14271	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 14272	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 14273	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 14274	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 14275	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 14276	Extend class notation with ring division.
class /r
Definition	df-dvr 14277*	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 14278*	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 14279	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 14280	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 14281	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 14282	A ring element divided by itself is the ring unity. (dividap 8975 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 14283	A ring element divided by the ring unity is itself. (div1 8977 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 14284	An associative law for division. (divassap 8964 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 14285	A cancellation law for division. (divcanap1 8955 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 14286	A cancellation law for division. (divcanap3 8972 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 14287	Equality in terms of ratio equal to ring unity. (diveqap1 8979 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 14288	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 14289	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 14290	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 14291*	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 14292*	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 14293*	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 14294*	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 14295	Extend class notation with the ring homomorphisms.
class RingHom
Syntax	crs 14296	Extend class notation with the ring isomorphisms.
class RingIso
Definition	df-rhm 14297*	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 14298*	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 14299*	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 14300	Reverse closure of a ring homomorphism. (Contributed by Stefan O'Rear, 7-Mar-2015.)
|- ( F e. ( R RingHom S ) -> R e. Ring )