P. 193 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 19201-19300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	rlmsca2 19201	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- ( _I ` R ) = (Scalar ` (ringLMod ` R ) )
Theorem	rlmvsca 19202	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( .r ` R ) = ( .s ` (ringLMod ` R ) )
Theorem	rlmtopn 19203	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) )
Theorem	rlmds 19204	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( dist ` R ) = ( dist ` (ringLMod ` R ) )
Theorem	rlmlmod 19205	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmlvec 19206	The ring module over a division ring is a vector space. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( R e. DivRing -> (ringLMod ` R ) e. LVec )
Theorem	rlmvneg 19207	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- ( invg ` R ) = ( invg ` (ringLMod ` R ) )
Theorem	rlmscaf 19208	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( +f ` (mulGrp ` R ) ) = ( .sf ` (ringLMod ` R ) )
Theorem	ixpsnbasval 19209*	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 ) ) } )
Theorem	lidlss 19210	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	islidl 19211*	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 /\ I =/= (/) /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) .+ b ) e. I ) )
Theorem	lidl0cl 19212	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 19213	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 19214	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 19215	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 19216	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	lidlmcl 19217	An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )
Theorem	lidl1el 19218	An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )
Theorem	lidl0 19219	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 19220	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	lidlacs 19221	The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- B = ( Base ` W )   &    |- I = (LIdeal ` W )   =>    |- ( W e. Ring -> I e. (ACS ` B ) )
Theorem	rspcl 19222	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 19223	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	rsp1 19224	The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- K = (RSpan ` R )   &    |- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( K ` { .1. } ) = B )
Theorem	rsp0 19225	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 19226	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	mrcrsp 19227	Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- U = (LIdeal ` R )   &    |- K = (RSpan ` R )   &    |- F = (mrCls ` U )   =>    |- ( R e. Ring -> K = F )
Theorem	lidlnz 19228*	A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ I =/= { .0. } ) -> E. x e. I x =/= .0. )
Theorem	drngnidl 19229	A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. DivRing -> U = { { .0. } , B } )
Theorem	lidlrsppropd 19230*	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 -> ( (LIdeal ` K ) = (LIdeal ` L ) /\ (RSpan ` K ) = (RSpan ` L ) ) )
10.8.2  Two-sided ideals and quotient rings
Syntax	c2idl 19231	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 19232	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	2idlval 19233	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	2idlcpbl 19234	The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.)
|- 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	qus1 19235	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 19236	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 19237*	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	crngridl 19238	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 19239	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	quscrng 19240	The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- U = ( R /.s ( R ~QG S ) )   &    |- I = (LIdeal ` R )   =>    |- ( ( R e. CRing /\ S e. I ) -> U e. CRing )
10.8.3  Principal ideal rings. Divisibility in the integers
Syntax	clpidl 19241	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 19242	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 19243*	Define the class of left principal ideals of a ring, which are ideals with a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- LPIdeal = ( w e. Ring |-> U_ g e. ( Base ` w ) { ( (RSpan ` w ) ` { g } ) } )
Definition	df-lpir 19244	Define the class of left principal ideal rings, rings where every left ideal has a single generator. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- LPIR = { w e. Ring | (LIdeal ` w ) = (LPIdeal ` w ) }
Theorem	lpival 19245*	Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- K = (RSpan ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> P = U_ g e. B { ( K ` { g } ) } )
Theorem	islpidl 19246*	Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- K = (RSpan ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> ( I e. P <-> E. g e. B I = ( K ` { g } ) ) )
Theorem	lpi0 19247	The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Ring -> { .0. } e. P )
Theorem	lpi1 19248	The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- B = ( Base ` R )   =>    |- ( R e. Ring -> B e. P )
Theorem	islpir 19249	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. LPIR <-> ( R e. Ring /\ U = P ) )
Theorem	lpiss 19250	Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. Ring -> P C_ U )
Theorem	islpir2 19251	Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- P = (LPIdeal ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. LPIR <-> ( R e. Ring /\ U C_ P ) )
Theorem	lpirring 19252	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( R e. LPIR -> R e. Ring )
Theorem	drnglpir 19253	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- ( R e. DivRing -> R e. LPIR )
Theorem	rspsn 19254*	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 } )
Theorem	lidldvgen 19255*	An element generates an ideal iff it is contained in the ideal and all elements are right-divided by it. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- B = ( Base ` R )   &    |- U = (LIdeal ` R )   &    |- K = (RSpan ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ G e. B ) -> ( I = ( K ` { G } ) <-> ( G e. I /\ A. x e. I G .|| x ) ) )
Theorem	lpigen 19256*	An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.)
|- U = (LIdeal ` R )   &    |- P = (LPIdeal ` R )   &    |- .|| = ( ||r ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> ( I e. P <-> E. x e. I A. y e. I x .|| y ) )
10.8.4  Nonzero rings and zero rings
Syntax	cnzr 19257	The class of nonzero rings.
class NzRing
Definition	df-nzr 19258	A nonzero or nontrivial ring is a ring with at least two values, or equivalently where 1 and 0 are different. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- NzRing = { r e. Ring | ( 1r ` r ) =/= ( 0g ` r ) }
Theorem	isnzr 19259	Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. NzRing <-> ( R e. Ring /\ .1. =/= .0. ) )
Theorem	nzrnz 19260	One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- .1. = ( 1r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. NzRing -> .1. =/= .0. )
Theorem	nzrring 19261	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. NzRing -> R e. Ring )
Theorem	drngnzr 19262	All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. DivRing -> R e. NzRing )
Theorem	isnzr2 19263	Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- B = ( Base ` R )   =>    |- ( R e. NzRing <-> ( R e. Ring /\ 2o ~<_ B ) )
Theorem	isnzr2hash 19264	Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 19263. (Contributed by AV, 14-Apr-2019.)
|- B = ( Base ` R )   =>    |- ( R e. NzRing <-> ( R e. Ring /\ 1 < ( # ` B ) ) )
Theorem	opprnzr 19265	The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- O = (oppr ` R )   =>    |- ( R e. NzRing -> O e. NzRing )
Theorem	ringelnzr 19266	A ring is nonzero if it has a nonzero element. (Contributed by Stefan O'Rear, 6-Feb-2015.) (Revised by Mario Carneiro, 13-Jun-2015.)
|- .0. = ( 0g ` R )   &    |- B = ( Base ` R )   =>    |- ( ( R e. Ring /\ X e. ( B \ { .0. } ) ) -> R e. NzRing )
Theorem	nzrunit 19267	A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. NzRing /\ A e. U ) -> A =/= .0. )
Theorem	subrgnzr 19268	A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.)
|- S = ( R ↾s A )   =>    |- ( ( R e. NzRing /\ A e. (SubRing ` R ) ) -> S e. NzRing )
Theorem	0ringnnzr 19269	A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019.)
|- ( R e. Ring -> ( ( # ` ( Base ` R ) ) = 1 <-> -. R e. NzRing ) )
Theorem	0ring 19270	If a ring has only one element, it is the zero ring. According to Wikipedia ("Zero ring", 14-Apr-2019, https://en.wikipedia.org/wiki/Zero_ring): "The zero ring, denoted {0} or simply 0, consists of the one-element set {0} with the operations + and * defined so that 0 + 0 = 0 and 0 * 0 = 0.". (Contributed by AV, 14-Apr-2019.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> B = { .0. } )
Theorem	0ring01eq 19271	In a ring with only one element, i.e. a zero ring, the zero and the identity element are the same. (Contributed by AV, 14-Apr-2019.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ ( # ` B ) = 1 ) -> .0. = .1. )
Theorem	01eq0ring 19272	If the zero and the identity element of a ring are the same, the ring is the zero ring. (Contributed by AV, 16-Apr-2019.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ .0. = .1. ) -> B = { .0. } )
Theorem	0ring01eqbi 19273	In a unital ring the zero equals the unity iff the ring is the zero ring. (Contributed by FL, 14-Feb-2010.) (Revised by AV, 23-Jan-2020.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( R e. Ring -> ( B ~~ 1o <-> .1. = .0. ) )
Theorem	rng1nnzr 19274	The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   =>    |- ( Z e. V -> M e/ NzRing )
Theorem	ring1zr 19275	The only (unital) ring with a base set consisting of one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 13-Feb-2010.) (Revised by AV, 25-Jan-2020.) (Proof shortened by AV, 7-Feb-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B = { Z } <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	rngen1zr 19276	The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 14-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   =>    |- ( ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) /\ Z e. B ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	ringen1zr 19277	The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption R e. Ring could be weakened if a definition of a non-unital ring ("Rng") was available (it would be sufficient that the multiplication is closed). (Contributed by FL, 15-Feb-2010.) (Revised by AV, 25-Jan-2020.)
|- B = ( Base ` R )   &    |- .+ = ( +g ` R )   &    |- .* = ( .r ` R )   &    |- Z = ( 0g ` R )   =>    |- ( ( R e. Ring /\ .+ Fn ( B X. B ) /\ .* Fn ( B X. B ) ) -> ( B ~~ 1o <-> ( .+ = { <. <. Z , Z >. , Z >. } /\ .* = { <. <. Z , Z >. , Z >. } ) ) )
Theorem	rng1nfld 19278	The zero ring is not a field. (Contributed by AV, 29-Apr-2019.)
|- M = { <. ( Base ` ndx ) , { Z } >. , <. ( +g ` ndx ) , { <. <. Z , Z >. , Z >. } >. , <. ( .r ` ndx ) , { <. <. Z , Z >. , Z >. } >. }   =>    |- ( Z e. V -> M e/ Field )
10.8.5  Left regular elements. More kinds of rings
Syntax	crlreg 19279	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 19280	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 19281	Class of integral domains.
class IDomn
Syntax	cpid 19282	Class of principal ideal domains.
class PID
Definition	df-rlreg 19283*	Define the set of left-regular elements in a ring as those elements which are not left zero divisors, meaning that multiplying a nonzero element on the left by a left-regular element gives a nonzero product. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- RLReg = ( r e. _V |-> { x e. ( Base ` r ) | A. y e. ( Base ` r ) ( ( x ( .r ` r ) y ) = ( 0g ` r ) -> y = ( 0g ` r ) ) } )
Definition	df-domn 19284*	A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- Domn = { r e. NzRing | [. ( Base ` r ) / b ]. [. ( 0g ` r ) / z ]. A. x e. b A. y e. b ( ( x ( .r ` r ) y ) = z -> ( x = z \/ y = z ) ) }
Definition	df-idom 19285	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- IDomn = ( CRing i^i Domn )
Definition	df-pid 19286	A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.)
|- PID = (IDomn i^i LPIR )
Theorem	rrgval 19287*	Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- E = { x e. B | A. y e. B ( ( x .x. y ) = .0. -> y = .0. ) }
Theorem	isrrg 19288*	Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( X e. E <-> ( X e. B /\ A. y e. B ( ( X .x. y ) = .0. -> y = .0. ) ) )
Theorem	rrgeq0i 19289	Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. -> Y = .0. ) )
Theorem	rrgeq0 19290	Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Ring /\ X e. E /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> Y = .0. ) )
Theorem	rrgsupp 19291	Left multiplication by a left regular element does not change the support set of a vector. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Revised by AV, 20-Jul-2019.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> I e. V )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> X e. E )   &    |- ( ph -> Y : I --> B )   =>    |- ( ph -> ( ( ( I X. { X } ) oF .x. Y ) supp .0. ) = ( Y supp .0. ) )
Theorem	rrgss 19292	Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- B = ( Base ` R )   =>    |- E C_ B
Theorem	unitrrg 19293	Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.)
|- E = (RLReg ` R )   &    |- U = (Unit ` R )   =>    |- ( R e. Ring -> U C_ E )
Theorem	isdomn 19294*	Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Domn <-> ( R e. NzRing /\ A. x e. B A. y e. B ( ( x .x. y ) = .0. -> ( x = .0. \/ y = .0. ) ) ) )
Theorem	domnnzr 19295	A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. NzRing )
Theorem	domnring 19296	A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- ( R e. Domn -> R e. Ring )
Theorem	domneq0 19297	In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ X e. B /\ Y e. B ) -> ( ( X .x. Y ) = .0. <-> ( X = .0. \/ Y = .0. ) ) )
Theorem	domnmuln0 19298	In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ ( X e. B /\ X =/= .0. ) /\ ( Y e. B /\ Y =/= .0. ) ) -> ( X .x. Y ) =/= .0. )
Theorem	isdomn2 19299	A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- E = (RLReg ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( R e. Domn <-> ( R e. NzRing /\ ( B \ { .0. } ) C_ E ) )
Theorem	domnrrg 19300	In a domain, any nonzero element is a nonzero-divisor. (Contributed by Mario Carneiro, 28-Mar-2015.)
|- B = ( Base ` R )   &    |- E = (RLReg ` R )   &    |- .0. = ( 0g ` R )   =>    |- ( ( R e. Domn /\ X e. B /\ X =/= .0. ) -> X e. E )