![]() |
Metamath
Proof Explorer Theorem List (p. 211 of 480) | < 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rspssp 21001 | 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 21002 | Moore closure generalizes ideal span. (Contributed by Stefan O'Rear, 4-Apr-2015.) |
β’ π = (LIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ πΉ = (mrClsβπ) β β’ (π β Ring β πΎ = πΉ) | ||
Theorem | lidlnz 21003* | A nonzero ideal contains a nonzero element. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ πΌ β π β§ πΌ β { 0 }) β βπ₯ β πΌ π₯ β 0 ) | ||
Theorem | drngnidl 21004 | 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 21005* | 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 21006 | Ring two-sided ideal function. |
class 2Ideal | ||
Definition | df-2idl 21007 | 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 21008 | Definition of a two-sided ideal. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΌ = (LIdealβπ ) & β’ π = (opprβπ ) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ ) β β’ π = (πΌ β© π½) | ||
Theorem | isridl 21009* | 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.) |
β’ π = (LIdealβ(opprβπ )) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (πΌ β π β (πΌ β (SubGrpβπ ) β§ βπ₯ β π΅ βπ¦ β πΌ (π¦ Β· π₯) β πΌ))) | ||
Theorem | df2idl2 21010* | 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.) |
β’ π = (2Idealβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (πΌ β π β (πΌ β (SubGrpβπ ) β§ βπ₯ β π΅ βπ¦ β πΌ ((π₯ Β· π¦) β πΌ β§ (π¦ Β· π₯) β πΌ)))) | ||
Theorem | ridl0 21011 | Every ring contains a zero right ideal. (Contributed by AV, 13-Feb-2025.) |
β’ π = (LIdealβ(opprβπ )) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β π) | ||
Theorem | ridl1 21012 | Every ring contains a unit right ideal. (Contributed by AV, 13-Feb-2025.) |
β’ π = (LIdealβ(opprβπ )) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β π) | ||
Theorem | 2idl0 21013 | Every ring contains a zero two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
β’ πΌ = (2Idealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β πΌ) | ||
Theorem | 2idl1 21014 | Every ring contains a unit two-sided ideal. (Contributed by AV, 13-Feb-2025.) |
β’ πΌ = (2Idealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β πΌ) | ||
Theorem | 2idlelb 21015 | Membership in a two-sided ideal. Formerly part of proof for 2idlcpbl 21022. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) |
β’ πΌ = (LIdealβπ ) & β’ π = (opprβπ ) & β’ π½ = (LIdealβπ) & β’ π = (2Idealβπ ) β β’ (π β π β (π β πΌ β§ π β π½)) | ||
Theorem | 2idllidld 21016 | A two-sided ideal is a left ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ (π β πΌ β (2Idealβπ )) β β’ (π β πΌ β (LIdealβπ )) | ||
Theorem | 2idlridld 21017 | A two-sided ideal is a right ideal. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ (π β πΌ β (2Idealβπ )) & β’ π = (opprβπ ) β β’ (π β πΌ β (LIdealβπ)) | ||
Theorem | 2idlss 21018 | A two-sided ideal is a subset of the base set. Formerly part of proof for 2idlcpbl 21022. (Contributed by Mario Carneiro, 14-Jun-2015.) (Revised by AV, 20-Feb-2025.) (Proof shortened by AV, 13-Mar-2025.) |
β’ π΅ = (Baseβπ) & β’ πΌ = (2Idealβπ) β β’ (π β πΌ β π β π΅) | ||
Theorem | 2idlbas 21019 | The base set of a two-sided ideal as structure. (Contributed by AV, 20-Feb-2025.) |
β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ π΅ = (Baseβπ½) β β’ (π β π΅ = πΌ) | ||
Theorem | 2idlelbas 21020 | The base set of a two-sided ideal as structure is a left and right ideal. (Contributed by AV, 20-Feb-2025.) |
β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ π΅ = (Baseβπ½) β β’ (π β (π΅ β (LIdealβπ ) β§ π΅ β (LIdealβ(opprβπ )))) | ||
Theorem | 2idlcpblrng 21021 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) Generalization for non-unital rings and two-sided ideals which are subgroups of the additive group of the non-unital ring. (Revised by AV, 23-Feb-2025.) |
β’ π = (Baseβπ ) & β’ πΈ = (π ~QG π) & β’ πΌ = (2Idealβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ π β πΌ β§ π β (SubGrpβπ )) β ((π΄πΈπΆ β§ π΅πΈπ·) β (π΄ Β· π΅)πΈ(πΆ Β· π·))) | ||
Theorem | 2idlcpbl 21022 | The coset equivalence relation for a two-sided ideal is compatible with ring multiplication. (Contributed by Mario Carneiro, 14-Jun-2015.) (Proof shortened by AV, 31-Mar-2025.) |
β’ π = (Baseβπ ) & β’ πΈ = (π ~QG π) & β’ πΌ = (2Idealβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β πΌ) β ((π΄πΈπΆ β§ π΅πΈπ·) β (π΄ Β· π΅)πΈ(πΆ Β· π·))) | ||
Theorem | qus1 21023 | 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 21024 | 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 21025* | 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 | qusmul2 21026 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
β’ π = (π /s (π ~QG πΌ)) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ([π](π ~QG πΌ) Γ [π](π ~QG πΌ)) = [(π Β· π)](π ~QG πΌ)) | ||
Theorem | crngridl 21027 | In a commutative ring, the left and right ideals coincide. (Contributed by Mario Carneiro, 14-Jun-2015.) |
β’ πΌ = (LIdealβπ ) & β’ π = (opprβπ ) β β’ (π β CRing β πΌ = (LIdealβπ)) | ||
Theorem | crng2idl 21028 | 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 | qusmulrng 21029 | Value of the multiplication operation in a quotient ring of a non-unital ring. Formerly part of proof for quscrng 21030. Similar to qusmul2 21026. (Contributed by Mario Carneiro, 15-Jun-2015.) (Revised by AV, 28-Feb-2025.) |
β’ βΌ = (π ~QG π) & β’ π» = (π /s βΌ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ β = (.rβπ») β β’ (((π β Rng β§ π β (2Idealβπ ) β§ π β (SubGrpβπ )) β§ (π β π΅ β§ π β π΅)) β ([π] βΌ β [π] βΌ ) = [(π Β· π)] βΌ ) | ||
Theorem | quscrng 21030 | The quotient of a commutative ring by an ideal is a commutative ring. (Contributed by Mario Carneiro, 15-Jun-2015.) (Proof shortened by AV, 3-Apr-2025.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (LIdealβπ ) β β’ ((π β CRing β§ π β πΌ) β π β CRing) | ||
Remark: Usually, (left) ideals are defined as a subset of a (unital or non-unital) ring that is a subgroup of the additive group of the ring that "absorbs multiplication from the left by elements of the ring", see Wikipedia https://en.wikipedia.org/wiki/Ideal_(ring_theory) (19.02.2025), or the definition 4 in [BourbakiAlg1] p. 103 and the definition in [Lang] p.86, although a ring is to be considered unital (and commutative!) here, see definition 1 in [BourbakiAlg1] p. 96 resp. the definition in [Lang] p. 83, or definition in [Roman] p. 20. In contrast, the definition of (LIdealβπ ), does not require the subset to be a subgroup of the additive group, as can be seen by islidl 20982. If π is a unital ring, however, it can be proven that each ideal in (LIdealβπ ) is a subgroup of the additive group of the ring, see lidlsubg 20988. This is not possible for arbitrary non-unital rings, because the proof uses the existence of the ring unity. | ||
Theorem | dflidl2rng 21031* | 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.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ πΌ β (SubGrpβπ )) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ (π₯ Β· π¦) β πΌ)) | ||
Theorem | isridlrng 21032* | 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.) |
β’ π = (LIdealβ(opprβπ )) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ πΌ β (SubGrpβπ )) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ (π¦ Β· π₯) β πΌ)) | ||
Theorem | rnglidl0 21033 | Every non-unital ring contains a zero ideal. (Contributed by AV, 19-Feb-2025.) |
β’ π = (LIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Rng β { 0 } β π) | ||
Theorem | rnglidl1 21034 | The base set of every non-unital ring is an ideal. For unital rings, such ideals are called "unit ideals", see lidl1 20995. (Contributed by AV, 19-Feb-2025.) |
β’ π = (LIdealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Rng β π΅ β π) | ||
Theorem | rnglidlmmgm 21035 | 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 β π is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.) |
β’ πΏ = (LIdealβπ ) & β’ πΌ = (π βΎs π) & β’ 0 = (0gβπ ) β β’ ((π β Rng β§ π β πΏ β§ 0 β π) β (mulGrpβπΌ) β Mgm) | ||
Theorem | rnglidlmsgrp 21036 | 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 β π is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.) |
β’ πΏ = (LIdealβπ ) & β’ πΌ = (π βΎs π) & β’ 0 = (0gβπ ) β β’ ((π β Rng β§ π β πΏ β§ 0 β π) β (mulGrpβπΌ) β Smgrp) | ||
Theorem | rnglidlrng 21037 | 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 π β (SubGrpβπ ) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025.) |
β’ πΏ = (LIdealβπ ) & β’ πΌ = (π βΎs π) β β’ ((π β Rng β§ π β πΏ β§ π β (SubGrpβπ )) β πΌ β Rng) | ||
Theorem | df2idl2rng 21038* | 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.) |
β’ π = (2Idealβπ ) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Rng β§ πΌ β (SubGrpβπ )) β (πΌ β π β βπ₯ β π΅ βπ¦ β πΌ ((π₯ Β· π¦) β πΌ β§ (π¦ Β· π₯) β πΌ))) | ||
Theorem | rng2idlsubrng 21039 | A two-sided ideal of a non-unital ring which is a non-unital ring is a subring of the ring. (Contributed by AV, 20-Feb-2025.) (Revised by AV, 11-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β (π βΎs πΌ) β Rng) β β’ (π β πΌ β (SubRngβπ )) | ||
Theorem | rng2idlnsg 21040 | A two-sided ideal of a non-unital ring which is a non-unital ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β (π βΎs πΌ) β Rng) β β’ (π β πΌ β (NrmSGrpβπ )) | ||
Theorem | rng2idl0 21041 | The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a non-unital ring. (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β (π βΎs πΌ) β Rng) β β’ (π β (0gβπ ) β πΌ) | ||
Theorem | rng2idlsubgsubrng 21042 | A two-sided ideal of a non-unital ring which is a subgroup of the ring is a subring of the ring. (Contributed by AV, 11-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β πΌ β (SubGrpβπ )) β β’ (π β πΌ β (SubRngβπ )) | ||
Theorem | rng2idlsubgnsg 21043 | A two-sided ideal of a non-unital ring which is a subgroup of the ring is a normal subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β πΌ β (SubGrpβπ )) β β’ (π β πΌ β (NrmSGrpβπ )) | ||
Theorem | rng2idlsubg0 21044 | The zero (additive identity) of a non-unital ring is an element of each two-sided ideal of the ring which is a subgroup of the ring. (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ (π β πΌ β (SubGrpβπ )) β β’ (π β (0gβπ ) β πΌ) | ||
Theorem | qus2idrng 21045 | The quotient of a non-unital ring modulo a two-sided ideal, which is a subgroup of the additive group of the non-unital ring, is a non-unital ring (qusring 21024 analog). (Contributed by AV, 23-Feb-2025.) |
β’ π = (π /s (π ~QG π)) & β’ πΌ = (2Idealβπ ) β β’ ((π β Rng β§ π β πΌ β§ π β (SubGrpβπ )) β π β Rng) | ||
In MathOverflow, the following theorem is claimed: "Theorem 1. Let A be a rng (= nonunital associative ring). Let J be a (two-sided) ideal of A. Assume that both rngs J and A/J are unital. Then, the rng A is also unital.", see https://mathoverflow.net/questions/487676 (/unitality-of-rngs-is-inherited-by-extensions). This thread also contains some hints to literature: Clifford and Preston's book "The Algebraic Theory of Semigroups"(Chapter 5 on representation theory), and Okninski's book Semigroup Algebras, Corollary 8 in Chapter 4. In the following, this theorem is proven formally, see rngringbdlem2 21067 (and variants rngringbd 21068 and ring2idlqusb 21070). This theorem is not trivial, since it is possible for a subset of a ring, especially a subring of a non-unital ring or (left/two-sided) ideal, to be a unital ring with a different ring unity. See also the comment for df-subrg 20460. In the given case, however, the ring unity of the larger ring can be determined by the ring unity of the two-sided ideal and a representative of the ring unity of the corresponding quotient, see ring2idlqus1 21079. An example for such a construction is given in pzriprng1ALT 21266, for the case mentioned in the comment for df-subrg 20460. | ||
Theorem | rngqiprng1elbas 21046 | The ring unity of a two-sided ideal of a non-unital ring belongs to the base set of the ring. (Contributed by AV, 15-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ (π β 1 β π΅) | ||
Theorem | rngqiprngghmlem1 21047 | Lemma 1 for rngqiprngghm 21059. (Contributed by AV, 25-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ ((π β§ π΄ β π΅) β ( 1 Β· π΄) β (Baseβπ½)) | ||
Theorem | rngqiprngghmlem2 21048 | Lemma 2 for rngqiprngghm 21059. (Contributed by AV, 25-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β (( 1 Β· π΄)(+gβπ½)( 1 Β· πΆ)) β (Baseβπ½)) | ||
Theorem | rngqiprngghmlem3 21049 | Lemma 3 for rngqiprngghm 21059. (Contributed by AV, 25-Feb-2025.) (Proof shortened by AV, 24-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β ( 1 Β· (π΄(+gβπ )πΆ)) = (( 1 Β· π΄)(+gβπ½)( 1 Β· πΆ))) | ||
Theorem | rngqiprngimfolem 21050 | Lemma for rngqiprngimfo 21061. (Contributed by AV, 5-Mar-2025.) (Proof shortened by AV, 24-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ ((π β§ π΄ β πΌ β§ πΆ β π΅) β ( 1 Β· ((πΆ(-gβπ )( 1 Β· πΆ))(+gβπ )π΄)) = π΄) | ||
Theorem | rngqiprnglinlem1 21051 | Lemma 1 for rngqiprnglin 21062. (Contributed by AV, 28-Feb-2025.) (Proof shortened by AV, 24-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β (( 1 Β· π΄) Β· ( 1 Β· πΆ)) = ( 1 Β· (π΄ Β· πΆ))) | ||
Theorem | rngqiprnglinlem2 21052 | Lemma 2 for rngqiprnglin 21062. (Contributed by AV, 28-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β [(π΄ Β· πΆ)] βΌ = ([π΄] βΌ (.rβπ)[πΆ] βΌ )) | ||
Theorem | rngqiprnglinlem3 21053 | Lemma 3 for rngqiprnglin 21062. (Contributed by AV, 28-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) β β’ ((π β§ (π΄ β π΅ β§ πΆ β π΅)) β ([π΄] βΌ (.rβπ)[πΆ] βΌ ) β (Baseβπ)) | ||
Theorem | rngqiprngimf1lem 21054 | Lemma for rngqiprngimf1 21060. (Contributed by AV, 7-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) β β’ ((π β§ π΄ β π΅) β (([π΄] βΌ = (0gβπ) β§ ( 1 Β· π΄) = (0gβπ½)) β π΄ = (0gβπ ))) | ||
Theorem | rngqipbas 21055 | The base set of the product of the quotient with a two-sided ideal and the two-sided ideal is the cartesian product of the base set of the quotient and the base set of the two-sided ideal. (Contributed by AV, 21-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) β β’ (π β (Baseβπ) = (πΆ Γ πΌ)) | ||
Theorem | rngqiprng 21056 | The product of the quotient with a two-sided ideal and the two-sided ideal is a non-unital ring. (Contributed by AV, 23-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) β β’ (π β π β Rng) | ||
Theorem | rngqiprngimf 21057* | πΉ is a function from (the base set of) a non-unital ring to the product of the (base set πΆ of the) quotient with a two-sided ideal and the (base set πΌ of the) two-sided ideal (because of 2idlbas 21019, (Baseβπ½) = πΌ!) (Contributed by AV, 21-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ:π΅βΆ(πΆ Γ πΌ)) | ||
Theorem | rngqiprngimfv 21058* | The value of the function πΉ at an element of (the base set of) a non-unital ring. (Contributed by AV, 24-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ ((π β§ π΄ β π΅) β (πΉβπ΄) = β¨[π΄] βΌ , ( 1 Β· π΄)β©) | ||
Theorem | rngqiprngghm 21059* | πΉ is a homomorphism of the additive groups of non-unital rings. (Contributed by AV, 24-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ β (π GrpHom π)) | ||
Theorem | rngqiprngimf1 21060* | πΉ is a one-to-one function from (the base set of) a non-unital ring to the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 7-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ:π΅β1-1β(πΆ Γ πΌ)) | ||
Theorem | rngqiprngimfo 21061* | πΉ is a function from (the base set of) a non-unital ring onto the product of the (base set of the) quotient with a two-sided ideal and the (base set of the) two-sided ideal. (Contributed by AV, 5-Mar-2025.) (Proof shortened by AV, 24-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ:π΅βontoβ(πΆ Γ πΌ)) | ||
Theorem | rngqiprnglin 21062* | πΉ is linear with respect to the multiplication. (Contributed by AV, 28-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β βπ β π΅ βπ β π΅ (πΉβ(π Β· π)) = ((πΉβπ)(.rβπ)(πΉβπ))) | ||
Theorem | rngqiprngho 21063* | πΉ is a homomorphism of non-unital rings. (Contributed by AV, 21-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ β (π RngHom π)) | ||
Theorem | rngqiprngim 21064* | πΉ is an isomorphism of non-unital rings. (Contributed by AV, 21-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ πΆ = (Baseβπ) & β’ π = (π Γs π½) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β πΉ β (π RngIso π)) | ||
Theorem | rng2idl1cntr 21065 | The unity of a two-sided ideal of a non-unital ring is central, i.e., an element of the center of the multiplicative semigroup of the non-unital ring. This is part of the proof given in MathOverflow, which seems to be sufficient to show that πΉ given below (see rngqiprngimf 21057) is an isomorphism. In our proof, however we show that πΉ is linear regarding the multiplication (rngqiprnglin 21062) via rngqiprnglinlem1 21051 instead. (Contributed by AV, 13-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ 1 = (1rβπ½) & β’ π = (mulGrpβπ ) β β’ (π β 1 β (Cntrβπ)) | ||
Theorem | rngringbdlem1 21066 | In a unital ring, the quotient of the ring and a two-sided ideal is unital. (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π = (π /s (π ~QG πΌ)) β β’ ((π β§ π β Ring) β π β Ring) | ||
Theorem | rngringbdlem2 21067 | A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 14-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π = (π /s (π ~QG πΌ)) β β’ ((π β§ π β Ring) β π β Ring) | ||
Theorem | rngringbd 21068 | A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π = (π /s (π ~QG πΌ)) β β’ (π β (π β Ring β π β Ring)) | ||
Theorem | ring2idlqus 21069* | For every unital ring there is a (two-sided) ideal of the ring (in fact the base set of the ring itself) which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 13-Feb-2025.) |
β’ (π β Ring β βπ β (2Idealβπ )((π βΎs π) β Ring β§ (π /s (π ~QG π)) β Ring)) | ||
Theorem | ring2idlqusb 21070* | A non-unital ring is unital if and only if there is a (two-sided) ideal of the ring which is unital, and the quotient of the ring and the ideal is unital. (Proposed by GL, 12-Feb-2025.) (Contributed by AV, 20-Feb-2025.) |
β’ (π β Rng β (π β Ring β βπ β (2Idealβπ )((π βΎs π) β Ring β§ (π /s (π ~QG π)) β Ring))) | ||
Theorem | rngqiprngfulem1 21071* | Lemma 1 for rngqiprngfu 21077 (and lemma for rngqiprngu 21078). (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) β β’ (π β βπ₯ β π΅ (1rβπ) = [π₯] βΌ ) | ||
Theorem | rngqiprngfulem2 21072 | Lemma 2 for rngqiprngfu 21077 (and lemma for rngqiprngu 21078). (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) β β’ (π β πΈ β π΅) | ||
Theorem | rngqiprngfulem3 21073 | Lemma 3 for rngqiprngfu 21077 (and lemma for rngqiprngu 21078). (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) β β’ (π β π β π΅) | ||
Theorem | rngqiprngfulem4 21074 | Lemma 4 for rngqiprngfu 21077. (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) β β’ (π β [π] βΌ = [πΈ] βΌ ) | ||
Theorem | rngqiprngfulem5 21075 | Lemma 5 for rngqiprngfu 21077. (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) β β’ (π β ( 1 Β· π) = 1 ) | ||
Theorem | rngqipring1 21076 | The ring unity of the product of the quotient with a two-sided ideal and the two-sided ideal, which both are rings. (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) & β’ π = (π Γs π½) β β’ (π β (1rβπ) = β¨[πΈ] βΌ , 1 β©) | ||
Theorem | rngqiprngfu 21077* | The function value of πΉ at the constructed expected ring unity of π is the ring unity of the product of the quotient with the two-sided ideal and the two-sided ideal. (Contributed by AV, 16-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) & β’ πΉ = (π₯ β π΅ β¦ β¨[π₯] βΌ , ( 1 Β· π₯)β©) β β’ (π β (πΉβπ) = β¨[πΈ] βΌ , 1 β©) | ||
Theorem | rngqiprngu 21078 | If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025.) |
β’ (π β π β Rng) & β’ (π β πΌ β (2Idealβπ )) & β’ π½ = (π βΎs πΌ) & β’ (π β π½ β Ring) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ 1 = (1rβπ½) & β’ βΌ = (π ~QG πΌ) & β’ π = (π /s βΌ ) & β’ (π β π β Ring) & β’ (π β πΈ β (1rβπ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) & β’ π = ((πΈ β ( 1 Β· πΈ)) + 1 ) β β’ (π β (1rβπ ) = π) | ||
Theorem | ring2idlqus1 21079 | If a non-unital ring has a (two-sided) ideal which is unital, and the quotient of the ring and the ideal is also unital, then the ring is also unital with a ring unity which can be constructed from the ring unity of the ideal and a representative of the ring unity of the quotient. (Contributed by AV, 17-Mar-2025.) |
β’ Β· = (.rβπ ) & β’ 1 = (1rβ(π βΎs πΌ)) & β’ β = (-gβπ ) & β’ + = (+gβπ ) β β’ (((π β Rng β§ πΌ β (2Idealβπ )) β§ ((π βΎs πΌ) β Ring β§ (π /s (π ~QG πΌ)) β Ring) β§ π β (1rβ(π /s (π ~QG πΌ)))) β (π β Ring β§ (1rβπ ) = ((π β ( 1 Β· π)) + 1 ))) | ||
Syntax | clpidl 21080 | Ring left-principal-ideal function. |
class LPIdeal | ||
Syntax | clpir 21081 | Class of left principal ideal rings. |
class LPIR | ||
Definition | df-lpidl 21082* | 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 21083 | 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 21084* | Value of the set of principal ideals. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π = βͺ π β π΅ {(πΎβ{π})}) | ||
Theorem | islpidl 21085* | Property of being a principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ πΎ = (RSpanβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β (πΌ β π β βπ β π΅ πΌ = (πΎβ{π}))) | ||
Theorem | lpi0 21086 | The zero ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } β π) | ||
Theorem | lpi1 21087 | The unit ideal is always principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π΅ = (Baseβπ ) β β’ (π β Ring β π΅ β π) | ||
Theorem | islpir 21088 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β LPIR β (π β Ring β§ π = π)) | ||
Theorem | lpiss 21089 | Principal ideals are a subclass of ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β Ring β π β π) | ||
Theorem | islpir2 21090 | Principal ideal rings are where all ideals are principal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ π = (LPIdealβπ ) & β’ π = (LIdealβπ ) β β’ (π β LPIR β (π β Ring β§ π β π)) | ||
Theorem | lpirring 21091 | Principal ideal rings are rings. (Contributed by Stefan O'Rear, 24-Jan-2015.) |
β’ (π β LPIR β π β Ring) | ||
Theorem | drnglpir 21092 | Division rings are principal ideal. (Contributed by Stefan O'Rear, 3-Jan-2015.) |
β’ (π β DivRing β π β LPIR) | ||
Theorem | rspsn 21093* | 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 21094* | 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 21095* | 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 | crlreg 21096 | Set of left-regular elements in a ring. |
class RLReg | ||
Syntax | cdomn 21097 | Class of (ring theoretic) domains. |
class Domn | ||
Syntax | cidom 21098 | Class of integral domains. |
class IDomn | ||
Syntax | cpid 21099 | Class of principal ideal domains. |
class PID | ||
Definition | df-rlreg 21100* | 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βπ))}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |