![]() |
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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | opprmxidlabs 32601 | The maximal ideal of the opposite ring's opposite ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π = (opprβπ ) & β’ (π β π β Ring) & β’ (π β π β (MaxIdealβπ )) β β’ (π β π β (MaxIdealβ(opprβπ))) | ||
Theorem | opprqusbas 32602 | The base of the quotient of the opposite ring is the same as the base of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β π β π) & β’ (π β πΌ β π΅) β β’ (π β (Baseβ(opprβπ)) = (Baseβ(π /s (π ~QG πΌ)))) | ||
Theorem | opprqusplusg 32603 | The group operation of the quotient of the opposite ring is the same as the group operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β πΌ β (NrmSGrpβπ )) & β’ πΈ = (Baseβπ) & β’ (π β π β πΈ) & β’ (π β π β πΈ) β β’ (π β (π(+gβ(opprβπ))π) = (π(+gβ(π /s (π ~QG πΌ)))π)) | ||
Theorem | opprqus0g 32604 | The group identity element of the quotient of the opposite ring is the same as the group identity element of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β πΌ β (NrmSGrpβπ )) β β’ (π β (0gβ(opprβπ)) = (0gβ(π /s (π ~QG πΌ)))) | ||
Theorem | opprqusmulr 32605 | The multiplication operation of the quotient of the opposite ring is the same as the multiplication operation of the opposite of the quotient ring. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π΅ = (Baseβπ ) & β’ π = (opprβπ ) & β’ π = (π /s (π ~QG πΌ)) & β’ (π β π β Ring) & β’ (π β πΌ β (2Idealβπ )) & β’ πΈ = (Baseβπ) & β’ (π β π β πΈ) & β’ (π β π β πΈ) β β’ (π β (π(.rβ(opprβπ))π) = (π(.rβ(π /s (π ~QG πΌ)))π)) | ||
Theorem | opprqus1r 32606 | 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 32607 | 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 32608* | Lemma for qsdrngi 32609. (Contributed by Thierry Arnoux, 9-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (MaxIdealβπ )) & β’ (π β π β (MaxIdealβπ)) & β’ (π β π β (Baseβπ )) & β’ (π β Β¬ π β π) β β’ (π β βπ£ β (Baseβπ)(π£(.rβπ)[π](π ~QG π)) = (1rβπ)) | ||
Theorem | qsdrngi 32609 | 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 32610 | Lemma for qsdrng 32611. (Contributed by Thierry Arnoux, 13-Mar-2025.) |
β’ π = (opprβπ ) & β’ π = (π /s (π ~QG π)) & β’ (π β π β NzRing) & β’ (π β π β (2Idealβπ )) & β’ π΅ = (Baseβπ ) & β’ (π β π β DivRing) & β’ (π β π½ β (LIdealβπ )) & β’ (π β π β π½) & β’ (π β π β (π½ β π)) β β’ (π β π½ = π΅) | ||
Theorem | qsdrng 32611 | 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 32612 | 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 32613 | 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 32614 | Extend class notation with the semiring of ideals of a ring. |
class IDLsrg | ||
Definition | df-idlsrg 32615* | 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 32616 | 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 32617* | Lemma for idlsrgbas 32618 through idlsrgtset 32622. (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 32618 | Base of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) β β’ (π β π β πΌ = (Baseβπ)) | ||
Theorem | idlsrgplusg 32619 | Additive operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ β = (LSSumβπ ) β β’ (π β π β β = (+gβπ)) | ||
Theorem | idlsrg0g 32620 | 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 32621* | Multiplicative operation of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ πΊ = (mulGrpβπ ) & β’ β = (LSSumβπΊ) β β’ (π β π β (π β π΅, π β π΅ β¦ ((RSpanβπ )β(π β π))) = (.rβπ)) | ||
Theorem | idlsrgtset 32622* | Topology component of the ideals of a ring. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ πΌ = (LIdealβπ ) & β’ π½ = ran (π β πΌ β¦ {π β πΌ β£ Β¬ π β π}) β β’ (π β π β π½ = (TopSetβπ)) | ||
Theorem | idlsrgmulrval 32623 | 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 32624 | Ideals of a ring π are closed under multiplication. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) & β’ π΅ = (LIdealβπ ) & β’ β = (.rβπ) & β’ (π β π β Ring) & β’ (π β πΌ β π΅) & β’ (π β π½ β π΅) β β’ (π β (πΌ β π½) β π΅) | ||
Theorem | idlsrgmulrss1 32625 | 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 32626 | 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 32627 | 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 32628 | The ideals of a ring form a monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β Mnd) | ||
Theorem | idlsrgcmnd 32629 | The ideals of a ring form a commutative monoid. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π = (IDLsrgβπ ) β β’ (π β Ring β π β CMnd) | ||
Syntax | cufd 32630 | Class of unique factorization domains. |
class UFD | ||
Definition | df-ufd 32631* | Define the class of unique factorization domains. A unique factorization domain (UFD for short), is a commutative ring with an absolute value (from abvtriv 20449 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 32632* | The property of being a Unique Factorization Domain. (Contributed by Thierry Arnoux, 1-Jun-2024.) |
β’ π΄ = (AbsValβπ ) & β’ πΌ = (PrmIdealβπ ) & β’ π = (RPrimeβπ ) β β’ (π β UFD β (π β CRing β§ (π΄ β β β§ βπ β πΌ (π β© π) β β ))) | ||
Theorem | rprmval 32633* | The prime elements of a ring π . (Contributed by Thierry Arnoux, 1-Jul-2024.) |
β’ π΅ = (Baseβπ ) & β’ π = (Unitβπ ) & β’ 0 = (0gβπ ) & β’ Β· = (.rβπ ) & β’ β₯ = (β₯rβπ ) β β’ (π β π β (RPrimeβπ ) = {π β (π΅ β (π βͺ { 0 })) β£ βπ₯ β π΅ βπ¦ β π΅ (π β₯ (π₯ Β· π¦) β (π β₯ π₯ β¨ π β₯ π¦))}) | ||
Theorem | isrprm 32634* | 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 32635 | Apply group multiplication to the algebra scalars. (Contributed by Thierry Arnoux, 24-Jul-2024.) |
β’ π΄ = (algScβπ) & β’ πΉ = (Scalarβπ) & β’ πΎ = (BaseβπΉ) & β’ β = (.gβπ) & β’ β = (.gβπΉ) β β’ ((π β AssAlg β§ π β β0 β§ π β πΎ) β (π΄β(π β π)) = (π β (π΄βπ))) | ||
Theorem | 0ringmon1p 32636 | There are no monic polynomials over a zero ring. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π = (Monic1pβπ ) & β’ π΅ = (Baseβπ ) & β’ (π β π β Ring) & β’ (π β (β―βπ΅) = 1) β β’ (π β π = β ) | ||
Theorem | fply1 32637 | 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 32638 | In a division ring, the univariate polynomials form a vector space. (Contributed by Thierry Arnoux, 19-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ (π β π β DivRing) β β’ (π β π β LVec) | ||
Theorem | ply1scleq 32639 | 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 32640 | Functionality of the subring polynomial evaluation. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β π Fn π) | ||
Theorem | evls1dm 32641 | The domain of the subring polynomial evaluation function. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (Poly1β(π βΎs π)) & β’ π = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β dom π = π) | ||
Theorem | evls1fvf 32642 | 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 32643 | Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ π΄ = (algScβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β π ) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π΄βπ))βπΆ) = π) | ||
Theorem | evls1expd 32644 | Univariate polynomial evaluation builder for an exponential. See also evl1expd 21864. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ πΎ = (Baseβπ) & β’ π = (Poly1βπ) & β’ π = (π βΎs π ) & β’ π΅ = (Baseβπ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β β0) & β’ (π β π β π΅) & β’ (π β πΆ β πΎ) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β ((πβπ)βπΆ))) | ||
Theorem | evls1varpwval 32645 | Univariate polynomial evaluation for subrings maps the exponentiation of a variable to the exponentiation of the evaluated variable. See evl1varpwval 21881. (Contributed by Thierry Arnoux, 24-Jan-2025.) |
β’ π = (π evalSub1 π ) & β’ π = (π βΎs π ) & β’ π = (Poly1βπ) & β’ π = (var1βπ) & β’ π΅ = (Baseβπ) & β’ β§ = (.gβ(mulGrpβπ)) & β’ β = (.gβ(mulGrpβπ)) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ)) & β’ (π β π β β0) & β’ (π β πΆ β π΅) β β’ (π β ((πβ(π β§ π))βπΆ) = (π β πΆ)) | ||
Theorem | evls1fpws 32646* | 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 32647 | 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 32648 | 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 32649 | 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 32650 | 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 32651 | 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 32652 | The zero scalar as a polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ π = (0gβπ ) & β’ 0 = (0gβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπ) = 0 ) | ||
Theorem | ply1ascl1 32653 | The multiplicative unit scalar as a univariate polynomial. (Contributed by Thierry Arnoux, 20-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π΄ = (algScβπ) & β’ πΌ = (1rβπ ) & β’ 1 = (1rβπ) & β’ (π β π β Ring) β β’ (π β (π΄βπΌ) = 1 ) | ||
Theorem | ply1asclunit 32654 | 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 32655 | A polynomial with nonpositive degree is the zero polynomial iff its constant term is zero. Biconditional version of deg1scl 25631. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
β’ π· = ( deg1 βπ ) & β’ π = (Poly1βπ ) & β’ 0 = (0gβπ ) & β’ π΅ = (Baseβπ) & β’ π = (0gβπ) & β’ (π β π β Ring) & β’ (π β πΉ β π΅) & β’ (π β (π·βπΉ) β€ 0) β β’ (π β (πΉ = π β ((coe1βπΉ)β0) = 0 )) | ||
Theorem | ressply10g 32656 | 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 32657 | The monic polynomials of a restricted polynomial algebra. (Contributed by Thierry Arnoux, 21-Jan-2025.) |
β’ π = (Poly1βπ ) & β’ π» = (π βΎs π) & β’ π = (Poly1βπ») & β’ π΅ = (Baseβπ) & β’ (π β π β (SubRingβπ )) & β’ π = (Monic1pβπ ) & β’ π = (Monic1pβπ») β β’ (π β π = (π΅ β© π)) | ||
Theorem | ressply1invg 32658 | 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 32659 | 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 32660 | 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 32661 | 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 32662 | 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 32663 | 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 32664* | 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 32665 | 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 32666 | 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 32667 | 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 32668* | 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 32669* | 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 32670 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ πΊ = (idlGen1pβπ ) & β’ π = (Baseβπ) & β’ (π β π β DivRing) & β’ (π β πΌ β (LIdealβπ)) & β’ (π β πΌ β π) β β’ (π β Β¬ (πΊβπΌ) β (Unitβπ)) | ||
Theorem | ig1pmindeg 32671 | 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 32672 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 1 = (1rβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β 1 = (1rβπ΄)) | ||
Theorem | sradrng 32673 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β DivRing β§ π β π΅) β π΄ β DivRing) | ||
Theorem | srasubrg 32674 | 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 32675 | 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 32676 | 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 32677 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπΈ) = (0gβπ΅)) | ||
Theorem | drgextvsca 32678 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (.rβπΈ) = ( Β·π βπ΅)) | ||
Theorem | drgext0gsca 32679 | 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 32680 | 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 32681 | 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 32682* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) & β’ (π β π β π) β β’ (π β (πΈ Ξ£g (π β π β¦ π)) = (π΅ Ξ£g (π β π β¦ π))) | ||
Theorem | lvecdimfi 32683 | Finite version of lvecdim 20770 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18507, which is required in the infinite case. Suggested by GΓ©rard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π½ = (LBasisβπ) & β’ (π β π β LVec) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β π β Fin) β β’ (π β π β π) | ||
Syntax | cldim 32684 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 32685 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 20770, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ dim = (π β V β¦ βͺ (β― β (LBasisβπ))) | ||
Theorem | dimval 32686 | 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 32687 | The dimension of a vector space πΉ is the cardinality of one of its bases. This version of dimval 32686 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 32688 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β LVec β (dimβπ) β β0*) | ||
Theorem | lmimdim 32689 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ (π β πΉ β (π LMIso π)) & β’ (π β π β LVec) β β’ (π β (dimβπ) = (dimβπ)) | ||
Theorem | lvecdim0i 32690 | 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 32691 | 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 32692 | 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 32693* | 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 32694 | 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 32695 | Obsolete version of rlmdim 32694 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 32696 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ πΉ = (π freeLMod πΌ) β β’ ((π β DivRing β§ πΌ β π) β (dimβπΉ) = (β―βπΌ)) | ||
Theorem | tnglvec 32697 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ (π β π β (πΊ β LVec β π β LVec)) | ||
Theorem | tngdim 32698 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ ((πΊ β LVec β§ π β π) β (dimβπΊ) = (dimβπ)) | ||
Theorem | rrxdim 32699 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β (dimβπ») = (β―βπΌ)) | ||
Theorem | matdim 32700 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π΄ = (πΌ Mat π ) & β’ π = (β―βπΌ) β β’ ((πΌ β Fin β§ π β DivRing) β (dimβπ΄) = (π Β· π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |