Home | Metamath
Proof Explorer Theorem List (p. 320 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 | resvval2 31901 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) | ||
Theorem | resvsca 31902 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ )) | ||
Theorem | resvlem 31903 | Other elements of a scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot (πΈβndx) & β’ (πΈβndx) β (Scalarβndx) β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | resvlemOLD 31904 | Obsolete version of resvlem 31903 as of 31-Oct-2024. Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (π βΎv π΄) & β’ πΆ = (πΈβπ) & β’ πΈ = Slot π & β’ π β β & β’ π β 5 β β’ (π΄ β π β πΆ = (πΈβπ )) | ||
Theorem | resvbas 31905 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
Theorem | resvbasOLD 31906 | Obsolete proof of resvbas 31905 as of 31-Oct-2024. Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
Theorem | resvplusg 31907 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
Theorem | resvplusgOLD 31908 | Obsolete proof of resvplusg 31907 as of 31-Oct-2024. +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
Theorem | resvvsca 31909 | Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
Theorem | resvvscaOLD 31910 | Obsolete proof of resvvsca 31909 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
Theorem | resvmulr 31911 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
Theorem | resvmulrOLD 31912 | Obsolete proof of resvmulr 31911 as of 31-Oct-2024. Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
Theorem | resv0g 31913 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β 0 = (0gβπ»)) | ||
Theorem | resv1r 31914 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 1 = (1rβπΊ) β β’ (π΄ β π β 1 = (1rβπ»)) | ||
Theorem | resvcmn 31915 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) β β’ (π΄ β π β (πΊ β CMnd β π» β CMnd)) | ||
Theorem | gzcrng 31916 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
β’ (βfld βΎs β€[i]) β CRing | ||
Theorem | reofld 31917 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β oField | ||
Theorem | nn0omnd 31918 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (βfld βΎs β0) β oMnd | ||
Theorem | rearchi 31919 | The field of the real numbers is Archimedean. See also arch 12344. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ βfld β Archi | ||
Theorem | nn0archi 31920 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
β’ (βfld βΎs β0) β Archi | ||
Theorem | xrge0slmod 31921 | The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ πΊ = (β*π βΎs (0[,]+β)) & β’ π = (πΊ βΎv (0[,)+β)) β β’ π β SLMod | ||
Theorem | qusker 31922* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) & β’ π = (π /s (π ~QG πΊ)) & β’ 0 = (0gβπ) β β’ (πΊ β (NrmSGrpβπ) β (β‘πΉ β { 0 }) = πΊ) | ||
Theorem | eqgvscpbl 31923 | 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 31924* | 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 | qusscaval 31925 | 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 31926* | 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 | quslmod 31927 | 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 31928* | 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 | ecxpid 31929 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ (π β π΄ β [π](π΄ Γ π΄) = π΄) | ||
Theorem | eqg0el 31930 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ βΌ = (πΊ ~QG π») β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ)) β ([π] βΌ = π» β π β π»)) | ||
Theorem | qsxpid 31931 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ (π΄ β β β (π΄ / (π΄ Γ π΄)) = {π΄}) | ||
Theorem | qusxpid 31932 | 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 31933 | The quotient of a group πΊ by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π΅)) β β’ (πΊ β Grp β (Baseβπ) = {π΅}) | ||
Theorem | qustrivr 31934 | Converse of qustriv 31933. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π»)) β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ) β§ (Baseβπ) = {π»}) β π» = π΅) | ||
Theorem | fermltlchr 31935 | A generalization of Fermat's little theorem in a commutative ring πΉ of prime characteristic. See fermltl 16591. (Contributed by Thierry Arnoux, 9-Jan-2024.) |
β’ π = (chrβπΉ) & β’ π΅ = (BaseβπΉ) & β’ β = (.gβ(mulGrpβπΉ)) & β’ π΄ = ((β€RHomβπΉ)βπΈ) & β’ (π β π β β) & β’ (π β πΈ β β€) & β’ (π β πΉ β CRing) β β’ (π β (π β π΄) = π΄) | ||
Theorem | znfermltl 31936 | Fermat's little theorem in β€/nβ€. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβ(mulGrpβπ)) β β’ ((π β β β§ π΄ β π΅) β (π β π΄) = π΄) | ||
Theorem | islinds5 31937* | 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 31938* | Variation on ellspd 21131. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β π΅) β β’ (π β (π β (πβπ) β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
Theorem | 0ellsp 31939 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π΅) β 0 β (πβπ)) | ||
Theorem | 0nellinds 31940 | 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 31941* | Membership in a principal ideal. Analogous to lspsnel 20387. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅) β (πΌ β (πΎβ{π}) β βπ₯ β π΅ πΌ = (π₯ Β· π))) | ||
Theorem | rspsnid 31942 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβ{πΊ})) | ||
Theorem | elrsp 31943* | 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 31944 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ πΎ = (RSpanβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΎβπΌ) = πΌ) | ||
Theorem | pidlnz 31945 | 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 | lbslsp 31946* | 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 31947 | 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 31948 | 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 | linds2eq 31949 | 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 31950* | 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 31951* | 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 31952* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β πΊ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π΄ β {π}) β βπ₯ β π΄ π = (π₯ + π))) | ||
Theorem | lsmsnorb 31953* | The sumset of a group with a single element is the element's orbit by the group action. See gaorb 19019. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π + π₯) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π΄ β {π}) = [π] βΌ ) | ||
Theorem | lsmsnorb2 31954* | The sumset of a single element with a group is the element's orbit by the group action. See gaorb 19019. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ βΌ = {β¨π₯, π¦β© β£ ({π₯, π¦} β π΅ β§ βπ β π΄ (π₯ + π) = π¦)} & β’ (π β πΊ β Mnd) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β ({π} β π΄) = [π] βΌ ) | ||
Theorem | elringlsm 31955* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (π β (πΈ Γ πΉ) β βπ₯ β πΈ βπ¦ β πΉ π = (π₯ Β· π¦))) | ||
Theorem | elringlsmd 31956 | 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 31957 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (πΈ Γ πΉ) β π΅) | ||
Theorem | ringlsmss1 31958 | 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 31959 | 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 31960 | 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 31961 | 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 31962 | 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 31963 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π½ β (LIdealβπ )) β β’ (π β (πΌ β π½) β (LIdealβπ )) | ||
Theorem | lsmssass 31964 | Group sum is associative, subset version (see lsmass 19380). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ β = (LSSumβπΊ) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β π) = (π β (π β π))) | ||
Theorem | grplsm0l 31965 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π΅ β§ π΄ β β ) β ({ 0 } β π΄) = π΄) | ||
Theorem | grplsmid 31966 | The direct sum of an element π of a subgroup π΄ is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ β = (LSSumβπΊ) β β’ ((π΄ β (SubGrpβπΊ) β§ π β π΄) β ({π} β π΄) = π΄) | ||
Theorem | quslsm 31967 | Express the image by the quotient map in terms of direct sum. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β π β (SubGrpβπΊ)) & β’ (π β π β π΅) β β’ (π β [π](πΊ ~QG π) = ({π} β π)) | ||
Theorem | qusima 31968* | 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 | nsgqus0 31969 | 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 31970* | Lemma for nsgmgc 31971. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ (π β π β (NrmSGrpβπΊ)) & β’ (π β πΉ β (SubGrpβπ)) β β’ (π β {π β π΅ β£ ({π} β π) β πΉ} β (SubGrpβπΊ)) | ||
Theorem | nsgmgc 31971* | 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 31972* | Lemma for nsgqusf1o 31975. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) | ||
Theorem | nsgqusf1olem2 31973* | Lemma for nsgqusf1o 31975. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΈ = π) | ||
Theorem | nsgqusf1olem3 31974* | Lemma for nsgqusf1o 31975. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΉ = π) | ||
Theorem | nsgqusf1o 31975* | 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 | intlidl 31976 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
β’ ((π β Ring β§ πΆ β β β§ πΆ β (LIdealβπ )) β β© πΆ β (LIdealβπ )) | ||
Theorem | rhmpreimaidl 31977 | The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ πΌ = (LIdealβπ ) β β’ ((πΉ β (π RingHom π) β§ π½ β (LIdealβπ)) β (β‘πΉ β π½) β πΌ) | ||
Theorem | kerlidl 31978 | The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ πΌ = (LIdealβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π RingHom π) β (β‘πΉ β { 0 }) β πΌ) | ||
Theorem | 0ringidl 31979 | 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 | elrspunidl 31980* | Elementhood to 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 | lidlincl 31981 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π½ β π) β (πΌ β© π½) β π) | ||
Theorem | idlinsubrg 31982 | 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 31983 | 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 πΉ = π΅ β§ πΌ β π) β (πΉ β πΌ) β π) | ||
Syntax | cprmidl 31984 | Extend class notation with the class of prime ideals. |
class PrmIdeal | ||
Definition | df-prmidl 31985* | 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 31990 and isprmidlc 31997. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
β’ PrmIdeal = (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Theorem | prmidlval 31986* | 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 31987* | 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 31988 | 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 31989* | 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 31990* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 36415 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 31991 | 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 31992 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β (LIdealβπ ) β§ πΌ β π΅) β Β¬ 1 β πΌ) | ||
Theorem | prmidlidl 31993 | 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 31994 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ (π β Ring β (PrmIdealβπ ) β (LIdealβπ )) | ||
Theorem | lidlnsg 31995 | An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ ((π β Ring β§ πΌ β (LIdealβπ )) β πΌ β (NrmSGrpβπ )) | ||
Theorem | cringm4 31996 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π Β· π) Β· (π Β· π)) = ((π Β· π) Β· (π Β· π))) | ||
Theorem | isprmidlc 31997* | 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 31998 | 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βπ )) β§ (πΌ β π΅ β§ π½ β π΅ β§ (πΌ Β· π½) β π)) β (πΌ β π β¨ π½ β π)) | ||
Theorem | 0ringprmidl 31999 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β (PrmIdealβπ ) = β ) | ||
Theorem | prmidl0 32000 | The zero ideal of a commutative ring π is a prime ideal if and only if π is an integral domain. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ 0 = (0gβπ ) β β’ ((π β CRing β§ { 0 } β (PrmIdealβπ )) β π β IDomn) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |