P. 147 of Theorem List - Intuitionistic Logic Explorer

Theorem List for Intuitionistic Logic Explorer - 14601-14700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rlmfn 14601	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14602	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )
Theorem	rlmbasg 14603	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( Base ` R ) = ( Base ` (ringLMod ` R ) ) )
Theorem	rlmplusgg 14604	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( +g ` R ) = ( +g ` (ringLMod ` R ) ) )
Theorem	rlm0g 14605	Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- ( R e. V -> ( 0g ` R ) = ( 0g ` (ringLMod ` R ) ) )
Theorem	rlmsubg 14606	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( R e. V -> ( -g ` R ) = ( -g ` (ringLMod ` R ) ) )
Theorem	rlmmulrg 14607	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( .r ` R ) = ( .r ` (ringLMod ` R ) ) )
Theorem	rlmscabas 14608	Scalars in the ring module have the same base set. (Contributed by Jim Kingdon, 29-Apr-2025.)
|- ( R e. X -> ( Base ` R ) = ( Base ` (Scalar ` (ringLMod ` R ) ) ) )
Theorem	rlmvscag 14609	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( .r ` R ) = ( .s ` (ringLMod ` R ) ) )
Theorem	rlmtopng 14610	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) ) )
Theorem	rlmdsg 14611	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( dist ` R ) = ( dist ` (ringLMod ` R ) ) )
Theorem	rlmlmod 14612	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmvnegg 14613	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- ( R e. V -> ( invg ` R ) = ( invg ` (ringLMod ` R ) ) )
Theorem	ixpsnbasval 14614*	The value of an infinite Cartesian product of the base of a left module over a ring with a singleton. (Contributed by AV, 3-Dec-2018.)
|- ( ( R e. V /\ X e. W ) -> X_ x e. { X } ( Base ` ( ( { X } X. { (ringLMod ` R ) } ) ` x ) ) = { f | ( f Fn { X } /\ ( f ` X ) e. ( Base ` R ) ) } )
7.6.2  Ideals and spans
Syntax	clidl 14615	Ring left-ideal function.
class LIdeal
Syntax	crsp 14616	Ring span function.
class RSpan
Definition	df-lidl 14617	Define the class of left ideals of a given ring. An ideal is a submodule of the ring viewed as a module over itself. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- LIdeal = ( LSubSp o. ringLMod )
Definition	df-rsp 14618	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- RSpan = ( LSpan o. ringLMod )
Theorem	lidlvalg 14619	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (LIdeal ` W ) = ( LSubSp ` (ringLMod ` W ) ) )
Theorem	rspvalg 14620	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( W e. V -> (RSpan ` W ) = ( LSpan ` (ringLMod ` W ) ) )
Theorem	lidlex 14621	Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> (LIdeal ` W ) e. _V )
Theorem	rspex 14622	Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( W e. V -> (RSpan ` W ) e. _V )
Theorem	lidlmex 14623	Existence of the set a left ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
|- I = (LIdeal ` W )   =>    |- ( U e. I -> W e. _V )
Theorem	lidlss 14624	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- B = ( Base ` W )   &    |- I = (LIdeal ` W )   =>    |- ( U e. I -> U C_ B )
Theorem	lidlssbas 14625	The base set of the restriction of the ring to a (left) ideal is a subset of the base set of the ring. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
Theorem	lidlbas 14626	A (left) ideal of a ring is the base set of the restriction of the ring to this ideal. (Contributed by AV, 17-Feb-2020.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( U e. L -> ( Base ` I ) = U )
Theorem	islidlm 14627*	Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( I e. U <-> ( I C_ B /\ E. j j e. I /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) .+ b ) e. I ) )
Theorem	rnglidlmcl 14628	A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven. (Contributed by AV, 18-Feb-2025.)
|- .0. = ( 0g ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- U = (LIdeal ` R )   =>    |- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )
Theorem	dflidl2rng 14629*	Alternate (the usual textbook) definition of a (left) ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ I e. (SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( x .x. y ) e. I ) )
Theorem	isridlrng 14630*	A right ideal is a left ideal of the opposite non-unital ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ I e. (SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( y .x. x ) e. I ) )
Theorem	lidl0cl 14631	An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> .0. e. I )
Theorem	lidlacl 14632	An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- .+ = ( +g ` R )   =>    |- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .+ Y ) e. I )
Theorem	lidlnegcl 14633	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- N = ( invg ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( N ` X ) e. I )
Theorem	lidlsubg 14634	An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> I e. (SubGrp ` R ) )
Theorem	lidlsubcl 14635	An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- U = (LIdeal ` R )   &    |- .- = ( -g ` R )   =>    |- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .- Y ) e. I )
Theorem	dflidl2 14636*	Alternate (the usual textbook) definition of a (left) ideal of a ring to be a subgroup of the additive group of the ring which is closed under left-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( I e. U <-> ( I e. (SubGrp ` R ) /\ A. x e. B A. y e. I ( x .x. y ) e. I ) ) )
Theorem	lidl0 14637	Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. U )
Theorem	lidl1 14638	Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. U )
Theorem	rspcl 14639	The span of a set of ring elements is an ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- K = (RSpan ` R )   &    |- B = ( Base ` R )   &    |- U = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ G C_ B ) -> ( K ` G ) e. U )
Theorem	rspssid 14640	The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ G C_ B ) -> G C_ ( K ` G ) )
Theorem	rsp0 14641	The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> ( K ` { .0. } ) = { .0. } )
Theorem	rspssp 14642	The ideal span of a set of elements in a ring is contained in any subring which contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- U = (LIdeal ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ G C_ I ) -> ( K ` G ) C_ I )
Theorem	lidlrsppropdg 14643*	The left ideals and ring span of a ring depend only on the ring components. Here W is expected to be either B (when closure is available) or _V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.)
|- ( ph -> B = ( Base ` K ) )   &    |- ( ph -> B = ( Base ` L ) )   &    |- ( ph -> B C_ W )   &    |- ( ( ph /\ ( x e. W /\ y e. W ) ) -> ( x ( +g ` K ) y ) = ( x ( +g ` L ) y ) )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. B /\ y e. B ) ) -> ( x ( .r ` K ) y ) = ( x ( .r ` L ) y ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( (LIdeal ` K ) = (LIdeal ` L ) /\ (RSpan ` K ) = (RSpan ` L ) ) )
Theorem	rnglidlmmgm 14644	The multiplicative group of a (left) ideal of a non-unital ring is a magma. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption .0. e. U is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> (mulGrp ` I ) e. Mgm )
Theorem	rnglidlmsgrp 14645	The multiplicative group of a (left) ideal of a non-unital ring is a semigroup. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption .0. e. U is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Rng /\ U e. L /\ .0. e. U ) -> (mulGrp ` I ) e. Smgrp )
Theorem	rnglidlrng 14646	A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020.) Generalization for non-unital rings. The assumption U e. (SubGrp ` R ) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.)
|- L = (LIdeal ` R )   &    |- I = ( R ↾s U )   =>    |- ( ( R e. Rng /\ U e. L /\ U e. (SubGrp ` R ) ) -> I e. Rng )
7.6.3  Two-sided ideals and quotient rings
Syntax	c2idl 14647	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 14648	Define the class of two-sided ideals of a ring. A two-sided ideal is a left ideal which is also a right ideal (or a left ideal over the opposite ring). (Contributed by Mario Carneiro, 14-Jun-2015.)
|- 2Ideal = ( r e. _V |-> ( (LIdeal ` r ) i^i (LIdeal ` (oppr ` r ) ) ) )
Theorem	2idlmex 14649	Existence of the set a two-sided ideal is built from (when the ideal is inhabited). (Contributed by Jim Kingdon, 18-Apr-2025.)
|- T = (2Ideal ` W )   =>    |- ( U e. T -> W e. _V )
Theorem	2idlval 14650	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- T = ( I i^i J )
Theorem	2idlvalg 14651	Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- ( R e. V -> T = ( I i^i J ) )
Theorem	isridl 14652*	A right ideal is a left ideal of the opposite ring. This theorem shows that this definition corresponds to the usual textbook definition of a right ideal of a ring to be a subgroup of the additive group of the ring which is closed under right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( I e. U <-> ( I e. (SubGrp ` R ) /\ A. x e. B A. y e. I ( y .x. x ) e. I ) ) )
Theorem	2idlelb 14653	Membership in a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   &    |- J = (LIdeal ` O )   &    |- T = (2Ideal ` R )   =>    |- ( U e. T <-> ( U e. I /\ U e. J ) )
Theorem	2idllidld 14654	A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   =>    |- ( ph -> I e. (LIdeal ` R ) )
Theorem	2idlridld 14655	A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- O = (oppr ` R )   =>    |- ( ph -> I e. (LIdeal ` O ) )
Theorem	df2idl2rng 14656*	Alternate (the usual textbook) definition of a two-sided ideal of a non-unital ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 21-Mar-2025.)
|- U = (2Ideal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ I e. (SubGrp ` R ) ) -> ( I e. U <-> A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) )
Theorem	df2idl2 14657*	Alternate (the usual textbook) definition of a two-sided ideal of a ring to be a subgroup of the additive group of the ring which is closed under left- and right-multiplication by elements of the full ring. (Contributed by AV, 13-Feb-2025.) (Proof shortened by AV, 18-Apr-2025.)
|- U = (2Ideal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( R e. Ring -> ( I e. U <-> ( I e. (SubGrp ` R ) /\ A. x e. B A. y e. I ( ( x .x. y ) e. I /\ ( y .x. x ) e. I ) ) ) )
Theorem	ridl0 14658	Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. U )
Theorem	ridl1 14659	Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.)
|- U = (LIdeal ` (oppr ` R ) )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. U )
Theorem	2idl0 14660	Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.)
|- I = (2Ideal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. I )
Theorem	2idl1 14661	Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.)
|- I = (2Ideal ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. I )
Theorem	2idlss 14662	A two-sided ideal is a subset of the base set. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.)
|- B = ( Base ` W )   &    |- I = (2Ideal ` W )   =>    |- ( U e. I -> U C_ B )
Theorem	2idlbas 14663	The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- J = ( R ↾s I )   &    |- B = ( Base ` J )   =>    |- ( ph -> B = I )
Theorem	2idlelbas 14664	The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> I e. (2Ideal ` R ) )   &    |- J = ( R ↾s I )   &    |- B = ( Base ` J )   =>    |- ( ph -> ( B e. (LIdeal ` R ) /\ B e. (LIdeal ` (oppr ` R ) ) ) )
Theorem	rng2idlsubrng 14665	A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> I e. (SubRng ` R ) )
Theorem	rng2idlnsg 14666	A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> I e. (NrmSGrp ` R ) )
Theorem	rng2idl0 14667	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> ( R ↾s I ) e. Rng )   =>    |- ( ph -> ( 0g ` R ) e. I )
Theorem	rng2idlsubgsubrng 14668	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> I e. (SubRng ` R ) )
Theorem	rng2idlsubgnsg 14669	A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> I e. (NrmSGrp ` R ) )
Theorem	rng2idlsubg0 14670	The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.)
|- ( ph -> R e. Rng )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> I e. (SubGrp ` R ) )   =>    |- ( ph -> ( 0g ` R ) e. I )
Theorem	2idlcpblrng 14671	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	2idlcpbl 14672	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.)
|- X = ( Base ` R )   &    |- E = ( R ~QG S )   &    |- I = (2Ideal ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( ( A E C /\ B E D ) -> ( A .x. B ) E ( C .x. D ) ) )
Theorem	qus2idrng 14673	The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 14675 analog). (Contributed by AV, 23-Feb-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Rng /\ S e. I /\ S e. (SubGrp ` R ) ) -> U e. Rng )
Theorem	qus1 14674	The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> ( U e. Ring /\ [ .1. ] ( R ~QG S ) = ( 1r ` U ) ) )
Theorem	qusring 14675	If S is a two-sided ideal in R, then U = R / S is a ring, called the quotient ring of R by S. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   =>    |- ( ( R e. Ring /\ S e. I ) -> U e. Ring )
Theorem	qusrhm 14676*	If S is a two-sided ideal in R, then the "natural map" from elements to their cosets is a ring homomorphism from R to R / S. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (2Ideal ` R )   &    |- X = ( Base ` R )   &    |- F = ( x e. X |-> [ x ] ( R ~QG S ) )   =>    |- ( ( R e. Ring /\ S e. I ) -> F e. ( R RingHom U ) )
Theorem	qusmul2 14677	Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.)
|- Q = ( R /.s ( R ~QG I ) )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .X. = ( .r ` Q )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> I e. (2Ideal ` R ) )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( [ X ] ( R ~QG I ) .X. [ Y ] ( R ~QG I ) ) = [ ( X .x. Y ) ] ( R ~QG I ) )
Theorem	crngridl 14678	In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   &    |- O = (oppr ` R )   =>    |- ( R e. CRing -> I = (LIdeal ` O ) )
Theorem	crng2idl 14679	In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- I = (LIdeal ` R )   =>    |- ( R e. CRing -> I = (2Ideal ` R ) )
Theorem	qusmulrng 14680	Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 14681. Similar to qusmul2 14677. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.)
|- .~ = ( R ~QG S )   &    |- H = ( R /.s .~ )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .xb = ( .r ` H )   =>    |- ( ( ( R e. Rng /\ S e. (2Ideal ` R ) /\ S e. (SubGrp ` R ) ) /\ ( X e. B /\ Y e. B ) ) -> ( [ X ] .~ .xb [ Y ] .~ ) = [ ( X .x. Y ) ] .~ )
Theorem	quscrng 14681	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (LIdeal ` R )   =>    |- ( ( R e. CRing /\ S e. I ) -> U e. CRing )
7.6.4  Principal ideal rings. Divisibility in the integers
Theorem	rspsn 14682*	Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- K = (RSpan ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ G e. B ) -> ( K ` { G } ) = { x | G .|| x } )
7.7  The complex numbers as an algebraic extensible structure
7.7.1  Definition and basic properties
Syntax	cpsmet 14683	Extend class notation with the class of all pseudometric spaces.
class PsMet
Syntax	cxmet 14684	Extend class notation with the class of all extended metric spaces.
class *Met
Syntax	cmet 14685	Extend class notation with the class of all metrics.
class Met
Syntax	cbl 14686	Extend class notation with the metric space ball function.
class ball
Syntax	cfbas 14687	Extend class definition to include the class of filter bases.
class fBas
Syntax	cfg 14688	Extend class definition to include the filter generating function.
class filGen
Syntax	cmopn 14689	Extend class notation with a function mapping each metric space to the family of its open sets.
class MetOpen
Syntax	cmetu 14690	Extend class notation with the function mapping metrics to the uniform structure generated by that metric.
class metUnif
Definition	df-psmet 14691*	Define the set of all pseudometrics on a given base set. In a pseudo metric, two distinct points may have a distance zero. (Contributed by Thierry Arnoux, 7-Feb-2018.)
|- PsMet = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x ( ( y d y ) = 0 /\ A. z e. x A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-xmet 14692*	Define the set of all extended metrics on a given base set. The definition is similar to df-met 14693, but we also allow the metric to take on the value +oo. (Contributed by Mario Carneiro, 20-Aug-2015.)
|- *Met = ( x e. _V |-> { d e. ( RR* ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) +e ( w d z ) ) ) } )
Definition	df-met 14693*	Define the (proper) class of all metrics. (A metric space is the metric's base set paired with the metric. However, we will often also call the metric itself a "metric space".) Equivalent to Definition 14-1.1 of [Gleason] p. 223. (Contributed by NM, 25-Aug-2006.)
|- Met = ( x e. _V |-> { d e. ( RR ^m ( x X. x ) ) | A. y e. x A. z e. x ( ( ( y d z ) = 0 <-> y = z ) /\ A. w e. x ( y d z ) <_ ( ( w d y ) + ( w d z ) ) ) } )
Definition	df-bl 14694*	Define the metric space ball function. (Contributed by NM, 30-Aug-2006.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- ball = ( d e. _V |-> ( x e. dom dom d , z e. RR* |-> { y e. dom dom d | ( x d y ) < z } ) )
Definition	df-mopn 14695	Define a function whose value is the family of open sets of a metric space. (Contributed by NM, 1-Sep-2006.)
|- MetOpen = ( d e. U. ran *Met |-> ( topGen ` ran ( ball ` d ) ) )
Definition	df-fbas 14696*	Define the class of all filter bases. Note that a filter base on one set is also a filter base for any superset, so there is not a unique base set that can be recovered. (Contributed by Jeff Hankins, 1-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- fBas = ( w e. _V |-> { x e. ~P ~P w | ( x =/= (/) /\ (/) e/ x /\ A. y e. x A. z e. x ( x i^i ~P ( y i^i z ) ) =/= (/) ) } )
Definition	df-fg 14697*	Define the filter generating function. (Contributed by Jeff Hankins, 3-Sep-2009.) (Revised by Stefan O'Rear, 11-Jul-2015.)
|- filGen = ( w e. _V , x e. ( fBas ` w ) |-> { y e. ~P w | ( x i^i ~P y ) =/= (/) } )
Definition	df-metu 14698*	Define the function mapping metrics to the uniform structure generated by that metric. (Contributed by Thierry Arnoux, 1-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
|- metUnif = ( d e. U. ran PsMet |-> ( ( dom dom d X. dom dom d ) filGen ran ( a e. RR+ |-> ( `' d " ( 0 [,) a ) ) ) ) )
Theorem	blfn 14699	The ball function has universal domain. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ball Fn _V
Theorem	mopnset 14700	Getting a set by applying MetOpen. (Contributed by Jim Kingdon, 24-Sep-2025.)
|- ( D e. V -> ( MetOpen ` D ) e. _V )