HomeTheorem List (p. 337 of 489)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 337 of 489) | < 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-30950) |
Hilbert Space Explorer
(30951-32473) |
Users' Mathboxes
(32474-48899) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | srafldlvec 33601 | 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 33602 | 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 33603 | A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶) & ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊)) | ||
| Theorem | drgext0g 33604 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
| Theorem | drgextvsca 33605 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
| Theorem | drgext0gsca 33606 | 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 33607 | 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 33608 | 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 33609* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
| Theorem | lvecdimfi 33610 | Finite version of lvecdim 21182 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18624, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Syntax | cldim 33611 | Extend class notation with the dimension of a vector space. |
| class dim | ||
| Definition | df-dim 33612 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21182, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
| Theorem | dimval 33613 | 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 33614 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33613 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 33615 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
| Theorem | lmimdim 33616 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lmicdim 33617 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
| ⊢ (𝜑 → 𝑆 ≃𝑚 𝑇) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lvecdim0i 33618 | 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 33619 | 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 33620 | 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 33621* | 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 33622 | 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 33623 | Obsolete version of rlmdim 33622 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 33624 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
| Theorem | tnglvec 33625 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
| Theorem | tngdim 33626 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
| Theorem | rrxdim 33627 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
| Theorem | matdim 33628 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
| Theorem | lbslsat 33629 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38932 and for example lsatlspsn 38949. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
| Theorem | lsatdim 33630 | 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 33631 | 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 33632 | 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 33633 | 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 33634 | 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 33635* | Lemma for ply1degltdim 33636. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ 𝐸 = (𝑃 ↾s 𝑆) & ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) | ||
| Theorem | ply1degltdim 33636 | 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 33637 | Lemma for lindsun 33638. (Contributed by Thierry Arnoux, 9-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
| Theorem | lindsun 33638 | 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 33639 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33638. (Contributed by Thierry Arnoux, 17-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
| Theorem | dimkerim 33640 | 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 33641 | 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 33642* | Lemma for fedgmul 33644. (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 33643* | Lemma for fedgmul 33644. (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 33644 | 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‘𝐶))) | ||
| Theorem | dimlssid 33645 | If the dimension of a linear subspace 𝐿 is the dimension of the whole vector space 𝐸, then 𝐿 is the whole space. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ LVec) & ⊢ (𝜑 → (dim‘𝐸) ∈ ℕ0) & ⊢ (𝜑 → 𝐿 ∈ (LSubSp‘𝐸)) & ⊢ (𝜑 → (dim‘(𝐸 ↾s 𝐿)) = (dim‘𝐸)) ⇒ ⊢ (𝜑 → 𝐿 = 𝐵) | ||
| Theorem | lvecendof1f1o 33646 | If an endomorphism 𝑈 of a vector space 𝐸 of finite dimension is injective, then it is bijective. Item (b) of Corollary of Proposition 9 in [BourbakiAlg1] p. 298 . (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ LVec) & ⊢ (𝜑 → (dim‘𝐸) ∈ ℕ0) & ⊢ (𝜑 → 𝑈 ∈ (𝐸 LMHom 𝐸)) & ⊢ (𝜑 → 𝑈:𝐵–1-1→𝐵) ⇒ ⊢ (𝜑 → 𝑈:𝐵–1-1-onto→𝐵) | ||
| Theorem | lactlmhm 33647* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20335. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴)) | ||
| Theorem | assalactf1o 33648* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33647. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ 𝐸 = (RLReg‘𝐴) & ⊢ 𝐾 = (Scalar‘𝐴) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵) | ||
| Theorem | assarrginv 33649 | If an element 𝑋 of an associative algebra 𝐴 over a division ring 𝐾 is regular, then it is a unit. Proposition 2. in Chapter 5. of [BourbakiAlg2] p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐸 = (RLReg‘𝐴) & ⊢ 𝑈 = (Unit‘𝐴) & ⊢ 𝐾 = (Scalar‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0) & ⊢ (𝜑 → 𝑋 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝑋 ∈ 𝑈) | ||
| Theorem | assafld 33650 | If an algebra 𝐴 of finite degree over a division ring 𝐾 is an integral domain, then it is a field. Corollary of Proposition 2. in Chapter 5. of [BourbakiAlg2] p. 113. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐾 = (Scalar‘𝐴) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ (𝜑 → 𝐴 ∈ IDomn) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0) ⇒ ⊢ (𝜑 → 𝐴 ∈ Field) | ||
| Syntax | cfldext 33651 | Syntax for the field extension relation. |
| class /FldExt | ||
| Syntax | cfinext 33652 | Syntax for the finite field extension relation. |
| class /FinExt | ||
| Syntax | calgext 33653 | Syntax for the algebraic field extension relation. |
| class /AlgExt | ||
| Syntax | cextdg 33654 | Syntax for the field extension degree operation. |
| class [:] | ||
| Definition | df-fldext 33655* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
| Definition | df-extdg 33656* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
| Definition | df-finext 33657* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
| Definition | df-algext 33658* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))} | ||
| Theorem | relfldext 33659 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ Rel /FldExt | ||
| Theorem | brfldext 33660 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
| Theorem | ccfldextrr 33661 | 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 33662 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
| Theorem | fldextfld2 33663 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
| Theorem | fldextsubrg 33664 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
| Theorem | fldextress 33665 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
| Theorem | brfinext 33666 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
| Theorem | extdgval 33667 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
| Theorem | fldextsralvec 33668 | 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 33669 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
| Theorem | extdggt0 33670 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
| Theorem | fldexttr 33671 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
| Theorem | fldextid 33672 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
| Theorem | extdgid 33673 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
| ⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
| Theorem | extdgmul 33674 | 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 33675 | 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 33676 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
| Theorem | extdg1b 33677 | The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹)) | ||
| Theorem | fldgenfldext 33678 | A subfield 𝐹 extended with a set 𝐴 forms a field extension. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ 𝐴))) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ⊆ 𝐵) ⇒ ⊢ (𝜑 → 𝐿/FldExt𝐾) | ||
| Theorem | fldextchr 33679 | 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 33680 | 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 33681 | 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 33682 | 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 33683 | Integral subring of a ring. |
| class IntgRing | ||
| Definition | df-irng 33684* | 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 33685* | 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 33686* | 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 33687 | 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 33689). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
| Theorem | irngssv 33688 | 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 33689 | 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 33690 | 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 𝐹)) | ||
| Theorem | irngnzply1 33691* | In the case of a field 𝐸, the roots of nonzero polynomials 𝑝 with coefficients in a subfield 𝐹 are exactly the integral elements over 𝐹. Roots of nonzero polynomials are called algebraic numbers, so this shows that in the case of a field, elements integral over 𝐹 are exactly the algebraic numbers. In this formula, dom 𝑂 represents the polynomials, and 𝑍 the zero polynomial. (Contributed by Thierry Arnoux, 5-Feb-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑍 = (0g‘(Poly1‘𝐸)) & ⊢ 0 = (0g‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) ⇒ ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = ∪ 𝑝 ∈ (dom 𝑂 ∖ {𝑍})(◡(𝑂‘𝑝) “ { 0 })) | ||
| Syntax | cminply 33692 | Extend class notation with the minimal polynomial builder function. |
| class minPoly | ||
| Definition | df-minply 33693* | Define the minimal polynomial builder function. (Contributed by Thierry Arnoux, 19-Jan-2025.) |
| ⊢ minPoly = (𝑒 ∈ V, 𝑓 ∈ V ↦ (𝑥 ∈ (Base‘𝑒) ↦ ((idlGen1p‘(𝑒 ↾s 𝑓))‘{𝑝 ∈ dom (𝑒 evalSub1 𝑓) ∣ (((𝑒 evalSub1 𝑓)‘𝑝)‘𝑥) = (0g‘𝑒)}))) | ||
| Theorem | ply1annidllem 33694* | Write the set 𝑄 of polynomials annihilating an element 𝐴 as the kernel of the ring homomorphism 𝐹 mapping polynomials 𝑝 to their subring evaluation at a given point 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } & ⊢ 𝐹 = (𝑝 ∈ (Base‘𝑃) ↦ ((𝑂‘𝑝)‘𝐴)) ⇒ ⊢ (𝜑 → 𝑄 = (◡𝐹 “ { 0 })) | ||
| Theorem | ply1annidl 33695* | The set 𝑄 of polynomials annihilating an element 𝐴 forms an ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } ⇒ ⊢ (𝜑 → 𝑄 ∈ (LIdeal‘𝑃)) | ||
| Theorem | ply1annnr 33696* | The set 𝑄 of polynomials annihilating an element 𝐴 is not the whole polynomial ring. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑃 = (Poly1‘(𝑅 ↾s 𝑆)) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑄 ≠ 𝑈) | ||
| Theorem | ply1annig1p 33697* | The ideal 𝑄 of polynomials annihilating an element 𝐴 is generated by the ideal's canonical generator. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } & ⊢ 𝐾 = (RSpan‘𝑃) & ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹)) ⇒ ⊢ (𝜑 → 𝑄 = (𝐾‘{(𝐺‘𝑄)})) | ||
| Theorem | minplyval 33698* | Expand the value of the minimal polynomial (𝑀‘𝐴) for a given element 𝐴. It is defined as the unique monic polynomial of minimal degree which annihilates 𝐴. By ply1annig1p 33697, that polynomial generates the ideal of the annihilators of 𝐴. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } & ⊢ 𝐾 = (RSpan‘𝑃) & ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) = (𝐺‘𝑄)) | ||
| Theorem | minplycl 33699* | The minimal polynomial is a polynomial. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } & ⊢ 𝐾 = (RSpan‘𝑃) & ⊢ 𝐺 = (idlGen1p‘(𝐸 ↾s 𝐹)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Base‘𝑃)) | ||
| Theorem | ply1annprmidl 33700* | The set 𝑄 of polynomials annihilating an element 𝐴 is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } ⇒ ⊢ (𝜑 → 𝑄 ∈ (PrmIdeal‘𝑃)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |