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	lspsn 14401*	Span of the singleton of a vector. (Contributed by NM, 14-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { X } ) = { v | E. k e. K v = ( k .x. X ) } )
Theorem	ellspsn 14402*	Member of span of the singleton of a vector. (Contributed by NM, 22-Feb-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( U e. ( N ` { X } ) <-> E. k e. K U = ( k .x. X ) ) )
Theorem	lspsnvsi 14403	Span of a scalar product of a singleton. (Contributed by NM, 23-Apr-2014.) (Proof shortened by Mario Carneiro, 4-Sep-2014.)
|- F = (Scalar ` W )   &    |- K = ( Base ` F )   &    |- V = ( Base ` W )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ R e. K /\ X e. V ) -> ( N ` { ( R .x. X ) } ) C_ ( N ` { X } ) )
Theorem	lspsnss2 14404*	Comparable spans of singletons must have proportional vectors. (Contributed by NM, 7-Jun-2015.)
|- V = ( Base ` W )   &    |- S = (Scalar ` W )   &    |- K = ( Base ` S )   &    |- .x. = ( .s ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( ( N ` { X } ) C_ ( N ` { Y } ) <-> E. k e. K X = ( k .x. Y ) ) )
Theorem	lspsnneg 14405	Negation does not change the span of a singleton. (Contributed by NM, 24-Apr-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- M = ( invg ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( N ` { ( M ` X ) } ) = ( N ` { X } ) )
Theorem	lspsnsub 14406	Swapping subtraction order does not change the span of a singleton. (Contributed by NM, 4-Apr-2015.)
|- V = ( Base ` W )   &    |- .- = ( -g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   =>    |- ( ph -> ( N ` { ( X .- Y ) } ) = ( N ` { ( Y .- X ) } ) )
Theorem	lspsn0 14407	Span of the singleton of the zero vector. (Contributed by NM, 15-Jan-2014.) (Proof shortened by Mario Carneiro, 19-Jun-2014.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( N ` { .0. } ) = { .0. } )
Theorem	lsp0 14408	Span of the empty set. (Contributed by Mario Carneiro, 5-Sep-2014.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> ( N ` (/) ) = { .0. } )
Theorem	lspuni0 14409	Union of the span of the empty set. (Contributed by NM, 14-Mar-2015.)
|- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( W e. LMod -> U. ( N ` (/) ) = .0. )
Theorem	lspun0 14410	The span of a union with the zero subspace. (Contributed by NM, 22-May-2015.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X C_ V )   =>    |- ( ph -> ( N ` ( X u. { .0. } ) ) = ( N ` X ) )
Theorem	lspsneq0 14411	Span of the singleton is the zero subspace iff the vector is zero. (Contributed by NM, 27-Apr-2014.) (Revised by Mario Carneiro, 19-Jun-2014.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   =>    |- ( ( W e. LMod /\ X e. V ) -> ( ( N ` { X } ) = { .0. } <-> X = .0. ) )
Theorem	lspsneq0b 14412	Equal singleton spans imply both arguments are zero or both are nonzero. (Contributed by NM, 21-Mar-2015.)
|- V = ( Base ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) = ( N ` { Y } ) )   =>    |- ( ph -> ( X = .0. <-> Y = .0. ) )
Theorem	lmodindp1 14413	Two independent (non-colinear) vectors have nonzero sum. (Contributed by NM, 22-Apr-2015.)
|- V = ( Base ` W )   &    |- .+ = ( +g ` W )   &    |- .0. = ( 0g ` W )   &    |- N = ( LSpan ` W )   &    |- ( ph -> W e. LMod )   &    |- ( ph -> X e. V )   &    |- ( ph -> Y e. V )   &    |- ( ph -> ( N ` { X } ) =/= ( N ` { Y } ) )   =>    |- ( ph -> ( X .+ Y ) =/= .0. )
Theorem	lsslsp 14414	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 14415	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 14416*	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 14417*	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 14418	Extend class notation with the subring algebra generator.
class subringAlg
Syntax	crglmod 14419	Extend class notation with the left module induced by a ring over itself.
class ringLMod
Definition	df-sra 14420*	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 14421	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 14422	Lemma for srabaseg 14424 through sravscag 14428. (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 14423	Lemma for srabaseg 14424 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 14424	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 14425	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 14426	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 14427	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 14428	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 14429	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 14430	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 14431	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 14432	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 14433	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 14434	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 14435	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 14436	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 14437*	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 14438	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmvalg 14439	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( W e. V -> (ringLMod ` W ) = ( (subringAlg ` W ) ` ( Base ` W ) ) )
Theorem	rlmbasg 14440	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( Base ` R ) = ( Base ` (ringLMod ` R ) ) )
Theorem	rlmplusgg 14441	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( +g ` R ) = ( +g ` (ringLMod ` R ) ) )
Theorem	rlm0g 14442	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 14443	Subtraction in the ring module. (Contributed by Thierry Arnoux, 30-Jun-2019.)
|- ( R e. V -> ( -g ` R ) = ( -g ` (ringLMod ` R ) ) )
Theorem	rlmmulrg 14444	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( .r ` R ) = ( .r ` (ringLMod ` R ) ) )
Theorem	rlmscabas 14445	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 14446	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( R e. V -> ( .r ` R ) = ( .s ` (ringLMod ` R ) ) )
Theorem	rlmtopng 14447	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) ) )
Theorem	rlmdsg 14448	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( R e. V -> ( dist ` R ) = ( dist ` (ringLMod ` R ) ) )
Theorem	rlmlmod 14449	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmvnegg 14450	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 14451*	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 14452	Ring left-ideal function.
class LIdeal
Syntax	crsp 14453	Ring span function.
class RSpan
Definition	df-lidl 14454	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 14455	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- RSpan = ( LSpan o. ringLMod )
Theorem	lidlvalg 14456	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 14457	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- ( W e. V -> (RSpan ` W ) = ( LSpan ` (ringLMod ` W ) ) )
Theorem	lidlex 14458	Existence of the set of left ideals. (Contributed by Jim Kingdon, 27-Apr-2025.)
|- ( W e. V -> (LIdeal ` W ) e. _V )
Theorem	rspex 14459	Existence of the ring span. (Contributed by Jim Kingdon, 25-Apr-2025.)
|- ( W e. V -> (RSpan ` W ) e. _V )
Theorem	lidlmex 14460	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 14461	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 14462	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 14463	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 14464*	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 14465	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 14466*	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 14467*	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 14468	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 14469	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 14470	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 14471	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 14472	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 14473*	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 14474	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 14475	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 14476	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 14477	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 14478	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 14479	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 14480*	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 14481	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 14482	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 14483	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 14484	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 14485	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 14486	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 14487	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 14488	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 14489*	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 14490	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 14491	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 14492	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 14493*	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 14494*	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 14495	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 14496	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 14497	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 14498	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 14499	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 14500	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 )