Home | Metamath
Proof Explorer Theorem List (p. 207 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rlmscaf 20601 | Functionalized scalar multiplication in the ring module. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ (+πβ(mulGrpβπ )) = ( Β·sf β(ringLModβπ )) | ||
Theorem | ixpsnbasval 20602* | 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.) |
β’ ((π β π β§ π β π) β Xπ₯ β {π} (Baseβ(({π} Γ {(ringLModβπ )})βπ₯)) = {π β£ (π Fn {π} β§ (πβπ) β (Baseβπ ))}) | ||
Theorem | lidlss 20603 | An ideal is a subset of the base set. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ π΅ = (Baseβπ) & β’ πΌ = (LIdealβπ) β β’ (π β πΌ β π β π΅) | ||
Theorem | islidl 20604* | Predicate of being a (left) ideal. (Contributed by Stefan O'Rear, 1-Apr-2015.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ Β· = (.rβπ ) β β’ (πΌ β π β (πΌ β π΅ β§ πΌ β β β§ βπ₯ β π΅ βπ β πΌ βπ β πΌ ((π₯ Β· π) + π) β πΌ)) | ||
Theorem | lidl0cl 20605 | An ideal contains 0. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΌ β π) β 0 β πΌ) | ||
Theorem | lidlacl 20606 | An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ + = (+gβπ ) β β’ (((π β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π + π) β πΌ) | ||
Theorem | lidlnegcl 20607 | An ideal contains negatives. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ π = (invgβπ ) β β’ ((π β Ring β§ πΌ β π β§ π β πΌ) β (πβπ) β πΌ) | ||
Theorem | lidlsubg 20608 | An ideal is a subgroup of the additive group. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β πΌ β (SubGrpβπ )) | ||
Theorem | lidlsubcl 20609 | An ideal is closed under subtraction. (Contributed by Stefan O'Rear, 28-Mar-2015.) (Proof shortened by OpenAI, 25-Mar-2020.) |
β’ π = (LIdealβπ ) & β’ β = (-gβπ ) β β’ (((π β Ring β§ πΌ β π) β§ (π β πΌ β§ π β πΌ)) β (π β π) β πΌ) | ||
Theorem | lidlmcl 20610 | An ideal is closed under left-multiplication by elements of the full ring. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (((π β Ring β§ πΌ β π) β§ (π β π΅ β§ π β πΌ)) β (π Β· π) β πΌ) | ||
Theorem | lidl1el 20611 | 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.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β π) β ( 1 β πΌ β πΌ = π΅)) | ||
Theorem | lidl0 20612 | Every ring contains a zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β π) | ||
Theorem | lidl1 20613 | Every ring contains a unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β π) | ||
Theorem | lidlacs 20614 | The ideal system is an algebraic closure system on the base set. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π΅ = (Baseβπ) & β’ πΌ = (LIdealβπ) β β’ (π β Ring β πΌ β (ACSβπ΅)) | ||
Theorem | rspcl 20615 | 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.) |
β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΊ β π΅) β (πΎβπΊ) β π) | ||
Theorem | rspssid 20616 | The span of a set of ring elements contains those elements. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβπΊ)) | ||
Theorem | rsp1 20617 | The span of the identity element is the unit ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β (πΎβ{ 1 }) = π΅) | ||
Theorem | rsp0 20618 | The span of the zero element is the zero ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ πΎ = (RSpanβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β (πΎβ{ 0 }) = { 0 }) | ||
Theorem | rspssp 20619 | 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.) |
β’ πΎ = (RSpanβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ πΊ β πΌ) β (πΎβπΊ) β πΌ) | ||
Theorem | mrcrsp 20620 | Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (LIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ πΉ = (mrClsβπ) β β’ (π β Ring β πΎ = πΉ) | ||
Theorem | lidlnz 20621* | A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΌ β π β§ πΌ β { 0 }) β βπ₯ β πΌ π₯ β 0 ) | ||
Theorem | drngnidl 20622 | A division ring has only the two trivial ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Wolf Lammen, 6-Sep-2020.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (LIdealβπ ) β β’ (π β DivRing β π = {{ 0 }, π΅}) | ||
Theorem | lidlrsppropd 20623* | The left ideals and ring span of a ring depend only on the ring components. Here π is expected to be either π΅ (when closure is available) or V (when strong equality is available). (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) β π) & β’ ((π β§ (π₯ β π΅ β§ π¦ β π΅)) β (π₯(.rβπΎ)π¦) = (π₯(.rβπΏ)π¦)) β β’ (π β ((LIdealβπΎ) = (LIdealβπΏ) β§ (RSpanβπΎ) = (RSpanβπΏ))) | ||
Syntax | c2idl 20624 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 20625 | 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 = (π β V β¦ ((LIdealβπ) β© (LIdealβ(opprβπ)))) | ||
Theorem | 2idlval 20626 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΌ = (LIdealβπ ) & β’ π = (opprβπ ) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ ) β β’ π = (πΌ β© π½) | ||
Theorem | 2idlcpbl 20627 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (Baseβπ ) & β’ πΈ = (π ~QG π) & β’ πΌ = (2Idealβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΌ) β ((π΄πΈπΆ β§ π΅πΈπ·) β (π΄ Β· π΅)πΈ(πΆ Β· π·))) | ||
Theorem | qus1 20628 | The multiplicative identity of the quotient ring. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (2Idealβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β πΌ) β (π β Ring β§ [ 1 ](π ~QG π) = (1rβπ))) | ||
Theorem | qusring 20629 | If π is a two-sided ideal in π , then π = π / π is a ring, called the quotient ring of π by π. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (2Idealβπ ) β β’ ((π β Ring β§ π β πΌ) β π β Ring) | ||
Theorem | qusrhm 20630* | If π is a two-sided ideal in π , then the "natural map" from elements to their cosets is a ring homomorphism from π to π / π. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (2Idealβπ ) & β’ π = (Baseβπ ) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG π)) β β’ ((π β Ring β§ π β πΌ) β πΉ β (π RingHom π)) | ||
Theorem | crngridl 20631 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΌ = (LIdealβπ ) & β’ π = (opprβπ ) β β’ (π β CRing β πΌ = (LIdealβπ)) | ||
Theorem | crng2idl 20632 | In a commutative ring, a two-sided ideal is the same as a left ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΌ = (LIdealβπ ) β β’ (π β CRing β πΌ = (2Idealβπ )) | ||
Theorem | quscrng 20633 | The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (LIdealβπ ) β β’ ((π β CRing β§ π β πΌ) β π β CRing) | ||
Syntax | clpidl 20634 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 20635 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 20636* | 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 = (π€ β Ring β¦ βͺ π β (Baseβπ€){((RSpanβπ€)β{π})}) | ||
Definition | df-lpir 20637 | 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 = {π€ β Ring β£ (LIdealβπ€) = (LPIdealβπ€)} | ||
Theorem | lpival 20638* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π = βͺ π β π΅ {(πΎβ{π})}) | ||
Theorem | islpidl 20639* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β (πΌ β π β βπ β π΅ πΌ = (πΎβ{π}))) | ||
Theorem | lpi0 20640 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β π) | ||
Theorem | lpi1 20641 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β π) | ||
Theorem | islpir 20642 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β LPIR β (π β Ring β§ π = π)) | ||
Theorem | lpiss 20643 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β Ring β π β π) | ||
Theorem | islpir2 20644 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β LPIR β (π β Ring β§ π β π)) | ||
Theorem | lpirring 20645 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π β LPIR β π β Ring) | ||
Theorem | drnglpir 20646 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ (π β DivRing β π β LPIR) | ||
Theorem | rspsn 20647* | Membership in principal ideals is closely related to divisibility. (Contributed by Stefan O'Rear, 3-Jan-2015.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ πΊ β π΅) β (πΎβ{πΊ}) = {π₯ β£ πΊ β₯ π₯}) | ||
Theorem | lidldvgen 20648* | 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.) |
β’ π΅ = (Baseβπ ) & β’ π = (LIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ πΌ β π β§ πΊ β π΅) β (πΌ = (πΎβ{πΊ}) β (πΊ β πΌ β§ βπ₯ β πΌ πΊ β₯ π₯))) | ||
Theorem | lpigen 20649* | 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.) |
β’ π = (LIdealβπ ) & β’ π = (LPIdealβπ ) & β’ β₯ = (β₯rβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΌ β π β βπ₯ β πΌ βπ¦ β πΌ π₯ β₯ π¦)) | ||
Syntax | cnzr 20650 | The class of nonzero rings. |
class NzRing | ||
Definition | df-nzr 20651 | 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 = {π β Ring β£ (1rβπ) β (0gβπ)} | ||
Theorem | isnzr 20652 | Property of a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β (π β Ring β§ 1 β 0 )) | ||
Theorem | nzrnz 20653 | One and zero are different in a nonzero ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ 1 = (1rβπ ) & β’ 0 = (0gβπ ) β β’ (π β NzRing β 1 β 0 ) | ||
Theorem | nzrring 20654 | A nonzero ring is a ring. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β NzRing β π β Ring) | ||
Theorem | drngnzr 20655 | All division rings are nonzero. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ (π β DivRing β π β NzRing) | ||
Theorem | isnzr2 20656 | Equivalent characterization of nonzero rings: they have at least two elements. (Contributed by Stefan O'Rear, 24-Feb-2015.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 2o βΌ π΅)) | ||
Theorem | isnzr2hash 20657 | Equivalent characterization of nonzero rings: they have at least two elements. Analogous to isnzr2 20656. (Contributed by AV, 14-Apr-2019.) |
β’ π΅ = (Baseβπ ) β β’ (π β NzRing β (π β Ring β§ 1 < (β―βπ΅))) | ||
Theorem | opprnzr 20658 | The opposite of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ π = (opprβπ ) β β’ (π β NzRing β π β NzRing) | ||
Theorem | ringelnzr 20659 | 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βπ ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (π΅ β { 0 })) β π β NzRing) | ||
Theorem | nzrunit 20660 | A unit is nonzero in any nonzero ring. (Contributed by Mario Carneiro, 6-Oct-2015.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) β β’ ((π β NzRing β§ π΄ β π) β π΄ β 0 ) | ||
Theorem | subrgnzr 20661 | A subring of a nonzero ring is nonzero. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (π βΎs π΄) β β’ ((π β NzRing β§ π΄ β (SubRingβπ )) β π β NzRing) | ||
Theorem | 0ringnnzr 20662 | A ring is a zero ring iff it is not a nonzero ring. (Contributed by AV, 14-Apr-2019.) |
β’ (π β Ring β ((β―β(Baseβπ )) = 1 β Β¬ π β NzRing)) | ||
Theorem | 0ring 20663 | 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.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β π΅ = { 0 }) | ||
Theorem | 0ring01eq 20664 | 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.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β 0 = 1 ) | ||
Theorem | 01eq0ring 20665 | 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.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ 0 = 1 ) β π΅ = { 0 }) | ||
Theorem | 0ring01eqbi 20666 | 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.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β Ring β (π΅ β 1o β 1 = 0 )) | ||
Theorem | rng1nnzr 20667 | The (smallest) structure representing a zero ring is not a nonzero ring. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β NzRing) | ||
Theorem | ring1zr 20668 | 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 π β 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.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) β β’ (((π β Ring β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β§ π β π΅) β (π΅ = {π} β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | rngen1zr 20669 | The only (unital) ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption π β 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.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) β β’ (((π β Ring β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β§ π β π΅) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | ringen1zr 20670 | The only unital ring with one element is the zero ring (at least if its operations are internal binary operations). Note: The assumption π β 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.) |
β’ π΅ = (Baseβπ ) & β’ + = (+gβπ ) & β’ β = (.rβπ ) & β’ π = (0gβπ ) β β’ ((π β Ring β§ + Fn (π΅ Γ π΅) β§ β Fn (π΅ Γ π΅)) β (π΅ β 1o β ( + = {β¨β¨π, πβ©, πβ©} β§ β = {β¨β¨π, πβ©, πβ©}))) | ||
Theorem | rng1nfld 20671 | The zero ring is not a field. (Contributed by AV, 29-Apr-2019.) |
β’ π = {β¨(Baseβndx), {π}β©, β¨(+gβndx), {β¨β¨π, πβ©, πβ©}β©, β¨(.rβndx), {β¨β¨π, πβ©, πβ©}β©} β β’ (π β π β π β Field) | ||
Syntax | crlreg 20672 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 20673 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 20674 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 20675 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 20676* | 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 = (π β V β¦ {π₯ β (Baseβπ) β£ βπ¦ β (Baseβπ)((π₯(.rβπ)π¦) = (0gβπ) β π¦ = (0gβπ))}) | ||
Definition | df-domn 20677* | A domain is a nonzero ring in which there are no nontrivial zero divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ Domn = {π β NzRing β£ [(Baseβπ) / π][(0gβπ) / π§]βπ₯ β π βπ¦ β π ((π₯(.rβπ)π¦) = π§ β (π₯ = π§ β¨ π¦ = π§))} | ||
Definition | df-idom 20678 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ IDomn = (CRing β© Domn) | ||
Definition | df-pid 20679 | A principal ideal domain is an integral domain satisfying the left principal ideal property. (Contributed by Stefan O'Rear, 29-Mar-2015.) |
β’ PID = (IDomn β© LPIR) | ||
Theorem | rrgval 20680* | Value of the set or left-regular elements in a ring. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ πΈ = {π₯ β π΅ β£ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β π¦ = 0 )} | ||
Theorem | isrrg 20681* | Membership in the set of left-regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β πΈ β (π β π΅ β§ βπ¦ β π΅ ((π Β· π¦) = 0 β π¦ = 0 ))) | ||
Theorem | rrgeq0i 20682 | Property of a left-regular element. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β πΈ β§ π β π΅) β ((π Β· π) = 0 β π = 0 )) | ||
Theorem | rrgeq0 20683 | Left-multiplication by a left regular element does not change zeroness. (Contributed by Stefan O'Rear, 28-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ π β πΈ β§ π β π΅) β ((π Β· π) = 0 β π = 0 )) | ||
Theorem | rrgsupp 20684 | 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.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) & β’ (π β πΌ β π) & β’ (π β π β Ring) & β’ (π β π β πΈ) & β’ (π β π:πΌβΆπ΅) β β’ (π β (((πΌ Γ {π}) βf Β· π) supp 0 ) = (π supp 0 )) | ||
Theorem | rrgss 20685 | Left-regular elements are a subset of the base set. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π΅ = (Baseβπ ) β β’ πΈ β π΅ | ||
Theorem | unitrrg 20686 | Units are regular elements. (Contributed by Stefan O'Rear, 22-Mar-2015.) |
β’ πΈ = (RLRegβπ ) & β’ π = (Unitβπ ) β β’ (π β Ring β π β πΈ) | ||
Theorem | isdomn 20687* | Expand definition of a domain. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ (π β Domn β (π β NzRing β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) = 0 β (π₯ = 0 β¨ π¦ = 0 )))) | ||
Theorem | domnnzr 20688 | A domain is a nonzero ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ (π β Domn β π β NzRing) | ||
Theorem | domnring 20689 | A domain is a ring. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ (π β Domn β π β Ring) | ||
Theorem | domneq0 20690 | In a domain, a product is zero iff it has a zero factor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Domn β§ π β π΅ β§ π β π΅) β ((π Β· π) = 0 β (π = 0 β¨ π = 0 ))) | ||
Theorem | domnmuln0 20691 | In a domain, a product of nonzero elements is nonzero. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Domn β§ (π β π΅ β§ π β 0 ) β§ (π β π΅ β§ π β 0 )) β (π Β· π) β 0 ) | ||
Theorem | isdomn2 20692 | A ring is a domain iff all nonzero elements are nonzero-divisors. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΈ = (RLRegβπ ) & β’ 0 = (0gβπ ) β β’ (π β Domn β (π β NzRing β§ (π΅ β { 0 }) β πΈ)) | ||
Theorem | domnrrg 20693 | In a domain, any nonzero element is a nonzero-divisor. (Contributed by Mario Carneiro, 28-Mar-2015.) |
β’ π΅ = (Baseβπ ) & β’ πΈ = (RLRegβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Domn β§ π β π΅ β§ π β 0 ) β π β πΈ) | ||
Theorem | opprdomn 20694 | The opposite of a domain is also a domain. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π = (opprβπ ) β β’ (π β Domn β π β Domn) | ||
Theorem | abvn0b 20695 | Another characterization of domains, hinted at in abvtriv 20223: a nonzero ring is a domain iff it has an absolute value. (Contributed by Mario Carneiro, 6-May-2015.) |
β’ π΄ = (AbsValβπ ) β β’ (π β Domn β (π β NzRing β§ π΄ β β )) | ||
Theorem | drngdomn 20696 | A division ring is a domain. (Contributed by Mario Carneiro, 29-Mar-2015.) |
β’ (π β DivRing β π β Domn) | ||
Theorem | isidom 20697 | An integral domain is a commutative domain. (Contributed by Mario Carneiro, 17-Jun-2015.) |
β’ (π β IDomn β (π β CRing β§ π β Domn)) | ||
Theorem | fldidom 20698 | A field is an integral domain. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof shortened by SN, 11-Nov-2024.) |
β’ (π β Field β π β IDomn) | ||
Theorem | fldidomOLD 20699 | Obsolete version of fldidom 20698 as of 11-Nov-2024. (Contributed by Mario Carneiro, 29-Mar-2015.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β Field β π β IDomn) | ||
Theorem | fidomndrnglem 20700* | Lemma for fidomndrng 20701. (Contributed by Mario Carneiro, 15-Jun-2015.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Domn) & β’ (π β π΅ β Fin) & β’ (π β π΄ β (π΅ β { 0 })) & β’ πΉ = (π₯ β π΅ β¦ (π₯ Β· π΄)) β β’ (π β π΄ β₯ 1 ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |