Home | Metamath
Proof Explorer Theorem List (p. 321 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-29659) |
Hilbert Space Explorer
(29660-31182) |
Users' Mathboxes
(31183-46998) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | prmidlnr 32001 | 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 32002* | 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 32003* | A condition that shows an ideal is prime. For commutative rings, this is often taken to be the definition. See ispridlc 36425 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 32004 | 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 32005 | A proper ideal cannot contain the ring unity. (Contributed by Thierry Arnoux, 9-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ πΌ β (LIdealβπ ) β§ πΌ β π΅) β Β¬ 1 β πΌ) | ||
Theorem | prmidlidl 32006 | 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 32007 | Prime ideals as a subset of ideals. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ (π β Ring β (PrmIdealβπ ) β (LIdealβπ )) | ||
Theorem | lidlnsg 32008 | An ideal is a normal subgroup. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ ((π β Ring β§ πΌ β (LIdealβπ )) β πΌ β (NrmSGrpβπ )) | ||
Theorem | cringm4 32009 | Commutative/associative law for commutative ring. (Contributed by Thierry Arnoux, 14-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ Β· = (.rβπ ) β β’ ((π β CRing β§ (π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅)) β ((π Β· π) Β· (π Β· π)) = ((π Β· π) Β· (π Β· π))) | ||
Theorem | isprmidlc 32010* | 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 32011 | 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 32012 | The trivial ring does not have any prime ideal. (Contributed by Thierry Arnoux, 30-Jun-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ (β―βπ΅) = 1) β (PrmIdealβπ ) = β ) | ||
Theorem | prmidl0 32013 | 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) | ||
Theorem | rhmpreimaprmidl 32014 | The preimage of a prime ideal by a ring homomorphism is a prime ideal. (Contributed by Thierry Arnoux, 29-Jun-2024.) |
β’ π = (PrmIdealβπ ) β β’ (((π β CRing β§ πΉ β (π RingHom π)) β§ π½ β (PrmIdealβπ)) β (β‘πΉ β π½) β π) | ||
Theorem | qsidomlem1 32015 | If the quotient ring of a commutative ring relative to an ideal is an integral domain, that ideal must be prime. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ π = (π /s (π ~QG πΌ)) β β’ (((π β CRing β§ πΌ β (LIdealβπ )) β§ π β IDomn) β πΌ β (PrmIdealβπ )) | ||
Theorem | qsidomlem2 32016 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ π = (π /s (π ~QG πΌ)) β β’ ((π β CRing β§ πΌ β (PrmIdealβπ )) β π β IDomn) | ||
Theorem | qsidom 32017 | An ideal πΌ in the commutative ring π is prime if and only if the factor ring π is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ π = (π /s (π ~QG πΌ)) β β’ ((π β CRing β§ πΌ β (LIdealβπ )) β (π β IDomn β πΌ β (PrmIdealβπ ))) | ||
Syntax | cmxidl 32018 | Extend class notation with the class of maximal ideals. |
class MaxIdeal | ||
Definition | df-mxidl 32019* | Define the class of maximal ideals of a ring π . A proper ideal is called maximal if it is maximal with respect to inclusion among proper ideals. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ MaxIdeal = (π β Ring β¦ {π β (LIdealβπ) β£ (π β (Baseβπ) β§ βπ β (LIdealβπ)(π β π β (π = π β¨ π = (Baseβπ))))}) | ||
Theorem | mxidlval 32020* | The set of maximal ideals of a ring. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (MaxIdealβπ ) = {π β (LIdealβπ ) β£ (π β π΅ β§ βπ β (LIdealβπ )(π β π β (π = π β¨ π = π΅)))}) | ||
Theorem | ismxidl 32021* | The predicate "is a maximal ideal". (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ (π β Ring β (π β (MaxIdealβπ ) β (π β (LIdealβπ ) β§ π β π΅ β§ βπ β (LIdealβπ )(π β π β (π = π β¨ π = π΅))))) | ||
Theorem | mxidlidl 32022 | A maximal ideal is an ideal. (Contributed by Jeff Madsen, 5-Jan-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (MaxIdealβπ )) β π β (LIdealβπ )) | ||
Theorem | mxidlnr 32023 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (MaxIdealβπ )) β π β π΅) | ||
Theorem | mxidlmax 32024 | A maximal ideal is a maximal proper ideal. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ (((π β Ring β§ π β (MaxIdealβπ )) β§ (πΌ β (LIdealβπ ) β§ π β πΌ)) β (πΌ = π β¨ πΌ = π΅)) | ||
Theorem | mxidln1 32025 | One is not contained in any maximal ideal. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) & β’ 1 = (1rβπ ) β β’ ((π β Ring β§ π β (MaxIdealβπ )) β Β¬ 1 β π) | ||
Theorem | mxidlnzr 32026 | A ring with a maximal ideal is a nonzero ring. (Contributed by Jeff Madsen, 17-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (MaxIdealβπ )) β π β NzRing) | ||
Theorem | mxidlprm 32027 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ Γ = (LSSumβ(mulGrpβπ )) β β’ ((π β CRing β§ π β (MaxIdealβπ )) β π β (PrmIdealβπ )) | ||
Theorem | ssmxidllem 32028* | The set π used in the proof of ssmxidl 32029 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = {π β (LIdealβπ ) β£ (π β π΅ β§ πΌ β π)} & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β πΌ β π΅) & β’ (π β π β π) & β’ (π β π β β ) & β’ (π β [β] Or π) β β’ (π β βͺ π β π) | ||
Theorem | ssmxidl 32029* | Let π be a ring, and let πΌ be a proper ideal of π . Then there is a maximal ideal of π containing πΌ. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ πΌ β (LIdealβπ ) β§ πΌ β π΅) β βπ β (MaxIdealβπ )πΌ β π) | ||
Theorem | krull 32030* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ (π β NzRing β βπ π β (MaxIdealβπ )) | ||
Theorem | mxidlnzrb 32031* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ (π β Ring β (π β NzRing β βπ π β (MaxIdealβπ ))) | ||
Syntax | cidlsrg 32032 | Extend class notation with the semiring of ideals of a ring. |
class IDLsrg | ||
Definition | df-idlsrg 32033* | Define a structure for the ideals of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ IDLsrg = (π β V β¦ β¦(LIdealβπ) / πβ¦({β¨(Baseβndx), πβ©, β¨(+gβndx), (LSSumβπ)β©, β¨(.rβndx), (π β π, π β π β¦ ((RSpanβπ)β(π(LSSumβ(mulGrpβπ))π)))β©} βͺ {β¨(TopSetβndx), ran (π β π β¦ {π β π β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β π β§ π β π)}β©})) | ||
Theorem | idlsrgstr 32034 | A constructed semiring of ideals is a structure. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = ({β¨(Baseβndx), π΅β©, β¨(+gβndx), + β©, β¨(.rβndx), Β· β©} βͺ {β¨(TopSetβndx), π½β©, β¨(leβndx), β€ β©}) β β’ π Struct β¨1, ;10β© | ||
Theorem | idlsrgval 32035* | Lemma for idlsrgbas 32036 through idlsrgtset 32040. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ πΌ = (LIdealβπ ) & β’ β = (LSSumβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (LSSumβπΊ) β β’ (π β π β (IDLsrgβπ ) = ({β¨(Baseβndx), πΌβ©, β¨(+gβndx), β β©, β¨(.rβndx), (π β πΌ, π β πΌ β¦ ((RSpanβπ )β(π β π)))β©} βͺ {β¨(TopSetβndx), ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π})β©, β¨(leβndx), {β¨π, πβ© β£ ({π, π} β πΌ β§ π β π)}β©})) | ||
Theorem | idlsrgbas 32036 | Baae of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) β β’ (π β π β πΌ = (Baseβπ)) | ||
Theorem | idlsrgplusg 32037 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ β = (LSSumβπ ) β β’ (π β π β β = (+gβπ)) | ||
Theorem | idlsrg0g 32038 | The zero ideal is the additive identity of the semiring of ideals. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ 0 = (0gβπ ) β β’ (π β Ring β { 0 } = (0gβπ)) | ||
Theorem | idlsrgmulr 32039* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (LSSumβπΊ) β β’ (π β π β (π β π΅, π β π΅ β¦ ((RSpanβπ )β(π β π))) = (.rβπ)) | ||
Theorem | idlsrgtset 32040* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β β’ (π β π β π½ = (TopSetβπ)) | ||
Theorem | idlsrgmulrval 32041 | Value of the ring multiplication for the ideals of a ring π . (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ πΊ = (mulGrpβπ ) & β’ Β· = (LSSumβπΊ) & β’ (π β π β π) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) = ((RSpanβπ )β(πΌ Β· π½))) | ||
Theorem | idlsrgmulrcl 32042 | Ideals of a ring π are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β π΅) | ||
Theorem | idlsrgmulrss1 32043 | In a commutative ring, the product of two ideals is a subset of the first one. (Contributed by Thierry Arnoux, 16-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ (π β π β CRing) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β πΌ) | ||
Theorem | idlsrgmulrss2 32044 | The product of two ideals is a subset of the second one. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ Β· = (.rβπ ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β π½) | ||
Theorem | idlsrgmulrssin 32045 | In a commutative ring, the product of two ideals is a subset of their intersection. (Contributed by Thierry Arnoux, 17-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ (π β π β CRing) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β (πΌ β© π½)) | ||
Theorem | idlsrgmnd 32046 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β Mnd) | ||
Theorem | idlsrgcmnd 32047 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β CMnd) | ||
Syntax | cufd 32048 | Class of unique factorization domains. |
class UFD | ||
Definition | df-ufd 32049* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20224 this is equivalent to being a domain) such that every prime ideal contains a prime element (this is a characterization due to Irving Kaplansky). A UFD is sometimes also called a "factorial ring" following the terminology of Bourbaki. (Contributed by Mario Carneiro, 17-Feb-2015.) |
β’ UFD = {π β CRing β£ ((AbsValβπ) β β β§ βπ β (PrmIdealβπ)(π β© (RPrimeβπ)) β β )} | ||
Theorem | isufd 32050* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π΄ = (AbsValβπ ) & β’ πΌ = (PrmIdealβπ ) & β’ π = (RPrimeβπ ) β β’ (π β UFD β (π β CRing β§ (π΄ β β β§ βπ β πΌ (π β© π) β β ))) | ||
Theorem | rprmval 32051* | The prime elements of a ring π . (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β π β (RPrimeβπ ) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) | ||
Theorem | isrprm 32052* | Property for π to be a prime element in the ring π . (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ β₯ = (β₯rβπ ) & β’ Β· = (.rβπ ) β β’ (π β π β (π β (RPrimeβπ ) β (π β (π΅ β (π βͺ { 0 })) β§ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))))) | ||
Theorem | asclmulg 32053 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ β = (.gβπΉ) β β’ ((π β AssAlg β§ π β β0 β§ π β πΎ) β (π΄β(π β π)) = (π β (π΄βπ))) | ||
Theorem | fply1 32054 | Conditions for a function to be a univariate polynomial. (Contributed by Thierry Arnoux, 19-Aug-2023.) |
β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ ) & β’ π = (Baseβ(Poly1βπ )) & β’ (π β πΉ:(β0 βm 1o)βΆπ΅) & β’ (π β πΉ finSupp 0 ) β β’ (π β πΉ β π) | ||
Theorem | ply1scleq 32055 | Equality of a constant polynomial is the same as equality of the constant term. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ π΄ = (algScβπ) & β’ (π β π β Ring) & β’ (π β πΈ β π΅) & β’ (π β πΉ β π΅) β β’ (π β ((π΄βπΈ) = (π΄βπΉ) β πΈ = πΉ)) | ||
Theorem | evls1scafv 32056 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π΄βπ))βπΆ) = π) | ||
Theorem | evls1expd 32057 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 21634. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β ((πβπ)βπΆ))) | ||
Theorem | evls1varpwval 32058 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 21651. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β πΆ)) | ||
Theorem | evls1fpws 32059* | Evaluation of a univariate subring polynomial as a function in a power series. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ Β· = (.rβπ) & β’ β = (.gβ(mulGrpβπ)) & β’ π΄ = (coe1βπ) β β’ (π β (πβπ) = (π₯ β πΎ β¦ (π Ξ£g (π β β0 β¦ ((π΄βπ) Β· (π β π₯)))))) | ||
Theorem | ressply1evl 32060 | Evaluation of a univariate subring polynomial is the same as the evaluation in the bigger ring. (Contributed by Thierry Arnoux, 23-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ πΈ = (eval1βπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) β β’ (π β π = (πΈ βΎ π΅)) | ||
Theorem | evls1muld 32061 | Univariate polynomial evaluation of a product of polynomials. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ Γ = (.rβπ) & β’ Β· = (.rβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π Γ π))βπΆ) = (((πβπ)βπΆ) Β· ((πβπ)βπΆ))) | ||
Theorem | ressdeg1 32062 | The degree of a univariate polynomial in a structure restriction. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π» = (π βΎs π) & β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β π΅) & β’ (π β π β (SubRingβπ )) β β’ (π β (π·βπ) = (( deg1 βπ»)βπ)) | ||
Theorem | ply1ascl0 32063 | The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπ) = 0 ) | ||
Theorem | ressply10g 32064 | A restricted polynomial algebra has the same group identity (zero polynomial). (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (0gβπ) β β’ (π β π = (0gβπ)) | ||
Theorem | ressply1mon1p 32065 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (Monic1pβπ ) & β’ π = (Monic1pβπ») β β’ (π β π = (π΅ β© π)) | ||
Theorem | ply1chr 32066 | The characteristic of a polynomial ring is the characteristic of the underlying ring. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (Poly1βπ ) β β’ (π β CRing β (chrβπ) = (chrβπ )) | ||
Theorem | ply1fermltlchr 32067 | Fermat's little theorem for polynomials in a commutative ring πΉ of characteristic π prime: we have the polynomial equation (π + π΄)βπ = ((πβπ) + π΄). (Contributed by Thierry Arnoux, 9-Jan-2025.) |
β’ π = (Poly1βπΉ) & β’ π = (var1βπΉ) & β’ + = (+gβπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ πΆ = (algScβπ) & β’ π΄ = (πΆβ((β€RHomβπΉ)βπΈ)) & β’ π = (chrβπΉ) & β’ (π β πΉ β CRing) & β’ (π β π β β) & β’ (π β πΈ β β€) β β’ (π β (π β (π + π΄)) = ((π β π) + π΄)) | ||
Theorem | ply1fermltl 32068 | Fermat's little theorem for polynomials. If π is prime, Then (π + π΄)βπ = ((πβπ) + π΄) modulo π. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π = (β€/nβ€βπ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ + = (+gβπ) & β’ π = (mulGrpβπ) & β’ β = (.gβπ) & β’ πΆ = (algScβπ) & β’ π΄ = (πΆβ((β€RHomβπ)βπΈ)) & β’ (π β π β β) & β’ (π β πΈ β β€) β β’ (π β (π β (π + π΄)) = ((π β π) + π΄)) | ||
Theorem | sra1r 32069 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 1 = (1rβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β 1 = (1rβπ΄)) | ||
Theorem | sraring 32070 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β π΄ β Ring) | ||
Theorem | sradrng 32071 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β DivRing β§ π β π΅) β π΄ β DivRing) | ||
Theorem | srasubrg 32072 | A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β π β (SubRingβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β π β (SubRingβπ΄)) | ||
Theorem | sralvec 32073 | Given a sub division ring πΉ of a division ring πΈ, πΈ may be considered as a vector space over πΉ, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ πΉ = (πΈ βΎs π) β β’ ((πΈ β DivRing β§ πΉ β DivRing β§ π β (SubRingβπΈ)) β π΄ β LVec) | ||
Theorem | srafldlvec 32074 | Given a subfield πΉ of a field πΈ, πΈ may be considered as a vector space over πΉ, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ πΉ = (πΈ βΎs π) β β’ ((πΈ β Field β§ πΉ β Field β§ π β (SubRingβπΈ)) β π΄ β LVec) | ||
Theorem | drgext0g 32075 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπΈ) = (0gβπ΅)) | ||
Theorem | drgextvsca 32076 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (.rβπΈ) = ( Β·π βπ΅)) | ||
Theorem | drgext0gsca 32077 | The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπ΅) = (0gβ(Scalarβπ΅))) | ||
Theorem | drgextsubrg 32078 | The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) β β’ (π β π β (SubRingβπ΅)) | ||
Theorem | drgextlsp 32079 | The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) β β’ (π β π β (LSubSpβπ΅)) | ||
Theorem | drgextgsum 32080* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) & β’ (π β π β π) β β’ (π β (πΈ Ξ£g (π β π β¦ π)) = (π΅ Ξ£g (π β π β¦ π))) | ||
Theorem | lvecdimfi 32081 | Finite version of lvecdim 20542 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18378, which is required in the infinite case. Suggested by GΓ©rard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π½ = (LBasisβπ) & β’ (π β π β LVec) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β π β Fin) β β’ (π β π β π) | ||
Syntax | cldim 32082 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 32083 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20542, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ dim = (π β V β¦ βͺ (β― β (LBasisβπ))) | ||
Theorem | dimval 32084 | The dimension of a vector space πΉ is the cardinality of one of its bases. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ π½ = (LBasisβπΉ) β β’ ((πΉ β LVec β§ π β π½) β (dimβπΉ) = (β―βπ)) | ||
Theorem | dimvalfi 32085 | The dimension of a vector space πΉ is the cardinality of one of its bases. This version of dimval 32084 does not depend on the axiom of choice, but it is limited to the case where the base π is finite. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π½ = (LBasisβπΉ) β β’ ((πΉ β LVec β§ π β π½ β§ π β Fin) β (dimβπΉ) = (β―βπ)) | ||
Theorem | dimcl 32086 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β LVec β (dimβπ) β β0*) | ||
Theorem | lvecdim0i 32087 | A vector space of dimension zero is reduced to its identity element. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
β’ 0 = (0gβπ) β β’ ((π β LVec β§ (dimβπ) = 0) β (Baseβπ) = { 0 }) | ||
Theorem | lvecdim0 32088 | A vector space of dimension zero is reduced to its identity element, biconditional version. (Contributed by Thierry Arnoux, 31-Jul-2023.) |
β’ 0 = (0gβπ) β β’ (π β LVec β ((dimβπ) = 0 β (Baseβπ) = { 0 })) | ||
Theorem | lssdimle 32089 | The dimension of a linear subspace is less than or equal to the dimension of the parent vector space. This is corollary 5.4 of [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (π βΎs π) β β’ ((π β LVec β§ π β (LSubSpβπ)) β (dimβπ) β€ (dimβπ)) | ||
Theorem | dimpropd 32090* | If two structures have the same components (properties), they have the same dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β π΅ = (BaseβπΎ)) & β’ (π β π΅ = (BaseβπΏ)) & β’ (π β π΅ β π) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΎ)π¦) = (π₯(+gβπΏ)π¦)) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) β π) & β’ ((π β§ (π₯ β π β§ π¦ β π΅)) β (π₯( Β·π βπΎ)π¦) = (π₯( Β·π βπΏ)π¦)) & β’ πΉ = (ScalarβπΎ) & β’ πΊ = (ScalarβπΏ) & β’ (π β π = (BaseβπΉ)) & β’ (π β π = (BaseβπΊ)) & β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯(+gβπΉ)π¦) = (π₯(+gβπΊ)π¦)) & β’ (π β πΎ β LVec) & β’ (π β πΏ β LVec) β β’ (π β (dimβπΎ) = (dimβπΏ)) | ||
Theorem | rgmoddim 32091 | The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.) |
β’ π = (ringLModβπΉ) β β’ (πΉ β Field β (dimβπ) = 1) | ||
Theorem | frlmdim 32092 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ πΉ = (π freeLMod πΌ) β β’ ((π β DivRing β§ πΌ β π) β (dimβπΉ) = (β―βπΌ)) | ||
Theorem | tnglvec 32093 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ (π β π β (πΊ β LVec β π β LVec)) | ||
Theorem | tngdim 32094 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ ((πΊ β LVec β§ π β π) β (dimβπΊ) = (dimβπ)) | ||
Theorem | rrxdim 32095 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β (dimβπ») = (β―βπΌ)) | ||
Theorem | matdim 32096 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π΄ = (πΌ Mat π ) & β’ π = (β―βπΌ) β β’ ((πΌ β Fin β§ π β DivRing) β (dimβπ΄) = (π Β· π)) | ||
Theorem | lbslsat 32097 | A nonzero vector π is a basis of a line spanned by the singleton π. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 37334 and for example lsatlspsn 37351. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs (πβ{π})) β β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) | ||
Theorem | lsatdim 32098 | A line, spanned by a nonzero singleton, has dimension 1. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs (πβ{π})) β β’ ((π β LVec β§ π β π β§ π β 0 ) β (dimβπ) = 1) | ||
Theorem | drngdimgt0 32099 | The dimension of a vector space that is also a division ring is greater than zero. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΉ β LVec β§ πΉ β DivRing) β 0 < (dimβπΉ)) | ||
Theorem | lmhmlvec2 32100 | A homomorphism of left vector spaces has a left vector space as codomain. (Contributed by Thierry Arnoux, 7-May-2023.) |
β’ ((π β LVec β§ πΉ β (π LMHom π)) β π β LVec) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |