![]() |
Metamath
Proof Explorer Theorem List (p. 333 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ply1gsumz 33201* | 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 | deg1addlt 33202 | If both factors have degree bounded by πΏ, then the sum of the polynomials also has degree bounded by πΏ. See also deg1addle 26024. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ (π β π β Ring) & β’ π΅ = (Baseβπ) & β’ + = (+gβπ) & β’ (π β πΉ β π΅) & β’ (π β πΊ β π΅) & β’ (π β πΏ β β*) & β’ (π β (π·βπΉ) < πΏ) & β’ (π β (π·βπΊ) < πΏ) β β’ (π β (π·β(πΉ + πΊ)) < πΏ) | ||
Theorem | ig1pnunit 33203 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
β’ π = (Poly1βπ ) & β’ πΊ = (idlGen1pβπ ) & β’ π = (Baseβπ) & β’ (π β π β DivRing) & β’ (π β πΌ β (LIdealβπ)) & β’ (π β πΌ β π) β β’ (π β Β¬ (πΊβπΌ) β (Unitβπ)) | ||
Theorem | ig1pmindeg 33204 | 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 | q1pdir 33205 | Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ / = (quot1pβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ (π β π΅ β π) & β’ + = (+gβπ) β β’ (π β ((π΄ + π΅) / πΆ) = ((π΄ / πΆ) + (π΅ / πΆ))) | ||
Theorem | q1pvsca 33206 | Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ / = (quot1pβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β πΆ β π) & β’ Γ = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β π΅ β πΎ) β β’ (π β ((π΅ Γ π΄) / πΆ) = (π΅ Γ (π΄ / πΆ))) | ||
Theorem | r1pvsca 33207 | Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ πΈ = (rem1pβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π· β π) & β’ Γ = ( Β·π βπ) & β’ πΎ = (Baseβπ ) & β’ (π β π΅ β πΎ) β β’ (π β ((π΅ Γ π΄)πΈπ·) = (π΅ Γ (π΄πΈπ·))) | ||
Theorem | r1p0 33208 | Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ πΈ = (rem1pβπ ) & β’ (π β π β Ring) & β’ (π β π· β π) & β’ 0 = (0gβπ) β β’ (π β ( 0 πΈπ·) = 0 ) | ||
Theorem | r1pcyc 33209 | The polynomial remainder operation is periodic. See modcyc 13895. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ πΈ = (rem1pβπ ) & β’ + = (+gβπ) & β’ Β· = (.rβπ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β ((π΄ + (πΆ Β· π΅))πΈπ΅) = (π΄πΈπ΅)) | ||
Theorem | r1padd1 33210 | Addition property of the polynomial remainder operation, similar to modadd1 13897. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ πΈ = (rem1pβπ ) & β’ (π β π β Ring) & β’ (π β π΄ β π) & β’ (π β π· β π) & β’ (π β (π΄πΈπ·) = (π΅πΈπ·)) & β’ + = (+gβπ) & β’ (π β π΅ β π) & β’ (π β πΆ β π) β β’ (π β ((π΄ + πΆ)πΈπ·) = ((π΅ + πΆ)πΈπ·)) | ||
Theorem | r1pid2 33211 | Identity law for polynomial remainder operation: it leaves a polynomial π΄ unchanged iff the degree of π΄ is less than the degree of the divisor π΅. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ π = (Unic1pβπ ) & β’ πΈ = (rem1pβπ ) & β’ (π β π β IDomn) & β’ π· = ( deg1 βπ ) & β’ (π β π΄ β π) & β’ (π β π΅ β π) β β’ (π β ((π΄πΈπ΅) = π΄ β (π·βπ΄) < (π·βπ΅))) | ||
Theorem | r1plmhm 33212* | The univariate polynomial remainder function πΉ is a module homomorphism. Its image (πΉ βs π) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ πΈ = (rem1pβπ ) & β’ π = (Unic1pβπ ) & β’ πΉ = (π β π β¦ (ππΈπ)) & β’ (π β π β Ring) & β’ (π β π β π) β β’ (π β πΉ β (π LMHom (πΉ βs π))) | ||
Theorem | r1pquslmic 33213* | The univariate polynomial remainder ring (πΉ βs π) is module isomorphic with the quotient ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = (Poly1βπ ) & β’ π = (Baseβπ) & β’ πΈ = (rem1pβπ ) & β’ π = (Unic1pβπ ) & β’ πΉ = (π β π β¦ (ππΈπ)) & β’ (π β π β Ring) & β’ (π β π β π) & β’ 0 = (0gβπ) & β’ πΎ = (β‘πΉ β { 0 }) & β’ π = (π /s (π ~QG πΎ)) β β’ (π β π βπ (πΉ βs π)) | ||
Theorem | sra1r 33214 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
β’ (π β π΄ = ((subringAlg βπ)βπ)) & β’ (π β 1 = (1rβπ)) & β’ (π β π β (Baseβπ)) β β’ (π β 1 = (1rβπ΄)) | ||
Theorem | sradrng 33215 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π΄ = ((subringAlg βπ )βπ) & β’ π΅ = (Baseβπ ) β β’ ((π β DivRing β§ π β π΅) β π΄ β DivRing) | ||
Theorem | srasubrg 33216 | 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 33217 | 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 33218 | 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 | resssra 33219 | The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΄ = (Baseβπ ) & β’ π = (π βΎs π΅) & β’ (π β π΅ β π΄) & β’ (π β πΆ β π΅) & β’ (π β π β π) β β’ (π β ((subringAlg βπ)βπΆ) = (((subringAlg βπ )βπΆ) βΎs π΅)) | ||
Theorem | lsssra 33220 | A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π = ((subringAlg βπ )βπΆ) & β’ π΄ = (Baseβπ ) & β’ π = (π βΎs π΅) & β’ (π β π΅ β (SubRingβπ )) & β’ (π β πΆ β (SubRingβπ)) β β’ (π β π΅ β (LSubSpβπ)) | ||
Theorem | drgext0g 33221 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (0gβπΈ) = (0gβπ΅)) | ||
Theorem | drgextvsca 33222 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) β β’ (π β (.rβπΈ) = ( Β·π βπ΅)) | ||
Theorem | drgext0gsca 33223 | 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 33224 | 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 33225 | 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 33226* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
β’ π΅ = ((subringAlg βπΈ)βπ) & β’ (π β πΈ β DivRing) & β’ (π β π β (SubRingβπΈ)) & β’ πΉ = (πΈ βΎs π) & β’ (π β πΉ β DivRing) & β’ (π β π β π) β β’ (π β (πΈ Ξ£g (π β π β¦ π)) = (π΅ Ξ£g (π β π β¦ π))) | ||
Theorem | lvecdimfi 33227 | Finite version of lvecdim 21034 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18537, which is required in the infinite case. Suggested by GΓ©rard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
β’ π½ = (LBasisβπ) & β’ (π β π β LVec) & β’ (π β π β π½) & β’ (π β π β π½) & β’ (π β π β Fin) β β’ (π β π β π) | ||
Syntax | cldim 33228 | Extend class notation with the dimension of a vector space. |
class dim | ||
Definition | df-dim 33229 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21034, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
β’ dim = (π β V β¦ βͺ (β― β (LBasisβπ))) | ||
Theorem | dimval 33230 | 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 33231 | The dimension of a vector space πΉ is the cardinality of one of its bases. This version of dimval 33230 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 33232 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
β’ (π β LVec β (dimβπ) β β0*) | ||
Theorem | lmimdim 33233 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
β’ (π β πΉ β (π LMIso π)) & β’ (π β π β LVec) β β’ (π β (dimβπ) = (dimβπ)) | ||
Theorem | lmicdim 33234 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
β’ (π β π βπ π) & β’ (π β π β LVec) β β’ (π β (dimβπ) = (dimβπ)) | ||
Theorem | lvecdim0i 33235 | 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 33236 | 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 33237 | 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 33238* | 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 33239 | 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 33240 | Obsolete version of rlmdim 33239 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 33241 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ πΉ = (π freeLMod πΌ) β β’ ((π β DivRing β§ πΌ β π) β (dimβπΉ) = (β―βπΌ)) | ||
Theorem | tnglvec 33242 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ (π β π β (πΊ β LVec β π β LVec)) | ||
Theorem | tngdim 33243 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (πΊ toNrmGrp π) β β’ ((πΊ β LVec β§ π β π) β (dimβπΊ) = (dimβπ)) | ||
Theorem | rrxdim 33244 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π» = (β^βπΌ) β β’ (πΌ β π β (dimβπ») = (β―βπΌ)) | ||
Theorem | matdim 33245 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π΄ = (πΌ Mat π ) & β’ π = (β―βπΌ) β β’ ((πΌ β Fin β§ π β DivRing) β (dimβπ΄) = (π Β· π)) | ||
Theorem | lbslsat 33246 | A nonzero vector π is a basis of a line spanned by the singleton π. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38385 and for example lsatlspsn 38402. (Contributed by Thierry Arnoux, 20-May-2023.) |
β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ π = (π βΎs (πβ{π})) β β’ ((π β LVec β§ π β π β§ π β 0 ) β {π} β (LBasisβπ)) | ||
Theorem | lsatdim 33247 | 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 33248 | 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 33249 | 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 33250 | 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 33251 | 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 | ply1degltdimlem 33252* | Lemma for ply1degltdim 33253. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π = (β‘π· β (-β[,)π)) & β’ (π β π β β0) & β’ (π β π β DivRing) & β’ πΈ = (π βΎs π) & β’ πΉ = (π β (0..^π) β¦ (π(.gβ(mulGrpβπ))(var1βπ ))) β β’ (π β ran πΉ β (LBasisβπΈ)) | ||
Theorem | ply1degltdim 33253 | The space π of the univariate polynomials of degree less than π has dimension π. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
β’ π = (Poly1βπ ) & β’ π· = ( deg1 βπ ) & β’ π = (β‘π· β (-β[,)π)) & β’ (π β π β β0) & β’ (π β π β DivRing) & β’ πΈ = (π βΎs π) β β’ (π β (dimβπΈ) = π) | ||
Theorem | lindsunlem 33254 | Lemma for lindsun 33255. (Contributed by Thierry Arnoux, 9-May-2023.) |
β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ (π β π β LVec) & β’ (π β π β (LIndSβπ)) & β’ (π β π β (LIndSβπ)) & β’ (π β ((πβπ) β© (πβπ)) = { 0 }) & β’ π = (0gβ(Scalarβπ)) & β’ πΉ = (Baseβ(Scalarβπ)) & β’ (π β πΆ β π) & β’ (π β πΎ β (πΉ β {π})) & β’ (π β (πΎ( Β·π βπ)πΆ) β (πβ((π βͺ π) β {πΆ}))) β β’ (π β β₯) | ||
Theorem | lindsun 33255 | 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 33256 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33255. (Contributed by Thierry Arnoux, 17-May-2023.) |
β’ π½ = (LBasisβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) β β’ ((π β LVec β§ π΅ β π½ β§ π β π΅) β ((πβ(π΅ β π)) β© (πβπ)) = { 0 }) | ||
Theorem | dimkerim 33257 | 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 33258 | 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 33259* | Lemma for fedgmul 33261. (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 33260* | Lemma for fedgmul 33261. (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 33261 | 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 33262 | Syntax for the field extension relation. |
class /FldExt | ||
Syntax | cfinext 33263 | Syntax for the finite field extension relation. |
class /FinExt | ||
Syntax | calgext 33264 | Syntax for the algebraic field extension relation. |
class /AlgExt | ||
Syntax | cextdg 33265 | Syntax for the field extension degree operation. |
class [:] | ||
Definition | df-fldext 33266* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FldExt = {β¨π, πβ© β£ ((π β Field β§ π β Field) β§ (π = (π βΎs (Baseβπ)) β§ (Baseβπ) β (SubRingβπ)))} | ||
Definition | df-extdg 33267* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ [:] = (π β V, π β (/FldExt β {π}) β¦ (dimβ((subringAlg βπ)β(Baseβπ)))) | ||
Definition | df-finext 33268* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /FinExt = {β¨π, πβ© β£ (π/FldExtπ β§ (π[:]π) β β0)} | ||
Definition | df-algext 33269* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ /AlgExt = {β¨π, πβ© β£ (π/FldExtπ β§ βπ₯ β (Baseβπ)βπ β (Poly1βπ)(((eval1βπ)βπ)βπ₯) = (0gβπ))} | ||
Theorem | relfldext 33270 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ Rel /FldExt | ||
Theorem | brfldext 33271 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ β Field β§ πΉ β Field) β (πΈ/FldExtπΉ β (πΉ = (πΈ βΎs (BaseβπΉ)) β§ (BaseβπΉ) β (SubRingβπΈ)))) | ||
Theorem | ccfldextrr 33272 | The field of the complex numbers is an extension of the field of the real numbers. (Contributed by Thierry Arnoux, 20-Jul-2023.) |
β’ βfld/FldExtβfld | ||
Theorem | fldextfld1 33273 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΈ β Field) | ||
Theorem | fldextfld2 33274 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ β Field) | ||
Theorem | fldextsubrg 33275 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ π = (BaseβπΉ) β β’ (πΈ/FldExtπΉ β π β (SubRingβπΈ)) | ||
Theorem | fldextress 33276 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β πΉ = (πΈ βΎs (BaseβπΉ))) | ||
Theorem | brfinext 33277 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ/FinExtπΉ β (πΈ[:]πΉ) β β0)) | ||
Theorem | extdgval 33278 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) = (dimβ((subringAlg βπΈ)β(BaseβπΉ)))) | ||
Theorem | fldextsralvec 33279 | The subring algebra associated with a field extension is a vector space. (Contributed by Thierry Arnoux, 3-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((subringAlg βπΈ)β(BaseβπΉ)) β LVec) | ||
Theorem | extdgcl 33280 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ (πΈ/FldExtπΉ β (πΈ[:]πΉ) β β0*) | ||
Theorem | extdggt0 33281 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΈ/FldExtπΉ β 0 < (πΈ[:]πΉ)) | ||
Theorem | fldexttr 33282 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β πΈ/FldExtπΎ) | ||
Theorem | fldextid 33283 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ (πΉ β Field β πΉ/FldExtπΉ) | ||
Theorem | extdgid 33284 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
β’ (πΈ β Field β (πΈ[:]πΈ) = 1) | ||
Theorem | extdgmul 33285 | The multiplicativity formula for degrees of field extensions. Given πΈ a field extension of πΉ, itself a field extension of πΎ, the degree of the extension πΈ/FldExtπΎ is the product of the degrees of the extensions πΈ/FldExtπΉ and πΉ/FldExtπΎ. Proposition 1.2 of [Lang], p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ[:]πΎ) = ((πΈ[:]πΉ) Β·e (πΉ[:]πΎ))) | ||
Theorem | finexttrb 33286 | The extension πΈ of πΎ is finite if and only if πΈ is finite over πΉ and πΉ is finite over πΎ. Corollary 1.3 of [Lang] , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
β’ ((πΈ/FldExtπΉ β§ πΉ/FldExtπΎ) β (πΈ/FinExtπΎ β (πΈ/FinExtπΉ β§ πΉ/FinExtπΎ))) | ||
Theorem | extdg1id 33287 | If the degree of the extension πΈ/FldExtπΉ is 1, then πΈ and πΉ are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ ((πΈ/FldExtπΉ β§ (πΈ[:]πΉ) = 1) β πΈ = πΉ) | ||
Theorem | extdg1b 33288 | The degree of the extension πΈ/FldExtπΉ is 1 iff πΈ and πΉ are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
β’ (πΈ/FldExtπΉ β ((πΈ[:]πΉ) = 1 β πΈ = πΉ)) | ||
Theorem | fldextchr 33289 | The characteristic of a subfield is the same as the characteristic of the larger field. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (πΈ/FldExtπΉ β (chrβπΉ) = (chrβπΈ)) | ||
Theorem | evls1fldgencl 33290 | Closure of the subring polynomial evaluation in the field extention. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
β’ π΅ = (BaseβπΈ) & β’ π = (πΈ evalSub1 πΉ) & β’ π = (Poly1β(πΈ βΎs πΉ)) & β’ π = (Baseβπ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ (π β π΄ β π΅) & β’ (π β πΊ β π) β β’ (π β ((πβπΊ)βπ΄) β (πΈ fldGen (πΉ βͺ {π΄}))) | ||
Theorem | ccfldsrarelvec 33291 | The subring algebra of the complex numbers over the real numbers is a left vector space. (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ ((subringAlg ββfld)ββ) β LVec | ||
Theorem | ccfldextdgrr 33292 | The degree of the field extension of the complex numbers over the real numbers is 2. (Suggested by GL, 4-Aug-2023.) (Contributed by Thierry Arnoux, 20-Aug-2023.) |
β’ (βfld[:]βfld) = 2 | ||
Syntax | cirng 33293 | Integral subring of a ring. |
class IntgRing | ||
Definition | df-irng 33294* | Define the subring of elements of a ring π integral over a subset π . (Contributed by Mario Carneiro, 2-Dec-2014.) (Revised by Thierry Arnoux, 28-Jan-2025.) |
β’ IntgRing = (π β V, π β V β¦ βͺ π β (Monic1pβ(π βΎs π ))(β‘((π evalSub1 π )βπ) β {(0gβπ)})) | ||
Theorem | irngval 33295* | The elements of a field π integral over a subset π. In the case of a subfield, those are the algebraic numbers over the field π within the field π . That is, the numbers π which are roots of monic polynomials π(π) with coefficients in π. (Contributed by Thierry Arnoux, 28-Jan-2025.) |
β’ π = (π evalSub1 π) & β’ π = (π βΎs π) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β Ring) & β’ (π β π β π΅) β β’ (π β (π IntgRing π) = βͺ π β (Monic1pβπ)(β‘(πβπ) β { 0 })) | ||
Theorem | elirng 33296* | Property for an element π of a field π to be integral over a subring π. (Contributed by Thierry Arnoux, 28-Jan-2025.) |
β’ π = (π evalSub1 π) & β’ π = (π βΎs π) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β (π β (π IntgRing π) β (π β π΅ β§ βπ β (Monic1pβπ)((πβπ)βπ) = 0 ))) | ||
Theorem | irngss 33297 | All elements of a subring π are integral over π. This is only true in the case of a nonzero ring, since there are no integral elements in a zero ring (see 0ringirng 33299). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
β’ π = (π evalSub1 π) & β’ π = (π βΎs π) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β π β NzRing) β β’ (π β π β (π IntgRing π)) | ||
Theorem | irngssv 33298 | An integral element is an element of the base set. (Contributed by Thierry Arnoux, 28-Jan-2025.) |
β’ π = (π evalSub1 π) & β’ π = (π βΎs π) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) β β’ (π β (π IntgRing π) β π΅) | ||
Theorem | 0ringirng 33299 | A zero ring π has no integral elements. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π = (π evalSub1 π) & β’ π = (π βΎs π) & β’ π΅ = (Baseβπ ) & β’ 0 = (0gβπ ) & β’ (π β π β CRing) & β’ (π β π β (SubRingβπ )) & β’ (π β Β¬ π β NzRing) β β’ (π β (π IntgRing π) = β ) | ||
Theorem | irngnzply1lem 33300 | In the case of a field πΈ, a root π of some nonzero polynomial π with coefficients in a subfield πΉ is integral over πΉ. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
β’ π = (πΈ evalSub1 πΉ) & β’ π = (0gβ(Poly1βπΈ)) & β’ 0 = (0gβπΈ) & β’ (π β πΈ β Field) & β’ (π β πΉ β (SubDRingβπΈ)) & β’ π΅ = (BaseβπΈ) & β’ (π β π β dom π) & β’ (π β π β π) & β’ (π β ((πβπ)βπ) = 0 ) & β’ (π β π β π΅) β β’ (π β π β (πΈ IntgRing πΉ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |