HomeTheorem List (p. 337 of 498)
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 498) | < 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-30847) |
Hilbert Space Explorer
(30848-32370) |
Users' Mathboxes
(32371-49794) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | lvecdim0i 33601 | 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 33602 | 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 33603 | 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 33604* | 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 33605 | 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 33606 | Obsolete version of rlmdim 33605 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 33607 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
| Theorem | tnglvec 33608 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
| Theorem | tngdim 33609 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
| Theorem | rrxdim 33610 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
| Theorem | matdim 33611 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
| Theorem | lbslsat 33612 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38969 and for example lsatlspsn 38986. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
| Theorem | lsatdim 33613 | 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 33614 | 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 33615 | 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 33616 | 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 33617 | 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 33618* | Lemma for ply1degltdim 33619. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ 𝐸 = (𝑃 ↾s 𝑆) & ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) | ||
| Theorem | ply1degltdim 33619 | 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 33620 | Lemma for lindsun 33621. (Contributed by Thierry Arnoux, 9-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
| Theorem | lindsun 33621 | 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 33622 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33621. (Contributed by Thierry Arnoux, 17-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
| Theorem | dimkerim 33623 | 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 33624 | 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 33625* | Lemma for fedgmul 33627. (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 33626* | Lemma for fedgmul 33627. (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 33627 | 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 33628 | 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 33629 | 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 33630* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20221. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴)) | ||
| Theorem | assalactf1o 33631* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 33630. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ 𝐸 = (RLReg‘𝐴) & ⊢ 𝐾 = (Scalar‘𝐴) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐵–1-1-onto→𝐵) | ||
| Theorem | assarrginv 33632 | 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 33633 | 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 33634 | Syntax for the field extension relation. |
| class /FldExt | ||
| Syntax | cfinext 33635 | Syntax for the finite field extension relation. |
| class /FinExt | ||
| Syntax | cextdg 33636 | Syntax for the field extension degree operation. |
| class [:] | ||
| Definition | df-fldext 33637* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
| Definition | df-extdg 33638* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
| Definition | df-finext 33639* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
| Theorem | relfldext 33640 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ Rel /FldExt | ||
| Theorem | brfldext 33641 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
| Theorem | ccfldextrr 33642 | 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 33643 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
| Theorem | fldextfld2 33644 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
| Theorem | fldextsubrg 33645 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
| Theorem | sdrgfldext 33646 | A field 𝐸 and any sub-division-ring 𝐹 of 𝐸 form a field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) ⇒ ⊢ (𝜑 → 𝐸/FldExt(𝐸 ↾s 𝐹)) | ||
| Theorem | fldextress 33647 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
| Theorem | brfinext 33648 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
| Theorem | extdgval 33649 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
| Theorem | fldextsdrg 33650 | Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐸/FldExt𝐹) ⇒ ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐸)) | ||
| Theorem | fldextsralvec 33651 | 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 33652 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
| Theorem | extdggt0 33653 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
| Theorem | fldexttr 33654 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
| Theorem | fldextid 33655 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
| Theorem | extdgid 33656 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
| ⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
| Theorem | fldsdrgfldext 33657 | A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐺 = (𝐹 ↾s 𝐴) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → 𝐹/FldExt𝐺) | ||
| Theorem | fldsdrgfldext2 33658 | A sub-sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐺 = (𝐹 ↾s 𝐴) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹)) & ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐺)) & ⊢ 𝐻 = (𝐹 ↾s 𝐵) ⇒ ⊢ (𝜑 → 𝐺/FldExt𝐻) | ||
| Theorem | extdgmul 33659 | 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 33660 | 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 33661 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
| Theorem | extdg1b 33662 | 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 33663 | 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 33664 | 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 33665 | 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 33666 | 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 33667 | 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 | ||
| Theorem | fldextrspunlsplem 33668* | Lemma for fldextrspunlsp 33669: First direction. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ 𝑁 = (RingSpan‘𝐿) & ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)) & ⊢ 𝐸 = (𝐿 ↾s 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) & ⊢ (𝜑 → 𝐵 ∈ Fin) & ⊢ (𝜑 → 𝑃:𝐻⟶𝐺) & ⊢ (𝜑 → 𝑃 finSupp (0g‘𝐿)) & ⊢ (𝜑 → 𝑋 = (𝐿 Σg (𝑓 ∈ 𝐻 ↦ ((𝑃‘𝑓)(.r‘𝐿)𝑓)))) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ (𝐺 ↑m 𝐵)(𝑎 finSupp (0g‘𝐿) ∧ 𝑋 = (𝐿 Σg (𝑏 ∈ 𝐵 ↦ ((𝑎‘𝑏)(.r‘𝐿)𝑏))))) | ||
| Theorem | fldextrspunlsp 33669 | Lemma for fldextrspunfld 33671. The subring generated by the union of two field extensions 𝐺 and 𝐻 is the vector sub- 𝐺 space generated by a basis 𝐵 of 𝐻. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ 𝑁 = (RingSpan‘𝐿) & ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)) & ⊢ 𝐸 = (𝐿 ↾s 𝐶) & ⊢ (𝜑 → 𝐵 ∈ (LBasis‘((subringAlg ‘𝐽)‘𝐹))) & ⊢ (𝜑 → 𝐵 ∈ Fin) ⇒ ⊢ (𝜑 → 𝐶 = ((LSpan‘((subringAlg ‘𝐿)‘𝐺))‘𝐵)) | ||
| Theorem | fldextrspunlem1 33670 | Lemma for fldextrspunfld 33671. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝑁 = (RingSpan‘𝐿) & ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)) & ⊢ 𝐸 = (𝐿 ↾s 𝐶) ⇒ ⊢ (𝜑 → (dim‘((subringAlg ‘𝐸)‘𝐺)) ≤ (𝐽[:]𝐾)) | ||
| Theorem | fldextrspunfld 33671 | The ring generated by the union of two field extensions is a field. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝑁 = (RingSpan‘𝐿) & ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)) & ⊢ 𝐸 = (𝐿 ↾s 𝐶) ⇒ ⊢ (𝜑 → 𝐸 ∈ Field) | ||
| Theorem | fldextrspunlem2 33672 | Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝑁 = (RingSpan‘𝐿) & ⊢ 𝐶 = (𝑁‘(𝐺 ∪ 𝐻)) & ⊢ 𝐸 = (𝐿 ↾s 𝐶) ⇒ ⊢ (𝜑 → 𝐶 = (𝐿 fldGen (𝐺 ∪ 𝐻))) | ||
| Theorem | fldextrspundgle 33673 | Inequality involving the degree of two different field extensions 𝐼 and 𝐽 of a same field 𝐹. Part of the proof of Proposition 5, Chapter 5, of [BourbakiAlg2] p. 116. (Contributed by Thierry Arnoux, 13-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) ⇒ ⊢ (𝜑 → (𝐸[:]𝐼) ≤ (𝐽[:]𝐾)) | ||
| Theorem | fldextrspundglemul 33674 | Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, 𝐽 / 𝐾 being finite, and the composiste field 𝐸 = 𝐼𝐽, the degree of the extension of the composite field 𝐸 / 𝐾 is at most the product of the field extension degrees of 𝐼 / 𝐾 and 𝐽 / 𝐾. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) ⇒ ⊢ (𝜑 → (𝐸[:]𝐾) ≤ ((𝐼[:]𝐾) ·e (𝐽[:]𝐾))) | ||
| Theorem | fldextrspundgdvdslem 33675 | Lemma for fldextrspundgdvds 33676. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0) | ||
| Theorem | fldextrspundgdvds 33676 | Given two finite extensions 𝐼 / 𝐾 and 𝐽 / 𝐾 of the same field 𝐾, the degree of the extension 𝐼 / 𝐾 divides the degree of the extension 𝐸 / 𝐾, 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐼[:]𝐾) ∥ (𝐸[:]𝐾)) | ||
| Theorem | fldext2rspun 33677* | Given two field extensions 𝐼 / 𝐾 and 𝐽 / 𝐾, 𝐼 / 𝐾 being a quadratic extension, and the degree of 𝐽 / 𝐾 being a power of 2, the degree of the extension 𝐸 / 𝐾 is a power of 2 , 𝐸 being the composite field 𝐼𝐽. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → (𝐼[:]𝐾) = 2) & ⊢ (𝜑 → (𝐽[:]𝐾) = (2↑𝑁)) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ0 (𝐸[:]𝐾) = (2↑𝑛)) | ||
| Syntax | cirng 33678 | Integral subring of a ring. |
| class IntgRing | ||
| Definition | df-irng 33679* | 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 33680* | 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 33681* | 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 33682 | 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 33684). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
| Theorem | irngssv 33683 | 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 33684 | 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 33685 | 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 33686* | 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 | calgext 33687 | Syntax for the algebraic field extension relation. |
| class /AlgExt | ||
| Definition | df-algext 33688* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing 𝑓) = (Base‘𝑒))} | ||
| Syntax | cminply 33689 | Extend class notation with the minimal polynomial builder function. |
| class minPoly | ||
| Definition | df-minply 33690* | 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 33691* | 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 33692* | 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 33693* | 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 33694* | 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 33695* | 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 33694, 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 33696* | 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 33697* | 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‘𝑃)) | ||
| Theorem | minplymindeg 33698 | The minimal polynomial of 𝐴 is minimal among the nonzero annihilators of 𝐴 with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝐷 = (deg1‘(𝐸 ↾s 𝐹)) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → ((𝑂‘𝐻)‘𝐴) = 0 ) & ⊢ (𝜑 → 𝐻 ∈ 𝑈) & ⊢ (𝜑 → 𝐻 ≠ 𝑍) ⇒ ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ≤ (𝐷‘𝐻)) | ||
| Theorem | minplyann 33699 | The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) ⇒ ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 ) | ||
| Theorem | minplyirredlem 33700 | Lemma for minplyirred 33701. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) & ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃)) & ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃)) & ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴)) & ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸)) & ⊢ (𝜑 → 𝐺 ≠ 𝑍) & ⊢ (𝜑 → 𝐻 ≠ 𝑍) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |