P. 163 of Theorem List - Metamath Proof Explorer

Mirrors  >  Metamath Home Page  >  MPE Home Page  >  Theorem List Contents  >  Recent Proofs       This page: Page List

Theorem List for Metamath Proof Explorer - 16201-16300   *Has distinct variable group(s)

Type	Label	Description
Statement
Definition	df-lidl 16201	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 16202	Define the linear span function in a ring (Ideal generator). (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- RSpan = ( LSpan o. ringLMod )
Theorem	sraval 16203	Lemma for srabase 16205 through sravsca 16209. (Contributed by Mario Carneiro, 27-Nov-2014.)
|- ( ( W e. V /\ S C_ ( Base ` W ) ) -> ( ( subringAlg ` W ) ` S ) = ( ( W sSet <. (Scalar ` ndx ) , ( W ↾s S ) >. ) sSet <. ( .s ` ndx ) , ( .r ` W ) >. ) )
Theorem	sralem 16204	Lemma for srabase 16205 and similar theorems. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   &    |- E = Slot N   &    |- N e. NN   &    |- ( N < 5 \/ 6 < N )   =>    |- ( ph -> ( E ` W ) = ( E ` A ) )
Theorem	srabase 16205	Base set of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( Base ` W ) = ( Base ` A ) )
Theorem	sraaddg 16206	Additive operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( +g ` W ) = ( +g ` A ) )
Theorem	sramulr 16207	Multiplicative operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( .r ` W ) = ( .r ` A ) )
Theorem	srasca 16208	The set of scalars of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( W ↾s S ) = (Scalar ` A ) )
Theorem	sravsca 16209	The scalar product operation of a subring algebra. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( .r ` W ) = ( .s ` A ) )
Theorem	sratset 16210	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> (TopSet ` W ) = (TopSet ` A ) )
Theorem	sratopn 16211	Topology component of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( TopOpen ` W ) = ( TopOpen ` A ) )
Theorem	srads 16212	Distance function of a subring algebra. (Contributed by Mario Carneiro, 4-Oct-2015.)
|- ( ph -> A = ( ( subringAlg ` W ) ` S ) )   &    |- ( ph -> S C_ ( Base ` W ) )   =>    |- ( ph -> ( dist ` W ) = ( dist ` A ) )
Theorem	sralmod 16213	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	sralmod0 16214	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 -> .0. = ( 0g ` A ) )
Theorem	issubgrpd2 16215*	Prove a subgroup 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 ) -> ( ( inv g ` I ) ` x ) e. D )   &    |- ( ph -> I e. Grp )   =>    |- ( ph -> D e. (SubGrp ` I ) )
Theorem	issubgrpd 16216*	Prove a subgroup by closure. (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 ) -> ( ( inv g ` I ) ` x ) e. D )   &    |- ( ph -> I e. Grp )   =>    |- ( ph -> S e. Grp )
Theorem	issubrngd2 16217*	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 ) -> ( ( inv g ` 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 16218	ringLMod is a function. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ringLMod Fn _V
Theorem	rlmval 16219	Value of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- (ringLMod ` W ) = ( ( subringAlg ` W ) ` ( Base ` W ) )
Theorem	lidlval 16220	Value of the set of ring ideals. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- (LIdeal ` W ) = ( LSubSp ` (ringLMod ` W ) )
Theorem	rspval 16221	Value of the ring span function. (Contributed by Stefan O'Rear, 4-Apr-2015.)
|- (RSpan ` W ) = ( LSpan ` (ringLMod ` W ) )
Theorem	rlmbas 16222	Base set of the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( Base ` R ) = ( Base ` (ringLMod ` R ) )
Theorem	rlmplusg 16223	Vector addition in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( +g ` R ) = ( +g ` (ringLMod ` R ) )
Theorem	rlm0 16224	Zero vector in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 2-Oct-2015.)
|- ( 0g ` R ) = ( 0g ` (ringLMod ` R ) )
Theorem	rlmmulr 16225	Ring multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( .r ` R ) = ( .r ` (ringLMod ` R ) )
Theorem	rlmsca 16226	Scalars in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. X -> R = (Scalar ` (ringLMod ` R ) ) )
Theorem	rlmsca2 16227	Scalars in the ring module. (Contributed by Stefan O'Rear, 1-Apr-2015.)
|- ( _I ` R ) = (Scalar ` (ringLMod ` R ) )
Theorem	rlmvsca 16228	Scalar multiplication in the ring module. (Contributed by Stefan O'Rear, 31-Mar-2015.)
|- ( .r ` R ) = ( .s ` (ringLMod ` R ) )
Theorem	rlmtopn 16229	Topology component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( TopOpen ` R ) = ( TopOpen ` (ringLMod ` R ) )
Theorem	rlmds 16230	Metric component of the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( dist ` R ) = ( dist ` (ringLMod ` R ) )
Theorem	rlmlmod 16231	The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014.)
|- ( R e. Ring -> (ringLMod ` R ) e. LMod )
Theorem	rlmlvec 16232	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 16233	Vector negation in the ring module. (Contributed by Stefan O'Rear, 6-Dec-2014.) (Revised by Mario Carneiro, 5-Jun-2015.)
|- ( inv g ` R ) = ( inv g ` (ringLMod ` R ) )
Theorem	rlmscaf 16234	Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.)
|- ( + f ` (mulGrp ` R ) ) = ( .s f ` (ringLMod ` R ) )
Theorem	lidlss 16235	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	lidlssOLD 16236	An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Proof modification is discouraged.) (New usage is discouraged.)
|- B = ( Base ` W )   &    |- I = (LIdeal ` W )   =>    |- ( ( W e. V /\ U e. I ) -> U C_ B )
Theorem	islidl 16237*	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 16238	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 16239	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 16240	An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- N = ( inv g ` R )   =>    |- ( ( R e. Ring /\ I e. U /\ X e. I ) -> ( N ` X ) e. I )
Theorem	lidlsubg 16241	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 16242	An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015.)
|- U = (LIdeal ` R )   &    |- .- = ( -g ` R )   =>    |- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .- Y ) e. I )
Theorem	lidlmcl 16243	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 16244	An ideal contains 1 iff it is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- U = (LIdeal ` R )   &    |- B = ( Base ` R )   &    |- .1. = ( 1r ` R )   =>    |- ( ( R e. Ring /\ I e. U ) -> ( .1. e. I <-> I = B ) )
Theorem	lidl0 16245	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 16246	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 16247	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 16248	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 16249	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 16250	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 16251	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 16252	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 16253	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 16254*	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 16255	A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- B = ( Base ` R )   &    |- .0. = ( 0g ` R )   &    |- U = (LIdeal ` R )   =>    |- ( R e. DivRing -> U = { { .0. } , B } )
Theorem	lidlrsppropd 16256*	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 16257	Ring two-sided ideal function.
class 2Ideal
Definition	df-2idl 16258	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 16259	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 16260	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	divs1 16261	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	divsrng 16262	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	divsrhm 16263*	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 16264	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 16265	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	divscrng 16266	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 16267	Ring left-principal-ideal function.
class LPIdeal
Syntax	clpir 16268	Class of left principal ideal rings.
class LPIR
Definition	df-lpidl 16269*	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 16270	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 16271*	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 16272*	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 16273	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 16274	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 16275	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 16276	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 16277	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	lpirrng 16278	Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.)
|- ( R e. LPIR -> R e. Ring )
Theorem	drnglpir 16279	Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- ( R e. DivRing -> R e. LPIR )
Theorem	rspsn 16280*	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 16281*	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 16282*	An ideal is principal iff it contains an element which right-divides all elements. (Contributed by Stefan O'Rear, 3-Jan-2015.)
|- 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
Syntax	cnzr 16283	The class of nonzero rings.
class NzRing
Definition	df-nzr 16284	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 16285	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 16286	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	nzrrng 16287	A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. NzRing -> R e. Ring )
Theorem	drngnzr 16288	All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.)
|- ( R e. DivRing -> R e. NzRing )
Theorem	isnzr2 16289	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	opprnzr 16290	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	rngelnzr 16291	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 16292	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 16293	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 )
10.8.5  Left regular elements. More kinds of rings
Syntax	crlreg 16294	Set of left-regular elements in a ring.
class RLReg
Syntax	cdomn 16295	Class of (ring theoretic) domains.
class Domn
Syntax	cidom 16296	Class of integral domains.
class IDomn
Syntax	cpid 16297	Class of principal ideal domains.
class PID
Definition	df-rlreg 16298*	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 16299*	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 16300	An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.)
|- IDomn = ( CRing i^i Domn )