HomeTheorem List (p. 344 of 513)
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. 344 of 513) | < 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-31550) |
Hilbert Space Explorer
(31551-33073) |
Users' Mathboxes
(33074-51270) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Syntax | cldim 34301 | Extend class notation with the dimension of a vector space. |
| class dim | ||
| Definition | df-dim 34302 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21465, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
| Theorem | dimval 34303 | 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 34304 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 34303 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 34305 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
| Theorem | lmimdim 34306 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lmicdim 34307 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
| ⊢ (𝜑 → 𝑆 ≃𝑚 𝑇) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lvecdim0i 34308 | 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 34309 | 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 34310 | 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 34311* | 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 34312 | 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 | frlmdim 34313 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
| Theorem | tnglvec 34314 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
| Theorem | tngdim 34315 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
| Theorem | rrxdim 34316 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
| Theorem | matdim 34317 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
| Theorem | lbslsat 34318 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 40225 and for example lsatlspsn 40242. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
| Theorem | lsatdim 34319 | 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 34320 | 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 34321 | 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 34322 | 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 34323 | 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 34324* | Lemma for ply1degltdim 34325. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = (deg1‘𝑅) & ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ 𝐸 = (𝑃 ↾s 𝑆) & ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) | ||
| Theorem | ply1degltdim 34325 | 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 34326 | Lemma for lindsun 34327. (Contributed by Thierry Arnoux, 9-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
| Theorem | lindsun 34327 | 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 34328 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 34327. (Contributed by Thierry Arnoux, 17-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
| Theorem | dimkerim 34329 | 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‘𝐾) +e (dim‘𝐼))) | ||
| Theorem | qusdimsum 34330 | 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‘𝑋) +e (dim‘𝑌))) | ||
| Theorem | fedgmullem1 34331* | Lemma for fedgmul 34333. (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 34332* | Lemma for fedgmul 34333. (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 34333 | 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.) Remove dependency on ax-reg 9613. (Revised by Timothy J. O'Malley, 15-Oct-2026.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) & ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ 𝐾 = (𝐸 ↾s 𝑉) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) ⇒ ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶))) | ||
| Theorem | dimlssid 34334 | 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 34335 | 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-1onto𝐵) | ||
| Theorem | lactlmhm 34336* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is a module homomorphism, analogous to ringlghm 20573. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ (𝜑 → 𝐶 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝐴 LMHom 𝐴)) | ||
| Theorem | assalactf1o 34337* | In an associative algebra 𝐴, left-multiplication by a fixed element of the algebra is bijective. See also lactlmhm 34336. (Contributed by Thierry Arnoux, 3-Aug-2025.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ · = (.r‘𝐴) & ⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐶 · 𝑥)) & ⊢ (𝜑 → 𝐴 ∈ AssAlg) & ⊢ 𝐸 = (RLReg‘𝐴) & ⊢ 𝐾 = (Scalar‘𝐴) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → (dim‘𝐴) ∈ ℕ0) & ⊢ (𝜑 → 𝐶 ∈ 𝐸) ⇒ ⊢ (𝜑 → 𝐹:𝐵⟶1-1onto𝐵) | ||
| Theorem | assarrginv 34338 | 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 34339 | 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 34340 | Syntax for the field extension relation. |
| class /FldExt | ||
| Syntax | cfinext 34341 | Syntax for the finite field extension relation. |
| class /FinExt | ||
| Syntax | cextdg 34342 | Syntax for the field extension degree operation. |
| class [:] | ||
| Definition | df-fldext 34343* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
| Definition | df-extdg 34344* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
| Definition | df-finext 34345* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
| Theorem | relfldext 34346 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ Rel /FldExt | ||
| Theorem | brfldext 34347 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
| Theorem | ccfldextrr 34348 | 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 34349 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
| Theorem | fldextfld2 34350 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
| Theorem | fldextsubrg 34351 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
| Theorem | sdrgfldext 34352 | 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 34353 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
| Theorem | brfinext 34354 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
| Theorem | extdgval 34355 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
| Theorem | fldextsdrg 34356 | Deduce sub-division-ring from field extension. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝐵 = (Base‘𝐹) & ⊢ (𝜑 → 𝐸/FldExt𝐹) ⇒ ⊢ (𝜑 → 𝐵 ∈ (SubDRing‘𝐸)) | ||
| Theorem | fldextsralvec 34357 | 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 34358 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
| Theorem | extdggt0 34359 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
| Theorem | fldexttr 34360 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
| Theorem | fldextid 34361 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
| Theorem | extdgid 34362 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
| ⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
| Theorem | fldsdrgfldext 34363 | A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐺 = (𝐹 ↾s 𝐴) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → 𝐹/FldExt𝐺) | ||
| Theorem | fldsdrgfldext2 34364 | 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 34365 | 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 | finextfldext 34366 | A finite field extension is a field extension. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐸/FinExt𝐹) ⇒ ⊢ (𝜑 → 𝐸/FldExt𝐹) | ||
| Theorem | finexttrb 34367 | 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 34368 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
| Theorem | extdg1b 34369 | 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 34370 | 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 34371 | 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 34372 | 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 34373 | 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 34374 | 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 34375* | Lemma for fldextrspunlsp 34376: 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 34376 | Lemma for fldextrspunfld 34378. 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 34377 | Lemma for fldextrspunfld 34378. 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 34378 | 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 34379 | 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 34380 | 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 34381 | 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 34382 | Lemma for fldextrspundgdvds 34383. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0) | ||
| Theorem | fldextrspundgdvds 34383 | 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 34384* | 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 34385 | Integral subring of a ring. |
| class IntgRing | ||
| Definition | df-irng 34386* | 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 34387* | 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 34388* | 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 34389 | 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 34391). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
| Theorem | irngssv 34390 | 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 34391 | 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 34392 | 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 34393* | 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 })) | ||
| Theorem | extdgfialglem1 34394* | Lemma for extdgfialg 34396. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ 𝑍 = (0g‘𝐸) & ⊢ · = (.r‘𝐸) & ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) ⇒ ⊢ (𝜑 → ∃𝑎 ∈ (𝐹 ↑m (0...𝐷))(𝑎 finSupp 𝑍 ∧ ((𝐸 Σg (𝑎 ∘f · 𝐺)) = 𝑍 ∧ 𝑎 ≠ ((0...𝐷) × {𝑍})))) | ||
| Theorem | extdgfialglem2 34395* | Lemma for extdgfialg 34396. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) & ⊢ 𝑍 = (0g‘𝐸) & ⊢ · = (.r‘𝐸) & ⊢ 𝐺 = (𝑛 ∈ (0...𝐷) ↦ (𝑛(.g‘(mulGrp‘((subringAlg ‘𝐸)‘𝐹)))𝑋)) & ⊢ (𝜑 → 𝑋 ∈ 𝐵) & ⊢ (𝜑 → 𝐴:(0...𝐷)⟶𝐹) & ⊢ (𝜑 → 𝐴 finSupp 𝑍) & ⊢ (𝜑 → (𝐸 Σg (𝐴 ∘f · 𝐺)) = 𝑍) & ⊢ (𝜑 → 𝐴 ≠ ((0...𝐷) × {𝑍})) ⇒ ⊢ (𝜑 → 𝑋 ∈ (𝐸 IntgRing 𝐹)) | ||
| Theorem | extdgfialg 34396 | A finite field extension 𝐸 / 𝐹 is algebraic. Part of the proof of Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐷 = (dim‘((subringAlg ‘𝐸)‘𝐹)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐷 ∈ ℕ0) ⇒ ⊢ (𝜑 → (𝐸 IntgRing 𝐹) = 𝐵) | ||
| Syntax | calgext 34397 | Syntax for the algebraic field extension relation. |
| class /AlgExt | ||
| Definition | df-algext 34398* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒 IntgRing (Base‘𝑓)) = (Base‘𝑒))} | ||
| Theorem | bralgext 34399 | Express the fact that a field extension 𝐸 / 𝐹 is algebraic. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ 𝐵 = (Base‘𝐸) & ⊢ 𝐶 = (Base‘𝐹) & ⊢ (𝜑 → 𝐸 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸/AlgExt𝐹 ↔ (𝐸/FldExt𝐹 ∧ (𝐸 IntgRing 𝐶) = 𝐵))) | ||
| Theorem | finextalg 34400 | A finite field extension is algebraic. Proposition 1.1 of [Lang], p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026.) |
| ⊢ (𝜑 → 𝐸/FinExt𝐹) ⇒ ⊢ (𝜑 → 𝐸/AlgExt𝐹) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |