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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | rhmpreimaprmidl 32001 | 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 32002 | 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 32003 | A quotient by a prime ideal is an integral domain. (Contributed by Thierry Arnoux, 16-Jan-2024.) |
β’ π = (π /s (π ~QG πΌ)) β β’ ((π β CRing β§ πΌ β (PrmIdealβπ )) β π β IDomn) | ||
Theorem | qsidom 32004 | 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 32005 | Extend class notation with the class of maximal ideals. |
class MaxIdeal | ||
Definition | df-mxidl 32006* | 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 32007* | 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 32008* | 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 32009 | 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 32010 | A maximal ideal is proper. (Contributed by Jeff Madsen, 16-Jun-2011.) (Revised by Thierry Arnoux, 19-Jan-2024.) |
β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β (MaxIdealβπ )) β π β π΅) | ||
Theorem | mxidlmax 32011 | 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 32012 | 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 32013 | 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 32014 | Every maximal ideal is prime. Statement in [Lang] p. 92. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
β’ Γ = (LSSumβ(mulGrpβπ )) β β’ ((π β CRing β§ π β (MaxIdealβπ )) β π β (PrmIdealβπ )) | ||
Theorem | ssmxidllem 32015* | The set π used in the proof of ssmxidl 32016 satisfies the condition of Zorn's Lemma. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = {π β (LIdealβπ ) β£ (π β π΅ β§ πΌ β π)} & β’ (π β π β Ring) & β’ (π β πΌ β (LIdealβπ )) & β’ (π β πΌ β π΅) & β’ (π β π β π) & β’ (π β π β β ) & β’ (π β [β] Or π) β β’ (π β βͺ π β π) | ||
Theorem | ssmxidl 32016* | 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 32017* | Krull's theorem: Any nonzero ring has at least one maximal ideal. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ (π β NzRing β βπ π β (MaxIdealβπ )) | ||
Theorem | mxidlnzrb 32018* | A ring is nonzero if and only if it has maximal ideals. (Contributed by Thierry Arnoux, 10-Apr-2024.) |
β’ (π β Ring β (π β NzRing β βπ π β (MaxIdealβπ ))) | ||
Syntax | cidlsrg 32019 | Extend class notation with the semiring of ideals of a ring. |
class IDLsrg | ||
Definition | df-idlsrg 32020* | 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 32021 | 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 32022* | Lemma for idlsrgbas 32023 through idlsrgtset 32027. (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 32023 | Baae of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) β β’ (π β π β πΌ = (Baseβπ)) | ||
Theorem | idlsrgplusg 32024 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ β = (LSSumβπ ) β β’ (π β π β β = (+gβπ)) | ||
Theorem | idlsrg0g 32025 | 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 32026* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (LSSumβπΊ) β β’ (π β π β (π β π΅, π β π΅ β¦ ((RSpanβπ )β(π β π))) = (.rβπ)) | ||
Theorem | idlsrgtset 32027* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β β’ (π β π β π½ = (TopSetβπ)) | ||
Theorem | idlsrgmulrval 32028 | 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 32029 | Ideals of a ring π are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β π΅) | ||
Theorem | idlsrgmulrss1 32030 | 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 32031 | 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 32032 | 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 32033 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β Mnd) | ||
Theorem | idlsrgcmnd 32034 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β CMnd) | ||
Syntax | cufd 32035 | Class of unique factorization domains. |
class UFD | ||
Definition | df-ufd 32036* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20223 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 32037* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π΄ = (AbsValβπ ) & β’ πΌ = (PrmIdealβπ ) & β’ π = (RPrimeβπ ) β β’ (π β UFD β (π β CRing β§ (π΄ β β β§ βπ β πΌ (π β© π) β β ))) | ||
Theorem | rprmval 32038* | The prime elements of a ring π . (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β π β (RPrimeβπ ) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) | ||
Theorem | isrprm 32039* | 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 32040 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ β = (.gβπΉ) β β’ ((π β AssAlg β§ π β β0 β§ π β πΎ) β (π΄β(π β π)) = (π β (π΄βπ))) | ||
Theorem | fply1 32041 | 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 32042 | 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 32043 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π΄βπ))βπΆ) = π) | ||
Theorem | evls1expd 32044 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 21633. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β ((πβπ)βπΆ))) | ||
Theorem | evls1varpwval 32045 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 21650. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β πΆ)) | ||
Theorem | evls1fpws 32046* | 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 32047 | 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 32048 | 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 32049 | 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 32050 | The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπ) = 0 ) | ||
Theorem | ressply10g 32051 | 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 32052 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (Monic1pβπ ) & β’ π = (Monic1pβπ») β β’ (π β π = (π΅ β© π)) | ||
Theorem | ply1chr 32053 | 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 32054 | 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 32055 | 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 32056 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 1 = (1rβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β 1 = (1rβπ΄)) | ||
Theorem | sraring 32057 | Condition for a subring algebra to be a ring. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β Ring β§ π β π΅) β π΄ β Ring) | ||
Theorem | sradrng 32058 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β DivRing β§ π β π΅) β π΄ β DivRing) | ||
Theorem | srasubrg 32059 | 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 32060 | 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 32061 | 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 32062 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπΈ) = (0gβπ΅)) | ||
Theorem | drgextvsca 32063 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (.rβπΈ) = ( Β·π βπ΅)) | ||
Theorem | drgext0gsca 32064 | 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 32065 | 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 32066 | 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 32067* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) & β’ (π β π β π) β β’ (π β (πΈ Ξ£g (π β π β¦ π)) = (π΅ Ξ£g (π β π β¦ π))) | ||
Theorem | lvecdimfi 32068 | Finite version of lvecdim 20541 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 32069 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 32070 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20541, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ dim = (π β V β¦ βͺ (β― β (LBasisβπ))) | ||
Theorem | dimval 32071 | 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 32072 | The dimension of a vector space πΉ is the cardinality of one of its bases. This version of dimval 32071 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 32073 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β LVec β (dimβπ) β β0*) | ||
Theorem | lvecdim0i 32074 | 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 32075 | 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 32076 | 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 32077* | 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 32078 | 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 32079 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ πΉ = (π freeLMod πΌ) β β’ ((π β DivRing β§ πΌ β π) β (dimβπΉ) = (β―βπΌ)) | ||
Theorem | tnglvec 32080 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ (π β π β (πΊ β LVec β π β LVec)) | ||
Theorem | tngdim 32081 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ ((πΊ β LVec β§ π β π) β (dimβπΊ) = (dimβπ)) | ||
Theorem | rrxdim 32082 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β (dimβπ») = (β―βπΌ)) | ||
Theorem | matdim 32083 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π΄ = (πΌ Mat π ) & β’ π = (β―βπΌ) β β’ ((πΌ β Fin β§ π β DivRing) β (dimβπ΄) = (π Β· π)) | ||
Theorem | lbslsat 32084 | A nonzero vector π is a basis of a line spanned by the singleton π. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 37324 and for example lsatlspsn 37341. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs (πβ{π})) β β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) | ||
Theorem | lsatdim 32085 | 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 32086 | 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 32087 | A homomorphism of left vector spaces has a left vector space as codomain. (Contributed by Thierry Arnoux, 7-May-2023.) |
β’ ((π β LVec β§ πΉ β (π LMHom π)) β π β LVec) | ||
Theorem | kerlmhm 32088 | The kernel of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.) |
β’ 0 = (0gβπ) & β’ πΎ = (π βΎs (β‘πΉ β { 0 })) β β’ ((π β LVec β§ πΉ β (π LMHom π)) β πΎ β LVec) | ||
Theorem | imlmhm 32089 | The image of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023.) |
β’ πΌ = (π βΎs ran πΉ) β β’ ((π β LVec β§ πΉ β (π LMHom π)) β πΌ β LVec) | ||
Theorem | lindsunlem 32090 | Lemma for lindsun 32091. (Contributed by Thierry Arnoux, 9-May-2023.) |
β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π β (LIndSβπ)) & β’ (π β π β (LIndSβπ)) & β’ (π β ((πβπ) β© (πβπ)) = { 0 }) & β’ π = (0gβ(Scalarβπ)) & β’ πΉ = (Baseβ(Scalarβπ)) & β’ (π β πΆ β π) & β’ (π β πΎ β (πΉ β {π})) & β’ (π β (πΎ( Β·π βπ)πΆ) β (πβ((π βͺ π) β {πΆ}))) β β’ (π β β₯) | ||
Theorem | lindsun 32091 | Condition for the union of two independent sets to be an independent set. (Contributed by Thierry Arnoux, 9-May-2023.) |
β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π β (LIndSβπ)) & β’ (π β π β (LIndSβπ)) & β’ (π β ((πβπ) β© (πβπ)) = { 0 }) β β’ (π β (π βͺ π) β (LIndSβπ)) | ||
Theorem | lbsdiflsp0 32092 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 32091. (Contributed by Thierry Arnoux, 17-May-2023.) |
β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π΅ β π½ β§ π β π΅) β ((πβ(π΅ β π)) β© (πβπ)) = { 0 }) | ||
Theorem | dimkerim 32093 | Given a linear map πΉ between vector spaces π and π, the dimension of the vector space π is the sum of the dimension of πΉ 's kernel and the dimension of πΉ's image. Second part of theorem 5.3 in [Lang] p. 141 This can also be described as the Rank-nullity theorem, (dimβπΌ) being the rank of πΉ (the dimension of its image), and (dimβπΎ) its nullity (the dimension of its kernel). (Contributed by Thierry Arnoux, 17-May-2023.) |
β’ 0 = (0gβπ) & β’ πΎ = (π βΎs (β‘πΉ β { 0 })) & β’ πΌ = (π βΎs ran πΉ) β β’ ((π β LVec β§ πΉ β (π LMHom π)) β (dimβπ) = ((dimβπΎ) +π (dimβπΌ))) | ||
Theorem | qusdimsum 32094 | Let π be a vector space, and let π be a subspace. Then the dimension of π is the sum of the dimension of π and the dimension of the quotient space of π. First part of theorem 5.3 in [Lang] p. 141. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (π βΎs π) & β’ π = (π /s (π ~QG π)) β β’ ((π β LVec β§ π β (LSubSpβπ)) β (dimβπ) = ((dimβπ) +π (dimβπ))) | ||
Theorem | fedgmullem1 32095* | Lemma for fedgmul 32097. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) & β’ π· = (π β π, π β π β¦ (π(.rβπΈ)π)) & β’ π» = (π β π, π β π β¦ ((πΊβπ)βπ)) & β’ (π β π β (LBasisβπΆ)) & β’ (π β π β (LBasisβπ΅)) & β’ (π β π β (Baseβπ΄)) & β’ (π β πΏ:πβΆ(Baseβ(Scalarβπ΅))) & β’ (π β πΏ finSupp (0gβ(Scalarβπ΅))) & β’ (π β π = (π΅ Ξ£g (π β π β¦ ((πΏβπ)( Β·π βπ΅)π)))) & β’ (π β πΊ:πβΆ((Baseβ(ScalarβπΆ)) βm π)) & β’ ((π β§ π β π) β (πΊβπ) finSupp (0gβ(ScalarβπΆ))) & β’ ((π β§ π β π) β (πΏβπ) = (πΆ Ξ£g (π β π β¦ (((πΊβπ)βπ)( Β·π βπΆ)π)))) β β’ (π β (π» finSupp (0gβ(Scalarβπ΄)) β§ π = (π΄ Ξ£g (π» βf ( Β·π βπ΄)π·)))) | ||
Theorem | fedgmullem2 32096* | Lemma for fedgmul 32097. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) & β’ π· = (π β π, π β π β¦ (π(.rβπΈ)π)) & β’ π» = (π β π, π β π β¦ ((πΊβπ)βπ)) & β’ (π β π β (LBasisβπΆ)) & β’ (π β π β (LBasisβπ΅)) & β’ (π β π β (Baseβ((Scalarβπ΄) freeLMod (π Γ π)))) & β’ (π β (π΄ Ξ£g (π βf ( Β·π βπ΄)π·)) = (0gβπ΄)) β β’ (π β π = ((π Γ π) Γ {(0gβ(Scalarβπ΄))})) | ||
Theorem | fedgmul 32097 | The multiplicativity formula for degrees of field extensions. Given πΈ a field extension of πΉ, itself a field extension of πΎ, we have [πΈ:πΎ] = [πΈ:πΉ][πΉ:πΎ]. Proposition 1.2 of [Lang], p. 224. Here (dimβπ΄) is the degree of the extension πΈ of πΎ, (dimβπ΅) is the degree of the extension πΈ of πΉ, and (dimβπΆ) is the degree of the extension πΉ of πΎ. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.) |
β’ π΄ = ((subringAlg βπΈ)βπ) & β’ π΅ = ((subringAlg βπΈ)βπ) & β’ πΆ = ((subringAlg βπΉ)βπ) & β’ πΉ = (πΈ βΎs π) & β’ πΎ = (πΈ βΎs π) & β’ (π β πΈ β DivRing) & β’ (π β πΉ β DivRing) & β’ (π β πΎ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ (π β π β (SubRingβπΉ)) β β’ (π β (dimβπ΄) = ((dimβπ΅) Β·e (dimβπΆ))) | ||
Syntax | cfldext 32098 | Syntax for the field extension relation. |
class /FldExt | ||
Syntax | cfinext 32099 | Syntax for the finite field extension relation. |
class /FinExt | ||
Syntax | calgext 32100 | Syntax for the algebraic field extension relation. |
class /AlgExt |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |