![]() |
Metamath
Proof Explorer Theorem List (p. 331 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | qusker 33001* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) & β’ π = (π /s (π ~QG πΊ)) & β’ 0 = (0gβπ) β β’ (πΊ β (NrmSGrpβπ) β (β‘πΉ β { 0 }) = πΊ) | ||
Theorem | eqgvscpbl 33002 | The left coset equivalence relation is compatible with the scalar multiplication operation. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) β β’ (π β (π βΌ π β (πΎ Β· π) βΌ (πΎ Β· π))) | ||
Theorem | qusvscpbl 33003* | The quotient map distributes over the scalar multiplication. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) & β’ π = (π /s (π ~QG πΊ)) & β’ β = ( Β·π βπ) & β’ πΉ = (π₯ β π΅ β¦ [π₯](π ~QG πΊ)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((πΉβπ) = (πΉβπ) β (πΉβ(πΎ Β· π)) = (πΉβ(πΎ Β· π)))) | ||
Theorem | qusvsval 33004 | Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π΅ = (Baseβπ) & β’ βΌ = (π ~QG πΊ) & β’ π = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ (π β πΎ β π) & β’ π = (π /s (π ~QG πΊ)) & β’ β = ( Β·π βπ) & β’ (π β π β π΅) β β’ (π β (πΎ β [π](π ~QG πΊ)) = [(πΎ Β· π)](π ~QG πΊ)) | ||
Theorem | imaslmod 33005* | The image structure of a left module is a left module. (Contributed by Thierry Arnoux, 15-May-2023.) |
β’ (π β π = (πΉ βs π)) & β’ π = (Baseβπ) & β’ π = (Baseβ(Scalarβπ)) & β’ + = (+gβπ) & β’ Β· = ( Β·π βπ) & β’ 0 = (0gβπ) & β’ (π β πΉ:πβontoβπ΅) & β’ ((π β§ (π β π β§ π β π) β§ (π β π β§ π β π)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ ((π β§ (π β π β§ π β π β§ π β π)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π β LMod) β β’ (π β π β LMod) | ||
Theorem | imasmhm 33006* | Given a function πΉ with homomorphic properties, build the image of a monoid. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΅ = (Baseβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ + = (+gβπ) & β’ ((π β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Mnd) β β’ (π β ((πΉ βs π) β Mnd β§ πΉ β (π MndHom (πΉ βs π)))) | ||
Theorem | imasghm 33007* | Given a function πΉ with homomorphic properties, build the image of a group. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΅ = (Baseβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ + = (+gβπ) & β’ ((π β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ (π β π β Grp) β β’ (π β ((πΉ βs π) β Grp β§ πΉ β (π GrpHom (πΉ βs π)))) | ||
Theorem | imasrhm 33008* | Given a function πΉ with homomorphic properties, build the image of a ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΅ = (Baseβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ + = (+gβπ) & β’ ((π β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ Β· = (.rβπ) & β’ ((π β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π Β· π)) = (πΉβ(π Β· π)))) & β’ (π β π β Ring) β β’ (π β ((πΉ βs π) β Ring β§ πΉ β (π RingHom (πΉ βs π)))) | ||
Theorem | imaslmhm 33009* | Given a function πΉ with homomorphic properties, build the image of a left module. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΅ = (Baseβπ) & β’ (π β πΉ:π΅βΆπΆ) & β’ + = (+gβπ) & β’ ((π β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β (((πΉβπ) = (πΉβπ) β§ (πΉβπ) = (πΉβπ)) β (πΉβ(π + π)) = (πΉβ(π + π)))) & β’ π· = (Scalarβπ) & β’ πΎ = (Baseβπ·) & β’ ((π β§ (π β πΎ β§ π β π΅ β§ π β π΅)) β ((πΉβπ) = (πΉβπ) β (πΉβ(π Γ π)) = (πΉβ(π Γ π)))) & β’ (π β π β LMod) & β’ Γ = ( Β·π βπ) β β’ (π β ((πΉ βs π) β LMod β§ πΉ β (π LMHom (πΉ βs π)))) | ||
Theorem | quslmod 33010 | If πΊ is a submodule in π, then π = π / πΊ is a left module, called the quotient module of π by πΊ. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (π /s (π ~QG πΊ)) & β’ π = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) β β’ (π β π β LMod) | ||
Theorem | quslmhm 33011* | If πΊ is a submodule of π, then the "natural map" from elements to their cosets is a left module homomorphism from π to π / πΊ. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (π /s (π ~QG πΊ)) & β’ π = (Baseβπ) & β’ (π β π β LMod) & β’ (π β πΊ β (LSubSpβπ)) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) β β’ (π β πΉ β (π LMHom π)) | ||
Theorem | quslvec 33012 | If π is a vector subspace in π, then π = π / π is a vector space, called the quotient space of π by π. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (π /s (π ~QG π)) & β’ (π β π β LVec) & β’ (π β π β (LSubSpβπ)) β β’ (π β π β LVec) | ||
Theorem | ecxpid 33013 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ (π β π΄ β [π](π΄ Γ π΄) = π΄) | ||
Theorem | qsxpid 33014 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ (π΄ β β β (π΄ / (π΄ Γ π΄)) = {π΄}) | ||
Theorem | qusxpid 33015 | The Group quotient equivalence relation for the whole group is the cartesian product, i.e. all elements are in the same equivalence class. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ π΅ = (BaseβπΊ) β β’ (πΊ β Grp β (πΊ ~QG π΅) = (π΅ Γ π΅)) | ||
Theorem | qustriv 33016 | The quotient of a group πΊ by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π΅)) β β’ (πΊ β Grp β (Baseβπ) = {π΅}) | ||
Theorem | qustrivr 33017 | Converse of qustriv 33016. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π»)) β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ) β§ (Baseβπ) = {π»}) β π» = π΅) | ||
Theorem | znfermltl 33018 | Fermat's little theorem in β€/nβ€. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβ(mulGrpβπ)) β β’ ((π β β β§ π΄ β π΅) β (π β π΄) = π΄) | ||
Theorem | islinds5 33019* | A set is linearly independent if and only if it has no non-trivial representations of zero. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ πΉ = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπΉ) β β’ ((π β LMod β§ π β π΅) β (π β (LIndSβπ) β βπ β (πΎ βm π)((π finSupp 0 β§ (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£))) = π) β π = (π Γ { 0 })))) | ||
Theorem | ellspds 33020* | Variation on ellspd 21723. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β π΅) β β’ (π β (π β (πβπ) β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
Theorem | 0ellsp 33021 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π΅) β 0 β (πβπ)) | ||
Theorem | 0nellinds 33022 | The group identity cannot be an element of an independent set. (Contributed by Thierry Arnoux, 8-May-2023.) |
β’ 0 = (0gβπ) β β’ ((π β LVec β§ πΉ β (LIndSβπ)) β Β¬ 0 β πΉ) | ||
Theorem | rspsnel 33023* | Membership in a principal ideal. Analogous to lspsnel 20876. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅) β (πΌ β (πΎβ{π}) β βπ₯ β π΅ πΌ = (π₯ Β· π))) | ||
Theorem | rspsnid 33024 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβ{πΊ})) | ||
Theorem | elrsp 33025* | Write the elements of a ring span as finite linear combinations. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) β β’ (π β (π β (πβπΌ) β βπ β (π΅ βm πΌ)(π finSupp 0 β§ π = (π Ξ£g (π β πΌ β¦ ((πβπ) Β· π)))))) | ||
Theorem | rspidlid 33026 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ πΎ = (RSpanβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΎβπΌ) = πΌ) | ||
Theorem | pidlnz 33027 | A principal ideal generated by a nonzero element is not the zero ideal. (Contributed by Thierry Arnoux, 11-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅ β§ π β 0 ) β (πΎβ{π}) β { 0 }) | ||
Theorem | dvdsruassoi 33028 | If two elements π and π of a ring π are unit multiples, then they are associates, i.e. each divides the other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β π) & β’ (π β (π Β· π) = π) β β’ (π β (π β₯ π β§ π β₯ π)) | ||
Theorem | dvdsruasso 33029* | Two elements π and π of a ring π are associates, i.e. each divides the other, iff they are unit multiples of each other. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ π = (Unitβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β IDomn) β β’ (π β ((π β₯ π β§ π β₯ π) β βπ’ β π (π’ Β· π) = π)) | ||
Theorem | dvdsrspss 33030 | In a ring, an element π divides π iff the ideal generated by π is a subset of the ideal generated by π (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Ring) β β’ (π β (π β₯ π β (πΎβ{π}) β (πΎβ{π}))) | ||
Theorem | rspsnasso 33031 | Two elements π and π of a ring π are associates, i.e. each divides the other, iff the ideals they generate are equal. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) & β’ β₯ = (β₯rβπ ) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β Ring) β β’ (π β ((π β₯ π β§ π β₯ π) β (πΎβ{π}) = (πΎβ{π}))) | ||
Theorem | lbslsp 33032* | Any element of a left module π can be expressed as a linear combination of the elements of a basis π of π. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β (LBasisβπ)) β β’ (π β (π β π΅ β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
Theorem | lindssn 33033 | Any singleton of a nonzero element is an independent set. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
β’ π΅ = (Baseβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π β π΅ β§ π β 0 ) β {π} β (LIndSβπ)) | ||
Theorem | lindflbs 33034 | Conditions for an independent family to be a basis. (Contributed by Thierry Arnoux, 21-Jul-2023.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (BaseβπΉ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β NzRing) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβ1-1βπ΅) β β’ (π β (ran πΉ β (LBasisβπ) β (πΉ LIndF π β§ (πβran πΉ) = π΅))) | ||
Theorem | islbs5 33035* | An equivalent formulation of the basis predicate in a vector space, using a function πΉ for generating the base. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ Β· = ( Β·π βπ) & β’ π = (0gβπ) & β’ 0 = (0gβπ) & β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ (π β π β LMod) & β’ (π β π β NzRing) & β’ (π β πΌ β π) & β’ (π β πΉ:πΌβ1-1βπ΅) β β’ (π β (ran πΉ β (LBasisβπ) β (βπ β (πΎ βm πΌ)((π finSupp 0 β§ (π Ξ£g (π βf Β· πΉ)) = π) β π = (πΌ Γ { 0 })) β§ (πβran πΉ) = π΅))) | ||
Theorem | linds2eq 33036 | Deduce equality of elements in an independent set. (Contributed by Thierry Arnoux, 18-Jul-2023.) |
β’ πΉ = (Baseβ(Scalarβπ)) & β’ Β· = ( Β·π βπ) & β’ + = (+gβπ) & β’ 0 = (0gβ(Scalarβπ)) & β’ (π β π β LVec) & β’ (π β π΅ β (LIndSβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΎ β πΉ) & β’ (π β πΏ β πΉ) & β’ (π β πΎ β 0 ) & β’ (π β (πΎ Β· π) = (πΏ Β· π)) β β’ (π β (π = π β§ πΎ = πΏ)) | ||
Theorem | lindfpropd 33037* | Property deduction for linearly independent families. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΏ))) & β’ (π β (0gβ(ScalarβπΎ)) = (0gβ(ScalarβπΏ))) & β’ ((π β§ (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ))) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) β (BaseβπΎ)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β π β π΄) β β’ (π β (π LIndF πΎ β π LIndF πΏ)) | ||
Theorem | lindspropd 33038* | Property deduction for linearly independent sets. (Contributed by Thierry Arnoux, 16-Jul-2023.) |
β’ (π β (BaseβπΎ) = (BaseβπΏ)) & β’ (π β (Baseβ(ScalarβπΎ)) = (Baseβ(ScalarβπΏ))) & β’ (π β (0gβ(ScalarβπΎ)) = (0gβ(ScalarβπΏ))) & β’ ((π β§ (π₯ β (BaseβπΎ) β§ π¦ β (BaseβπΎ))) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) β (BaseβπΎ)) & β’ ((π β§ (π₯ β (Baseβ(ScalarβπΎ)) β§ π¦ β (BaseβπΎ))) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ (π β πΎ β π) & β’ (π β πΏ β π) β β’ (π β (LIndSβπΎ) = (LIndSβπΏ)) | ||
The sumset (also called the Minkowski sum) of two subsets π΄ and π΅, is defined to be the set of all sums of an element from π΄ with an element from π΅. The sumset operation can be used for both group (additive) operations and ring (multiplicative) operations. | ||
Theorem | elgrplsmsn 33039* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β πΊ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π΄ β {π}) β βπ₯ β π΄ π = (π₯ + π))) | ||
Theorem | lsmsnorb 33040* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19249. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π + π₯) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π΄ β {π}) = [π] βΌ ) | ||
Theorem | lsmsnorb2 33041* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19249. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π₯ + π) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β ({π} β π΄) = [π] βΌ ) | ||
Theorem | elringlsm 33042* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (π β (πΈ Γ πΉ) β βπ₯ β πΈ βπ¦ β πΉ π = (π₯ Β· π¦))) | ||
Theorem | elringlsmd 33043 | Membership in a product of two subsets of a ring, one direction. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) & β’ (π β π β πΈ) & β’ (π β π β πΉ) β β’ (π β (π Β· π) β (πΈ Γ πΉ)) | ||
Theorem | ringlsmss 33044 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (πΈ Γ πΉ) β π΅) | ||
Theorem | ringlsmss1 33045 | The product of an ideal πΌ of a commutative ring π with some set E is a subset of the ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β CRing) & β’ (π β πΈ β π΅) & β’ (π β πΌ β (LIdealβπ )) β β’ (π β (πΌ Γ πΈ) β πΌ) | ||
Theorem | ringlsmss2 33046 | The product with an ideal of a ring is a subset of that ideal. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΌ β (LIdealβπ )) β β’ (π β (πΈ Γ πΌ) β πΌ) | ||
Theorem | lsmsnpridl 33047 | The product of the ring with a single element is equal to the principal ideal generated by that element. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π΅ Γ {π}) = (πΎβ{π})) | ||
Theorem | lsmsnidl 33048 | The product of the ring with a single element is a principal ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π΅ Γ {π}) β (LPIdealβπ )) | ||
Theorem | lsmidllsp 33049 | The sum of two ideals is the ideal generated by their union. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π½ β (LIdealβπ )) β β’ (π β (πΌ β π½) = (πΎβ(πΌ βͺ π½))) | ||
Theorem | lsmidl 33050 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π½ β (LIdealβπ )) β β’ (π β (πΌ β π½) β (LIdealβπ )) | ||
Theorem | lsmssass 33051 | Group sum is associative, subset version (see lsmass 19615). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ β = (LSSumβπΊ) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β π) = (π β (π β π))) | ||
Theorem | grplsm0l 33052 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π΅ β§ π΄ β β ) β ({ 0 } β π΄) = π΄) | ||
Theorem | grplsmid 33053 | The direct sum of an element π of a subgroup π΄ is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ β = (LSSumβπΊ) β β’ ((π΄ β (SubGrpβπΊ) β§ π β π΄) β ({π} β π΄) = π΄) | ||
Theorem | qusmul 33054 | Value of the ring operation in a quotient ring. (Contributed by Thierry Arnoux, 1-Sep-2024.) |
β’ π = (π /s (π ~QG πΌ)) & β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ Γ = (.rβπ) & β’ (π β π β CRing) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ([π](π ~QG πΌ) Γ [π](π ~QG πΌ)) = [(π Β· π)](π ~QG πΌ)) | ||
Theorem | quslsm 33055 | Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β π΅) β β’ (π β [π](πΊ ~QG π) = ({π} β π)) | ||
Theorem | qusbas2 33056* | Alternate definition of the group quotient set, as the set of all cosets of the form ({π₯} β π). (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ ((π β§ π₯ β π΅) β π β (SubGrpβπΊ)) β β’ (π β (π΅ / (πΊ ~QG π)) = ran (π₯ β π΅ β¦ ({π₯} β π))) | ||
Theorem | qus0g 33057 | The identity element of a quotient group. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (πΊ /s (πΊ ~QG π)) β β’ (π β (NrmSGrpβπΊ) β (0gβπ) = π) | ||
Theorem | qusima 33058* | The image of a subgroup by the natural map from elements to their cosets. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) & β’ (π β π β (NrmSGrpβπΊ)) & β’ (π β π» β π) & β’ (π β π β (SubGrpβπΊ)) β β’ (π β (πΈβπ») = (πΉ β π»)) | ||
Theorem | qusrn 33059* | The natural map from elements to their cosets is surjective. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (BaseβπΊ) & β’ π = (π΅ / (πΊ ~QG π)) & β’ πΉ = (π₯ β π΅ β¦ [π₯](πΊ ~QG π)) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΉ = π) | ||
Theorem | nsgqus0 33060 | A normal subgroup π is a member of all subgroups πΉ of the quotient group by π. In fact, it is the identity element of the quotient group. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π = (πΊ /s (πΊ ~QG π)) β β’ ((π β (NrmSGrpβπΊ) β§ πΉ β (SubGrpβπ)) β π β πΉ) | ||
Theorem | nsgmgclem 33061* | Lemma for nsgmgc 33062. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ (π β π β (NrmSGrpβπΊ)) & β’ (π β πΉ β (SubGrpβπ)) β β’ (π β {π β π΅ β£ ({π} β π) β πΉ} β (SubGrpβπΊ)) | ||
Theorem | nsgmgc 33062* | There is a monotone Galois connection between the lattice of subgroups of a group πΊ containing a normal subgroup π and the lattice of subgroups of the quotient group πΊ / π. This is sometimes called the lattice theorem. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ π½ = (πMGalConnπ) & β’ π = (toIncβπ) & β’ π = (toIncβπ) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β πΈπ½πΉ) | ||
Theorem | nsgqusf1olem1 33063* | Lemma for nsgqusf1o 33066. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) | ||
Theorem | nsgqusf1olem2 33064* | Lemma for nsgqusf1o 33066. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΈ = π) | ||
Theorem | nsgqusf1olem3 33065* | Lemma for nsgqusf1o 33066. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΉ = π) | ||
Theorem | nsgqusf1o 33066* | The canonical projection homomorphism πΈ defines a bijective correspondence between the set π of subgroups of πΊ containing a normal subgroup π and the subgroups of the quotient group πΊ / π. This theorem is sometimes called the correspondence theorem, or the fourth isomorphism theorem. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β πΈ:πβ1-1-ontoβπ) | ||
Theorem | lmhmqusker 33067* | A surjective module homomorphism πΉ from πΊ to π» induces an isomorphism π½ from π to π», where π is the factor group of πΊ by πΉ's kernel πΎ. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ 0 = (0gβπ») & β’ (π β πΉ β (πΊ LMHom π»)) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (πΊ /s (πΊ ~QG πΎ)) & β’ (π β ran πΉ = (Baseβπ»)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΉ β π)) β β’ (π β π½ β (π LMIso π»)) | ||
Theorem | lmicqusker 33068 | The image π» of a module homomorphism πΉ is isomorphic with the quotient module π over πΉ's kernel πΎ. This is part of what is sometimes called the first isomorphism theorem for modules. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
β’ 0 = (0gβπ») & β’ (π β πΉ β (πΊ LMHom π»)) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (πΊ /s (πΊ ~QG πΎ)) & β’ (π β ran πΉ = (Baseβπ»)) β β’ (π β π βπ π») | ||
Theorem | intlidl 33069 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
β’ ((π β Ring β§ πΆ β β β§ πΆ β (LIdealβπ )) β β© πΆ β (LIdealβπ )) | ||
Theorem | rhmpreimaidl 33070 | The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ πΌ = (LIdealβπ ) β β’ ((πΉ β (π RingHom π) β§ π½ β (LIdealβπ)) β (β‘πΉ β π½) β πΌ) | ||
Theorem | kerlidl 33071 | The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ πΌ = (LIdealβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π RingHom π) β (β‘πΉ β { 0 }) β πΌ) | ||
Theorem | 0ringidl 33072 | The zero ideal is the only ideal of the trivial ring. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β (LIdealβπ ) = {{ 0 }}) | ||
Theorem | pidlnzb 33073 | A principal ideal is nonzero iff it is generated by a nonzero elements (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅) β (π β 0 β (πΎβ{π}) β { 0 })) | ||
Theorem | lidlunitel 33074 | If an ideal πΌ contains a unit π½, then it is the whole ring. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ (π β π½ β π) & β’ (π β π½ β πΌ) & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) β β’ (π β πΌ = π΅) | ||
Theorem | unitpidl1 33075 | The ideal πΌ generated by an element π of an integral domain π is the unit ideal π΅ iff π is a ring unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (Unitβπ ) & β’ πΎ = (RSpanβπ ) & β’ πΌ = (πΎβ{π}) & β’ π΅ = (Baseβπ ) & β’ (π β π β π΅) & β’ (π β π β IDomn) β β’ (π β (πΌ = π΅ β π β π)) | ||
Theorem | rhmquskerlem 33076* | The mapping π½ induced by a ring homomorphism πΉ from the quotient group π over πΉ's kernel πΎ is a ring homomorphism. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ 0 = (0gβπ») & β’ (π β πΉ β (πΊ RingHom π»)) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (πΊ /s (πΊ ~QG πΎ)) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΉ β π)) & β’ (π β πΊ β CRing) β β’ (π β π½ β (π RingHom π»)) | ||
Theorem | rhmqusker 33077* | A surjective ring homomorphism πΉ from πΊ to π» induces an isomorphism π½ from π to π», where π is the factor group of πΊ by πΉ's kernel πΎ. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ 0 = (0gβπ») & β’ (π β πΉ β (πΊ RingHom π»)) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (πΊ /s (πΊ ~QG πΎ)) & β’ (π β ran πΉ = (Baseβπ»)) & β’ (π β πΊ β CRing) & β’ π½ = (π β (Baseβπ) β¦ βͺ (πΉ β π)) β β’ (π β π½ β (π RingIso π»)) | ||
Theorem | ricqusker 33078 | The image π» of a ring homomorphism πΉ is isomorphic with the quotient ring π over πΉ's kernel πΎ. This a part of what is sometimes called the first isomorphism theorem for rings. (Contributed by Thierry Arnoux, 10-Mar-2025.) |
β’ 0 = (0gβπ») & β’ (π β πΉ β (πΊ RingHom π»)) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (πΊ /s (πΊ ~QG πΎ)) & β’ (π β ran πΉ = (Baseβπ»)) & β’ (π β πΊ β CRing) β β’ (π β π βπ π») | ||
Theorem | elrspunidl 33079* | Elementhood in the span of a union of ideals. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ π = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β π β (LIdealβπ )) β β’ (π β (π β (πββͺ π) β βπ β (π΅ βm π)(π finSupp 0 β§ π = (π Ξ£g π) β§ βπ β π (πβπ) β π))) | ||
Theorem | elrspunsn 33080* | Membership to the span of an ideal π and a single element π. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π = (RSpanβπ ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ + = (+gβπ ) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π β (π΅ β πΌ)) β β’ (π β (π΄ β (πβ(πΌ βͺ {π})) β βπ β π΅ βπ β πΌ π΄ = ((π Β· π) + π))) | ||
Theorem | lidlincl 33081 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π½ β π) β (πΌ β© π½) β π) | ||
Theorem | idlinsubrg 33082 | The intersection between an ideal and a subring is an ideal of the subring. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
β’ π = (π βΎs π΄) & β’ π = (LIdealβπ ) & β’ π = (LIdealβπ) β β’ ((π΄ β (SubRingβπ ) β§ πΌ β π) β (πΌ β© π΄) β π) | ||
Theorem | rhmimaidl 33083 | The image of an ideal πΌ by a surjective ring homomorphism πΉ is an ideal. (Contributed by Thierry Arnoux, 6-Jul-2024.) |
β’ π΅ = (Baseβπ) & β’ π = (LIdealβπ ) & β’ π = (LIdealβπ) β β’ ((πΉ β (π RingHom π) β§ ran πΉ = π΅ β§ πΌ β π) β (πΉ β πΌ) β π) | ||
Theorem | drngidl 33084 | A nonzero ring is a division ring if and only if its only left ideals are the zero ideal and the unit ideal. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ π = (LIdealβπ ) β β’ (π β NzRing β (π β DivRing β π = {{ 0 }, π΅})) | ||
Theorem | drngidlhash 33085 | A ring is a division ring if and only if it admits exactly two ideals. (Proposed by Gerard Lang, 13-Mar-2025.) (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (LIdealβπ ) β β’ (π β Ring β (π β DivRing β (β―βπ) = 2)) | ||
Syntax | cprmidl 33086 | Extend class notation with the class of prime ideals. |
class PrmIdeal | ||
Definition | df-prmidl 33087* | Define the class of prime ideals of a ring π . A proper ideal πΌ of π is prime if whenever π΄π΅ β πΌ for ideals π΄ and π΅, either π΄ β πΌ or π΅ β πΌ. The more familiar definition using elements rather than ideals is equivalent provided π is commutative; see prmidl2 33092 and isprmidlc 33099. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
β’ PrmIdeal = (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Theorem | prmidlval 33088* | The class of prime ideals of a ring π . (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (PrmIdealβπ ) = {π β (LIdealβπ ) β£ (π β π΅ β§ βπ β (LIdealβπ )βπ β (LIdealβπ )(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π)))}) | ||
Theorem | isprmidl 33089* | The predicate "is a prime ideal". (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β Ring β (π β (PrmIdealβπ ) β (π β (LIdealβπ ) β§ π β π΅ β§ βπ β (LIdealβπ )βπ β (LIdealβπ )(βπ₯ β π βπ¦ β π (π₯ Β· π¦) β π β (π β π β¨ π β π))))) | ||
Theorem | prmidlnr 33090 | A prime ideal is a proper ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β Ring β§ π β (PrmIdealβπ )) β π β π΅) | ||
Theorem | prmidl 33091* | The main property of a prime ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((((π β Ring β§ π β (PrmIdealβπ )) β§ (πΌ β (LIdealβπ ) β§ π½ β (LIdealβπ ))) β§ βπ₯ β πΌ βπ¦ β π½ (π₯ Β· π¦) β π) β (πΌ β π β¨ π½ β π)) | ||
Theorem | prmidl2 33092* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 37478 for the equivalence in the commutative case. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (((π β Ring β§ π β (LIdealβπ )) β§ (π β π΅ β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) β π β (π₯ β π β¨ π¦ β π)))) β π β (PrmIdealβπ )) | ||
Theorem | idlmulssprm 33093 | Let π be a prime ideal containing the product (πΌ Γ π½) of two ideals πΌ and π½. Then πΌ β π or π½ β π. (Contributed by Thierry Arnoux, 13-Apr-2024.) |
β’ Γ = (LSSumβ(mulGrpβπ )) & β’ (π β π β Ring) & β’ (π β π β (PrmIdealβπ )) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π½ β (LIdealβπ )) & β’ (π β (πΌ Γ π½) β π) β β’ (π β (πΌ β π β¨ π½ β π)) | ||
Theorem | pridln1 33094 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β (LIdealβπ ) β§ πΌ β π΅) β Β¬ 1 β πΌ) | ||
Theorem | prmidlidl 33095 | A prime ideal is an ideal. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ ((π β Ring β§ π β (PrmIdealβπ )) β π β (LIdealβπ )) | ||
Theorem | prmidlssidl 33096 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ (π β Ring β (PrmIdealβπ ) β (LIdealβπ )) | ||
Theorem | lidlnsg 33097 | An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ ((π β Ring β§ πΌ β (LIdealβπ )) β πΌ β (NrmSGrpβπ )) | ||
Theorem | cringm4 33098 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π Β· π) Β· (π Β· π)) = ((π Β· π) Β· (π Β· π))) | ||
Theorem | isprmidlc 33099* | The predicate "is prime ideal" for commutative rings. Alternate definition for commutative rings. See definition in [Lang] p. 92. (Contributed by Jeff Madsen, 19-Jun-2010.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (π β CRing β (π β (PrmIdealβπ ) β (π β (LIdealβπ ) β§ π β π΅ β§ βπ₯ β π΅ βπ¦ β π΅ ((π₯ Β· π¦) β π β (π₯ β π β¨ π¦ β π))))) | ||
Theorem | prmidlc 33100 | Property of a prime ideal in a commutative ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 12-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ (((π β CRing β§ π β (PrmIdealβπ )) β§ (πΌ β π΅ β§ π½ β π΅ β§ (πΌ Β· π½) β π)) β (πΌ β π β¨ π½ β π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |