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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ofldlt1 31901 | In an ordered field, the ring unity is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ 0 = (0gβπΉ) & β’ 1 = (1rβπΉ) & β’ < = (ltβπΉ) β β’ (πΉ β oField β 0 < 1 ) | ||
Theorem | ofldchr 31902 | The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.) |
β’ (πΉ β oField β (chrβπΉ) = 0) | ||
Theorem | suborng 31903 | Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ ((π β oRing β§ (π βΎs π΄) β Ring) β (π βΎs π΄) β oRing) | ||
Theorem | subofld 31904 | Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ ((πΉ β oField β§ (πΉ βΎs π΄) β Field) β (πΉ βΎs π΄) β oField) | ||
Theorem | isarchiofld 31905* | Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ π΅ = (Baseβπ) & β’ π» = (β€RHomβπ) & β’ < = (ltβπ) β β’ (π β oField β (π β Archi β βπ₯ β π΅ βπ β β π₯ < (π»βπ))) | ||
Theorem | rhmdvd 31906 | A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.) |
β’ π = (Unitβπ) & β’ π = (Baseβπ ) & β’ / = (/rβπ) & β’ Β· = (.rβπ ) β β’ ((πΉ β (π RingHom π) β§ (π΄ β π β§ π΅ β π β§ πΆ β π) β§ ((πΉβπ΅) β π β§ (πΉβπΆ) β π)) β ((πΉβπ΄) / (πΉβπ΅)) = ((πΉβ(π΄ Β· πΆ)) / (πΉβ(π΅ Β· πΆ)))) | ||
Theorem | kerunit 31907 | If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.) |
β’ π = (Unitβπ ) & β’ 0 = (0gβπ) & β’ 1 = (1rβπ) β β’ ((πΉ β (π RingHom π) β§ (π β© (β‘πΉ β { 0 })) β β ) β 1 = 0 ) | ||
Syntax | cresv 31908 | Extend class notation with the scalar restriction operation. |
class βΎv | ||
Definition | df-resv 31909* | Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.) |
β’ βΎv = (π€ β V, π₯ β V β¦ if((Baseβ(Scalarβπ€)) β π₯, π€, (π€ sSet β¨(Scalarβndx), ((Scalarβπ€) βΎs π₯)β©))) | ||
Theorem | reldmresv 31910 | The scalar restriction is a proper operator, so it can be used with ovprc1 7388. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ Rel dom βΎv | ||
Theorem | resvval 31911 | Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π β π β§ π΄ β π) β π = if(π΅ β π΄, π, (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©))) | ||
Theorem | resvid2 31912 | General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((π΅ β π΄ β§ π β π β§ π΄ β π) β π = π) | ||
Theorem | resvval2 31913 | Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ ((Β¬ π΅ β π΄ β§ π β π β§ π΄ β π) β π = (π sSet β¨(Scalarβndx), (πΉ βΎs π΄)β©)) | ||
Theorem | resvsca 31914 | Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π = (π βΎv π΄) & β’ πΉ = (Scalarβπ) & β’ π΅ = (BaseβπΉ) β β’ (π΄ β π β (πΉ βΎs π΄) = (Scalarβπ )) | ||
Theorem | resvlem 31915 | 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 31916 | Obsolete version of resvlem 31915 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 31917 | Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ π΅ = (BaseβπΊ) β β’ (π΄ β π β π΅ = (Baseβπ»)) | ||
Theorem | resvbasOLD 31918 | Obsolete proof of resvbas 31917 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 31919 | +g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ + = (+gβπΊ) β β’ (π΄ β π β + = (+gβπ»)) | ||
Theorem | resvplusgOLD 31920 | Obsolete proof of resvplusg 31919 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 31921 | Β·π is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Proof shortened by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = ( Β·π βπΊ) β β’ (π΄ β π β Β· = ( Β·π βπ»)) | ||
Theorem | resvvscaOLD 31922 | Obsolete proof of resvvsca 31921 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 31923 | .r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) (Revised by AV, 31-Oct-2024.) |
β’ π» = (πΊ βΎv π΄) & β’ Β· = (.rβπΊ) β β’ (π΄ β π β Β· = (.rβπ»)) | ||
Theorem | resvmulrOLD 31924 | Obsolete proof of resvmulr 31923 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 31925 | 0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 0 = (0gβπΊ) β β’ (π΄ β π β 0 = (0gβπ»)) | ||
Theorem | resv1r 31926 | 1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) & β’ 1 = (1rβπΊ) β β’ (π΄ β π β 1 = (1rβπ»)) | ||
Theorem | resvcmn 31927 | Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.) |
β’ π» = (πΊ βΎv π΄) β β’ (π΄ β π β (πΊ β CMnd β π» β CMnd)) | ||
Theorem | gzcrng 31928 | The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.) |
β’ (βfld βΎs β€[i]) β CRing | ||
Theorem | reofld 31929 | The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.) |
β’ βfld β oField | ||
Theorem | nn0omnd 31930 | The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.) |
β’ (βfld βΎs β0) β oMnd | ||
Theorem | rearchi 31931 | The field of the real numbers is Archimedean. See also arch 12343. (Contributed by Thierry Arnoux, 9-Apr-2018.) |
β’ βfld β Archi | ||
Theorem | nn0archi 31932 | The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.) |
β’ (βfld βΎs β0) β Archi | ||
Theorem | xrge0slmod 31933 | 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 31934* | The kernel of a quotient map. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ πΉ = (π₯ β π β¦ [π₯](π ~QG πΊ)) & β’ π = (π /s (π ~QG πΊ)) & β’ 0 = (0gβπ) β β’ (πΊ β (NrmSGrpβπ) β (β‘πΉ β { 0 }) = πΊ) | ||
Theorem | eqgvscpbl 31935 | 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 31936* | 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 31937 | 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 31938* | 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 31939 | 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 31940* | 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 31941 | The equivalence class of a cartesian product is the whole set. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ (π β π΄ β [π](π΄ Γ π΄) = π΄) | ||
Theorem | eqg0el 31942 | Equivalence class of a quotient group for a subgroup. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ βΌ = (πΊ ~QG π») β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ)) β ([π] βΌ = π» β π β π»)) | ||
Theorem | qsxpid 31943 | The quotient set of a cartesian product is trivial. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ (π΄ β β β (π΄ / (π΄ Γ π΄)) = {π΄}) | ||
Theorem | qusxpid 31944 | 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 31945 | The quotient of a group πΊ by itself is trivial. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π΅)) β β’ (πΊ β Grp β (Baseβπ) = {π΅}) | ||
Theorem | qustrivr 31946 | Converse of qustriv 31945. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π»)) β β’ ((πΊ β Grp β§ π» β (SubGrpβπΊ) β§ (Baseβπ) = {π»}) β π» = π΅) | ||
Theorem | fermltlchr 31947 | A generalization of Fermat's little theorem in a commutative ring πΉ of prime characteristic. See fermltl 16590. (Contributed by Thierry Arnoux, 9-Jan-2024.) |
β’ π = (chrβπΉ) & β’ π΅ = (BaseβπΉ) & β’ β = (.gβ(mulGrpβπΉ)) & β’ π΄ = ((β€RHomβπΉ)βπΈ) & β’ (π β π β β) & β’ (π β πΈ β β€) & β’ (π β πΉ β CRing) β β’ (π β (π β π΄) = π΄) | ||
Theorem | znfermltl 31948 | Fermat's little theorem in β€/nβ€. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (β€/nβ€βπ) & β’ π΅ = (Baseβπ) & β’ β = (.gβ(mulGrpβπ)) β β’ ((π β β β§ π΄ β π΅) β (π β π΄) = π΄) | ||
Theorem | islinds5 31949* | 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 31950* | Variation on ellspd 21131. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ π = (LSpanβπ) & β’ π΅ = (Baseβπ) & β’ πΎ = (Baseβπ) & β’ π = (Scalarβπ) & β’ 0 = (0gβπ) & β’ Β· = ( Β·π βπ) & β’ (π β π β LMod) & β’ (π β π β π΅) β β’ (π β (π β (πβπ) β βπ β (πΎ βm π)(π finSupp 0 β§ π = (π Ξ£g (π£ β π β¦ ((πβπ£) Β· π£)))))) | ||
Theorem | 0ellsp 31951 | Zero is in all spans. (Contributed by Thierry Arnoux, 8-May-2023.) |
β’ 0 = (0gβπ) & β’ π΅ = (Baseβπ) & β’ π = (LSpanβπ) β β’ ((π β LMod β§ π β π΅) β 0 β (πβπ)) | ||
Theorem | 0nellinds 31952 | 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 31953* | Membership in a principal ideal. Analogous to lspsnel 20387. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ π β π΅) β (πΌ β (πΎβ{π}) β βπ₯ β π΅ πΌ = (π₯ Β· π))) | ||
Theorem | rspsnid 31954 | A principal ideal contains the element that generates it. (Contributed by Thierry Arnoux, 15-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΎ = (RSpanβπ ) β β’ ((π β Ring β§ πΊ β π΅) β πΊ β (πΎβ{πΊ})) | ||
Theorem | elrsp 31955* | 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 31956 | The ideal span of an ideal is the ideal itself. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ πΎ = (RSpanβπ ) & β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π) β (πΎβπΌ) = πΌ) | ||
Theorem | pidlnz 31957 | 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 31958* | 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 31959 | 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 31960 | 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 31961 | 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 31962* | 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 31963* | 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 31964* | Membership in a sumset with a singleton for a group operation. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (BaseβπΊ) & β’ + = (+gβπΊ) & β’ β = (LSSumβπΊ) & β’ (π β πΊ β π) & β’ (π β π΄ β π΅) & β’ (π β π β π΅) β β’ (π β (π β (π΄ β {π}) β βπ₯ β π΄ π = (π₯ + π))) | ||
Theorem | lsmsnorb 31965* | 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 31966* | 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 31967* | Membership in a product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (π β (πΈ Γ πΉ) β βπ₯ β πΈ βπ¦ β πΉ π = (π₯ Β· π¦))) | ||
Theorem | elringlsmd 31968 | 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 31969 | Closure of the product of two subsets of a ring. (Contributed by Thierry Arnoux, 20-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ πΊ = (mulGrpβπ ) & β’ Γ = (LSSumβπΊ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β (πΈ Γ πΉ) β π΅) | ||
Theorem | ringlsmss1 31970 | 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 31971 | 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 31972 | 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 31973 | 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 31974 | 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 31975 | The sum of two ideals is an ideal. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ β = (LSSumβπ ) & β’ πΎ = (RSpanβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β π½ β (LIdealβπ )) β β’ (π β (πΌ β π½) β (LIdealβπ )) | ||
Theorem | lsmssass 31976 | Group sum is associative, subset version (see lsmass 19380). (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ β = (LSSumβπΊ) & β’ π΅ = (BaseβπΊ) & β’ (π β πΊ β Mnd) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β ((π β π) β π) = (π β (π β π))) | ||
Theorem | grplsm0l 31977 | Sumset with the identity singleton is the original set. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ β = (LSSumβπΊ) & β’ 0 = (0gβπΊ) β β’ ((πΊ β Grp β§ π΄ β π΅ β§ π΄ β β ) β ({ 0 } β π΄) = π΄) | ||
Theorem | grplsmid 31978 | The direct sum of an element π of a subgroup π΄ is the subgroup itself. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ β = (LSSumβπΊ) β β’ ((π΄ β (SubGrpβπΊ) β§ π β π΄) β ({π} β π΄) = π΄) | ||
Theorem | quslsm 31979 | 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 31980* | 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 31981 | 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 31982* | Lemma for nsgmgc 31983. (Contributed by Thierry Arnoux, 27-Jul-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ (π β π β (NrmSGrpβπΊ)) & β’ (π β πΉ β (SubGrpβπ)) β β’ (π β {π β π΅ β£ ({π} β π) β πΉ} β (SubGrpβπΊ)) | ||
Theorem | nsgmgc 31983* | 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 31984* | Lemma for nsgqusf1o 31987. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (((π β§ β β (SubGrpβπΊ)) β§ π β β) β ran (π₯ β β β¦ ({π₯} β π)) β π) | ||
Theorem | nsgqusf1olem2 31985* | Lemma for nsgqusf1o 31987. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΈ = π) | ||
Theorem | nsgqusf1olem3 31986* | Lemma for nsgqusf1o 31987. (Contributed by Thierry Arnoux, 4-Aug-2024.) |
β’ π΅ = (BaseβπΊ) & β’ π = {β β (SubGrpβπΊ) β£ π β β} & β’ π = (SubGrpβπ) & β’ β€ = (leβ(toIncβπ)) & β’ β² = (leβ(toIncβπ)) & β’ π = (πΊ /s (πΊ ~QG π)) & β’ β = (LSSumβπΊ) & β’ πΈ = (β β π β¦ ran (π₯ β β β¦ ({π₯} β π))) & β’ πΉ = (π β π β¦ {π β π΅ β£ ({π} β π) β π}) & β’ (π β π β (NrmSGrpβπΊ)) β β’ (π β ran πΉ = π) | ||
Theorem | nsgqusf1o 31987* | 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 31988 | The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024.) |
β’ ((π β Ring β§ πΆ β β β§ πΆ β (LIdealβπ )) β β© πΆ β (LIdealβπ )) | ||
Theorem | rhmpreimaidl 31989 | The preimage of an ideal by a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ πΌ = (LIdealβπ ) β β’ ((πΉ β (π RingHom π) β§ π½ β (LIdealβπ)) β (β‘πΉ β π½) β πΌ) | ||
Theorem | kerlidl 31990 | The kernel of a ring homomorphism is an ideal. (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ πΌ = (LIdealβπ ) & β’ 0 = (0gβπ) β β’ (πΉ β (π RingHom π) β (β‘πΉ β { 0 }) β πΌ) | ||
Theorem | 0ringidl 31991 | 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 31992* | 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 31993 | Ideals are closed under intersection. (Contributed by Thierry Arnoux, 5-Jul-2024.) |
β’ π = (LIdealβπ ) β β’ ((π β Ring β§ πΌ β π β§ π½ β π) β (πΌ β© π½) β π) | ||
Theorem | idlinsubrg 31994 | 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 31995 | 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 31996 | Extend class notation with the class of prime ideals. |
class PrmIdeal | ||
Definition | df-prmidl 31997* | 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 32002 and isprmidlc 32009. (Contributed by Jeff Madsen, 10-Jun-2010.) (Revised by Thierry Arnoux, 14-Jan-2024.) |
β’ PrmIdeal = (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)βπ β (LIdealβπ)(βπ₯ β π βπ¦ β π (π₯(.rβπ)π¦) β π β (π β π β¨ π β π)))}) | ||
Theorem | prmidlval 31998* | 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 31999* | 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 32000 | 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βπ )) β π β π΅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |