![]() |
Metamath
Proof Explorer Theorem List (p. 327 of 479) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opprqus1r 32601 | The ring unity of the quotient of the opposite ring is the same as the ring unity of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β π β Ring) & β’ (π β πΌ β (2Idealβπ )) β β’ (π β (1rβ(opprβπ)) = (1rβ(π /s (π ~QG πΌ)))) | ||
Theorem | opprqusdrng 32602 | The quotient of the opposite ring is a division ring iff the opposite of the quotient ring is. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β π β Ring) & β’ (π β πΌ β (2Idealβπ )) β β’ (π β ((opprβπ) β DivRing β (π /s (π ~QG πΌ)) β DivRing)) | ||
Theorem | qsdrngilem 32603* | Lemma for qsdrngi 32604. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (MaxIdealβπ )) & β’ (π β π β (MaxIdealβπ)) & β’ (π β π β (Baseβπ )) & β’ (π β Β¬ π β π) β β’ (π β βπ£ β (Baseβπ)(π£(.rβπ)[π](π ~QG π)) = (1rβπ)) | ||
Theorem | qsdrngi 32604 | A quotient by a maximal left and maximal right ideal is a division ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (MaxIdealβπ )) & β’ (π β π β (MaxIdealβπ)) β β’ (π β π β DivRing) | ||
Theorem | qsdrnglem2 32605 | Lemma for qsdrng 32606. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (2Idealβπ )) & β’ π΅ = (Baseβπ ) & β’ (π β π β DivRing) & β’ (π β π½ β (LIdealβπ )) & β’ (π β π β π½) & β’ (π β π β (π½ β π)) β β’ (π β π½ = π΅) | ||
Theorem | qsdrng 32606 | An ideal π is both left and right maximal if and only if the factor ring π is a division ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (2Idealβπ )) β β’ (π β (π β DivRing β (π β (MaxIdealβπ ) β§ π β (MaxIdealβπ)))) | ||
Theorem | qsfld 32607 | An ideal π in the commutative ring π is maximal if and only if the factor ring π is a field. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (π /s (π ~QG π)) & β’ (π β π β CRing) & β’ (π β π β NzRing) & β’ (π β π β (LIdealβπ )) β β’ (π β (π β Field β π β (MaxIdealβπ ))) | ||
Theorem | mxidlprmALT 32608 | Every maximal ideal is prime - alternative proof. (Contributed by Thierry Arnoux, 15-Mar-2025.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ (π β π β CRing) & β’ (π β π β (MaxIdealβπ )) β β’ (π β π β (PrmIdealβπ )) | ||
Syntax | cidlsrg 32609 | Extend class notation with the semiring of ideals of a ring. |
class IDLsrg | ||
Definition | df-idlsrg 32610* | 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 32611 | 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 32612* | Lemma for idlsrgbas 32613 through idlsrgtset 32617. (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 32613 | Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) β β’ (π β π β πΌ = (Baseβπ)) | ||
Theorem | idlsrgplusg 32614 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ β = (LSSumβπ ) β β’ (π β π β β = (+gβπ)) | ||
Theorem | idlsrg0g 32615 | 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 32616* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (LSSumβπΊ) β β’ (π β π β (π β π΅, π β π΅ β¦ ((RSpanβπ )β(π β π))) = (.rβπ)) | ||
Theorem | idlsrgtset 32617* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β β’ (π β π β π½ = (TopSetβπ)) | ||
Theorem | idlsrgmulrval 32618 | 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 32619 | Ideals of a ring π are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β π΅) | ||
Theorem | idlsrgmulrss1 32620 | 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 32621 | 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 32622 | 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 32623 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β Mnd) | ||
Theorem | idlsrgcmnd 32624 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β CMnd) | ||
Syntax | cufd 32625 | Class of unique factorization domains. |
class UFD | ||
Definition | df-ufd 32626* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20448 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 32627* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π΄ = (AbsValβπ ) & β’ πΌ = (PrmIdealβπ ) & β’ π = (RPrimeβπ ) β β’ (π β UFD β (π β CRing β§ (π΄ β β β§ βπ β πΌ (π β© π) β β ))) | ||
Theorem | rprmval 32628* | The prime elements of a ring π . (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β π β (RPrimeβπ ) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) | ||
Theorem | isrprm 32629* | 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 32630 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ β = (.gβπΉ) β β’ ((π β AssAlg β§ π β β0 β§ π β πΎ) β (π΄β(π β π)) = (π β (π΄βπ))) | ||
Theorem | 0ringmon1p 32631 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π = (Monic1pβπ ) & β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) β β’ (π β π = β ) | ||
Theorem | fply1 32632 | 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 | ply1lvec 32633 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ (π β π β DivRing) β β’ (π β π β LVec) | ||
Theorem | ply1scleq 32634 | 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 | evls1fn 32635 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β π Fn π) | ||
Theorem | evls1dm 32636 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β dom π = π) | ||
Theorem | evls1fvf 32637 | The subring evaluation function for a univariate polynomial as a function, with domain and codomain. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ π΅ = (Baseβπ ) & β’ (π β π β π) β β’ (π β (πβπ):π΅βΆπ΅) | ||
Theorem | evls1scafv 32638 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π΄βπ))βπΆ) = π) | ||
Theorem | evls1expd 32639 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 21863. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β ((πβπ)βπΆ))) | ||
Theorem | evls1varpwval 32640 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 21880. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β πΆ)) | ||
Theorem | evls1fpws 32641* | 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 32642 | 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 | evls1addd 32643 | Univariate polynomial evaluation of a sum of polynomials. (Contributed by Thierry Arnoux, 8-Feb-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & ⒠⨣ = (+gβπ) & β’ + = (+gβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π΅) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π ⨣ π))βπΆ) = (((πβπ)βπΆ) + ((πβπ)βπΆ))) | ||
Theorem | evls1muld 32644 | 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 | evls1vsca 32645 | Univariate polynomial evaluation of a scalar product of polynomials. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ Γ = ( Β·π βπ) & β’ Β· = (.rβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π΄ β π ) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π΄ Γ π))βπΆ) = (π΄ Β· ((πβπ)βπΆ))) | ||
Theorem | ressdeg1 32646 | 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 32647 | The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπ) = 0 ) | ||
Theorem | ply1ascl1 32648 | The multiplicative unit scalar as a univariate polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΌ = (1rβπ ) & β’ 1 = (1rβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπΌ) = 1 ) | ||
Theorem | ply1asclunit 32649 | A non-zero scalar polynomial is a unit. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Field) & β’ (π β π β π΅) & β’ (π β π β 0 ) β β’ (π β (π΄βπ) β (Unitβπ)) | ||
Theorem | deg1le0eq0 32650 | A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 25630. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β (π·βπΉ) β€ 0) β β’ (π β (πΉ = π β ((coe1βπΉ)β0) = 0 )) | ||
Theorem | ressply10g 32651 | 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 32652 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (Monic1pβπ ) & β’ π = (Monic1pβπ») β β’ (π β π = (π΅ β© π)) | ||
Theorem | ressply1invg 32653 | An element of a restricted polynomial algebra has the same group inverse. (Contributed by Thierry Arnoux, 30-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) & β’ (π β π β π΅) β β’ (π β ((invgβπ)βπ) = ((invgβπ)βπ)) | ||
Theorem | ressply1sub 32654 | A restricted polynomial algebra has the same subtraction operation. (Contributed by Thierry Arnoux, 30-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (π βΎs π΅) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (π(-gβπ)π) = (π(-gβπ)π)) | ||
Theorem | asclply1subcl 32655 | Closure of the algebra scalar injection function in a polynomial on a subring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π΄ = (algScβπ) & β’ π = (π βΎs π) & β’ π = (Poly1βπ ) & β’ π = (Poly1βπ) & β’ π = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ (π β π β π) β β’ (π β (π΄βπ) β π) | ||
Theorem | ply1chr 32656 | 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 32657 | 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 32658 | 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 | coe1mon 32659* | Coefficient vector of a monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ (π β π β β0) & β’ 0 = (0gβπ ) & β’ 1 = (1rβπ ) β β’ (π β (coe1β(π β π)) = (π β β0 β¦ if(π = π, 1 , 0 ))) | ||
Theorem | ply1moneq 32660 | Two monomials are equal iff their powers are equal. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β NzRing) & β’ (π β π β β0) & β’ (π β π β β0) β β’ (π β ((π β π) = (π β π) β π = π)) | ||
Theorem | ply1degltel 32661 | Characterize elementhood to the set π of polynomials of degree less than π. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π = (β‘π· β (-β[,)π)) & β’ (π β π β β0) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) β β’ (π β (πΉ β π β (πΉ β π΅ β§ (π·βπΉ) β€ (π β 1)))) | ||
Theorem | ply1degltlss 32662 | The space π of the univariate polynomials of degree less than π forms a vector subspace. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π = (β‘π· β (-β[,)π)) & β’ (π β π β β0) & β’ (π β π β Ring) β β’ (π β π β (LSubSpβπ)) | ||
Theorem | gsummoncoe1fzo 32663* | A coefficient of the polynomial represented as a sum of scaled monomials is the coefficient of the corresponding scaled monomial. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ) & β’ π = (var1βπ ) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β Ring) & β’ πΎ = (Baseβπ ) & β’ β = ( Β·π βπ) & β’ 0 = (0gβπ ) & β’ (π β βπ β (0..^π)π΄ β πΎ) & β’ (π β πΏ β (0..^π)) & β’ (π β π β β0) & β’ (π = πΏ β π΄ = πΆ) β β’ (π β ((coe1β(π Ξ£g (π β (0..^π) β¦ (π΄ β (π β π)))))βπΏ) = πΆ) | ||
Theorem | ply1gsumz 32664* | If a polynomial given as a sum of scaled monomials by factors π΄ is the zero polynomial, then all factors π΄ are zero. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π΅ = (Baseβπ ) & β’ (π β π β β0) & β’ (π β π β Ring) & β’ πΉ = (π β (0..^π) β¦ (π(.gβ(mulGrpβπ))(var1βπ ))) & β’ 0 = (0gβπ ) & β’ π = (0gβπ) & β’ (π β π΄:(0..^π)βΆπ΅) & β’ (π β (π Ξ£g (π΄ βf ( Β·π βπ)πΉ)) = π) β β’ (π β π΄ = ((0..^π) Γ { 0 })) | ||
Theorem | ig1pnunit 32665 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ πΊ = (idlGen1pβπ ) & β’ π = (Baseβπ) & β’ (π β π β DivRing) & β’ (π β πΌ β (LIdealβπ)) & β’ (π β πΌ β π) β β’ (π β Β¬ (πΊβπΌ) β (Unitβπ)) | ||
Theorem | ig1pmindeg 32666 | The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ πΊ = (idlGen1pβπ ) & β’ π = (Baseβπ) & β’ (π β π β DivRing) & β’ (π β πΌ β (LIdealβπ)) & β’ π· = ( deg1 βπ ) & β’ 0 = (0gβπ) & β’ (π β πΉ β πΌ) & β’ (π β πΉ β 0 ) β β’ (π β (π·β(πΊβπΌ)) β€ (π·βπΉ)) | ||
Theorem | sra1r 32667 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 1 = (1rβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β 1 = (1rβπ΄)) | ||
Theorem | sradrng 32668 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β DivRing β§ π β π΅) β π΄ β DivRing) | ||
Theorem | srasubrg 32669 | 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 32670 | 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 32671 | 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 32672 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπΈ) = (0gβπ΅)) | ||
Theorem | drgextvsca 32673 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (.rβπΈ) = ( Β·π βπ΅)) | ||
Theorem | drgext0gsca 32674 | 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 32675 | 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 32676 | 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 32677* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) & β’ (π β π β π) β β’ (π β (πΈ Ξ£g (π β π β¦ π)) = (π΅ Ξ£g (π β π β¦ π))) | ||
Theorem | lvecdimfi 32678 | Finite version of lvecdim 20769 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18506, which is required in the infinite case. Suggested by GΓ©rard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π½ = (LBasisβπ) & β’ (π β π β LVec) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β π β Fin) β β’ (π β π β π) | ||
Syntax | cldim 32679 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 32680 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20769, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ dim = (π β V β¦ βͺ (β― β (LBasisβπ))) | ||
Theorem | dimval 32681 | 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 32682 | The dimension of a vector space πΉ is the cardinality of one of its bases. This version of dimval 32681 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 32683 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β LVec β (dimβπ) β β0*) | ||
Theorem | lmimdim 32684 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ (π β πΉ β (π LMIso π)) & β’ (π β π β LVec) β β’ (π β (dimβπ) = (dimβπ)) | ||
Theorem | lvecdim0i 32685 | 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 32686 | 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 32687 | 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 32688* | 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 | rlmdim 32689 | The left vector space induced by a ring over itself has dimension 1. (Contributed by Thierry Arnoux, 5-Aug-2023.) Generalize to division rings. (Revised by SN, 22-Mar-2025.) |
β’ π = (ringLModβπΉ) β β’ (πΉ β DivRing β (dimβπ) = 1) | ||
Theorem | rgmoddimOLD 32690 | Obsolete version of rlmdim 32689 as of 21-Mar-2025. (Contributed by Thierry Arnoux, 5-Aug-2023.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (ringLModβπΉ) β β’ (πΉ β Field β (dimβπ) = 1) | ||
Theorem | frlmdim 32691 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ πΉ = (π freeLMod πΌ) β β’ ((π β DivRing β§ πΌ β π) β (dimβπΉ) = (β―βπΌ)) | ||
Theorem | tnglvec 32692 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ (π β π β (πΊ β LVec β π β LVec)) | ||
Theorem | tngdim 32693 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ ((πΊ β LVec β§ π β π) β (dimβπΊ) = (dimβπ)) | ||
Theorem | rrxdim 32694 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β (dimβπ») = (β―βπΌ)) | ||
Theorem | matdim 32695 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π΄ = (πΌ Mat π ) & β’ π = (β―βπΌ) β β’ ((πΌ β Fin β§ π β DivRing) β (dimβπ΄) = (π Β· π)) | ||
Theorem | lbslsat 32696 | A nonzero vector π is a basis of a line spanned by the singleton π. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 37841 and for example lsatlspsn 37858. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs (πβ{π})) β β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) | ||
Theorem | lsatdim 32697 | 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 32698 | 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 32699 | 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 32700 | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |