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	lsslsp 14401	Spans in submodules correspond to spans in the containing module. (Contributed by Stefan O'Rear, 12-Dec-2014.) Terms in the equation were swapped as proposed by NM on 15-Mar-2015. (Revised by AV, 18-Apr-2025.)
|- X = ( W ↾s U )   &    |- M = ( LSpan ` W )   &    |- N = ( LSpan ` X )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. L /\ G C_ U ) -> ( N ` G ) = ( M ` G ) )
Theorem	lss0v 14402	The zero vector in a submodule equals the zero vector in the including module. (Contributed by NM, 15-Mar-2015.)
|- X = ( W ↾s U )   &    |- .0. = ( 0g ` W )   &    |- Z = ( 0g ` X )   &    |- L = ( LSubSp ` W )   =>    |- ( ( W e. LMod /\ U e. L ) -> Z = .0. )
Theorem	lsspropdg 14403*	If two structures have the same components (properties), they have the same subspace structure. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised 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. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ph -> P = ( Base ` (Scalar ` K ) ) )   &    |- ( ph -> P = ( Base ` (Scalar ` L ) ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( LSubSp ` K ) = ( LSubSp ` L ) )
Theorem	lsppropd 14404*	If two structures have the same components (properties), they have the same span function. (Contributed by Mario Carneiro, 9-Feb-2015.) (Revised by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 24-Apr-2024.)
|- ( 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. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) e. W )   &    |- ( ( ph /\ ( x e. P /\ y e. B ) ) -> ( x ( .s ` K ) y ) = ( x ( .s ` L ) y ) )   &    |- ( ph -> P = ( Base ` (Scalar ` K ) ) )   &    |- ( ph -> P = ( Base ` (Scalar ` L ) ) )   &    |- ( ph -> K e. X )   &    |- ( ph -> L e. Y )   =>    |- ( ph -> ( LSpan ` K ) = ( LSpan ` L ) )
7.6  Subring algebras and ideals
7.6.1  Subring algebras
Syntax	csra 14405	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 14406	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 14407*	Any ring can be regarded as a left algebra over any of its subrings. The function subringAlg associates with any ring and any of its subrings the left algebra consisting in the ring itself regarded as a left algebra over the subring. It has an inner product which is simply the ring product. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- subringAlg = ( w e. _V |-> ( s e. ~P ( Base ` w ) |-> ( ( ( w sSet <. (Scalar ` ndx ) , ( w ↾s s ) >. ) sSet <. ( .s ` ndx ) , ( .r ` w ) >. ) sSet <. ( .i ` ndx ) , ( .r ` w ) >. ) ) )
Definition	df-rgmod 14408	Any ring can be regarded as a left algebra over itself. The function ringLMod associates with any ring the left algebra consisting in the ring itself regarded as a left algebra over itself. It has an inner product which is simply the ring product. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod = ( w e. _V |-> ( (subringAlg ` w ) ` ( Base ` w ) ) )
Theorem	sraval 14409	Lemma for srabaseg 14411 through sravscag 14415. (Contributed by Mario Carneiro, 27-Nov-2014.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( (subringAlg ` W ) ` S ) = ( ( ( W sSet <. (Scalar ` ndx ) , ( W ↾s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) sSet <. ( .i ` ndx ) , ( .r ` W ) >. ) )
Theorem	sralemg 14410	Lemma for srabaseg 14411 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   &    |- ( E = Slot ( E ` ndx ) /\ ( E ` ndx ) e. NN )   &    |- (Scalar ` ndx ) =/= ( E ` ndx )   &    |- ( .s ` ndx ) =/= ( E ` ndx )   &    |- ( .i ` ndx ) =/= ( E ` ndx )   =>    |- ( ph -> ( E ` W ) = ( E ` A ) )
Theorem	srabaseg 14411	Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( Base ` W ) = ( Base ` A ) )
Theorem	sraaddgg 14412	Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( +g ` W ) = ( +g ` A ) )
Theorem	sramulrg 14413	Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .r ` A ) )
Theorem	srascag 14414	The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( W ↾s S ) = (Scalar ` A ) )
Theorem	sravscag 14415	The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 12-Nov-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .s ` A ) )
Theorem	sraipg 14416	The inner product operation of a subring algebra. (Contributed by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( .r ` W ) = ( .i ` A ) )
Theorem	sratsetg 14417	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> (TopSet ` W ) = (TopSet ` A ) )
Theorem	sraex 14418	Existence of a subring algebra. (Contributed by Jim Kingdon, 16-Apr-2025.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> A e. _V )
Theorem	sratopng 14419	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( TopOpen ` W ) = ( TopOpen ` A ) )
Theorem	sradsg 14420	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.) (Revised by Thierry Arnoux, 16-Jun-2019.) (Revised by AV, 29-Oct-2024.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> ( dist ` W ) = ( dist ` A ) )
Theorem	sraring 14421	Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.)
|- A = ( (subringAlg ` R ) ` V )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ V C_ B ) -> A e. Ring )
Theorem	sralmod 14422	The subring algebra is a left module. (Contributed by Stefan O'Rear, 27-Nov-2014.)
|- A = ( (subringAlg ` W ) ` S )   =>    |- ( S e. (SubRing ` W ) -> A e. LMod )
Theorem	sralmod0g 14423	The subring module inherits a zero from its ring. (Contributed by Stefan O'Rear, 27-Dec-2014.)
|- ( ph -> A = ( (subringAlg ` W ) ` S ) )   &    |- ( ph -> .0. = ( 0g ` W ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- ( ph -> W e. X )   =>    |- ( ph -> .0. = ( 0g ` A ) )
Theorem	issubrgd 14424*	Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014.)
|- ( ph -> S = ( I ↾s D ) )   &    |- ( ph -> .0. = ( 0g ` I ) )   &    |- ( ph -> .+ = ( +g ` I ) )   &    |- ( ph -> D C_ ( Base ` I ) )   &    |- ( ph -> .0. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .+ y ) e. D )   &    |- ( ( ph /\ x e. D ) -> ( ( invg ` I ) ` x ) e. D )   &    |- ( ph -> .1. = ( 1r ` I ) )   &    |- ( ph -> .x. = ( .r ` I ) )   &    |- ( ph -> .1. e. D )   &    |- ( ( ph /\ x e. D /\ y e. D ) -> ( x .x. y ) e. D )   &    |- ( ph -> I e. Ring )   =>    |- ( ph -> D e. (SubRing ` I ) )
Theorem	rlmfn 14425	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14426	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )
Theorem	rlmbasg 14427	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( Base ` R ) = ( Base ` (ringLMod ` R ) ) )
Theorem	rlmplusgg 14428	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( +g ` R ) = ( +g ` (ringLMod ` R ) ) )
Theorem	rlm0g 14429	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 14430	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( R e. V -> ( -g ` R ) = ( -g ` (ringLMod ` R ) ) )
Theorem	rlmmulrg 14431	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( .r ` R ) = ( .r ` (ringLMod ` R ) ) )
Theorem	rlmscabas 14432	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 14433	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( .r ` R ) = ( .s ` (ringLMod ` R ) ) )
Theorem	rlmtopng 14434	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) ) )
Theorem	rlmdsg 14435	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( dist ` R ) = ( dist ` (ringLMod ` R ) ) )
Theorem	rlmlmod 14436	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmvnegg 14437	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 14438*	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 14439	Ring left-ideal function.
class LIdeal
Syntax	crsp 14440	Ring span function.
class RSpan
Definition	df-lidl 14441	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 14442	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- RSpan = ( LSpan o. ringLMod )
Theorem	lidlvalg 14443	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 14444	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( W e. V -> (RSpan ` W ) = ( LSpan ` (ringLMod ` W ) ) )
Theorem	lidlex 14445	Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> (LIdeal ` W ) e. _V )
Theorem	rspex 14446	Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( W e. V -> (RSpan ` W ) e. _V )
Theorem	lidlmex 14447	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 14448	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 14449	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 14450	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 14451*	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 14452	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 14453*	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 14454*	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 14455	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 14456	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 14457	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 14458	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 14459	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 14460*	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 14461	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 14462	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 14463	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 14464	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 14465	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 14466	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 14467*	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 14468	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 14469	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 14470	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 14471	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 14472	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 14473	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 14474	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 14475	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 14476*	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 14477	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 14478	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 14479	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 14480*	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 14481*	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 14482	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 14483	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 14484	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 14485	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 14486	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 14487	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 14488	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 14489	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 14490	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 14491	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 14492	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 14493	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 14494	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 14495	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 14496	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 14497	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 14499 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 14498	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 14499	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 14500*	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 ) )