![]() |
Metamath
Proof Explorer Theorem List (p. 334 of 483) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30741) |
![]() (30742-32264) |
![]() (32265-48238) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lmimdim 33301 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
Theorem | lmicdim 33302 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
⊢ (𝜑 → 𝑆 ≃𝑚 𝑇) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
Theorem | lvecdim0i 33303 | 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 33304 | 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 33305 | 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 33306* | 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 33307 | 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 33308 | Obsolete version of rlmdim 33307 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 33309 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
Theorem | tnglvec 33310 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
Theorem | tngdim 33311 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
Theorem | rrxdim 33312 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
Theorem | matdim 33313 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
Theorem | lbslsat 33314 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38448 and for example lsatlspsn 38465. (Contributed by Thierry Arnoux, 20-May-2023.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
Theorem | lsatdim 33315 | 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 33316 | 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 33317 | 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 33318 | 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 33319 | 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 33320* | Lemma for ply1degltdim 33321. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ 𝐸 = (𝑃 ↾s 𝑆) & ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) | ||
Theorem | ply1degltdim 33321 | 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 33322 | Lemma for lindsun 33323. (Contributed by Thierry Arnoux, 9-May-2023.) |
⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
Theorem | lindsun 33323 | 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 33324 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33323. (Contributed by Thierry Arnoux, 17-May-2023.) |
⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
Theorem | dimkerim 33325 | 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 33326 | 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 33327* | Lemma for fedgmul 33329. (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 33328* | Lemma for fedgmul 33329. (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 33329 | The multiplicativity formula for degrees of field extensions. Given 𝐸 a field extension of 𝐹, itself a field extension of 𝐾, we have [𝐸:𝐾] = [𝐸:𝐹][𝐹:𝐾]. Proposition 1.2 of [Lang], p. 224. Here (dim‘𝐴) is the degree of the extension 𝐸 of 𝐾, (dim‘𝐵) is the degree of the extension 𝐸 of 𝐹, and (dim‘𝐶) is the degree of the extension 𝐹 of 𝐾. This proof is valid for infinite dimensions, and is actually valid for division ring extensions, not just field extensions. (Contributed by Thierry Arnoux, 25-Jul-2023.) |
⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑉) & ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐶 = ((subringAlg ‘𝐹)‘𝑉) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ 𝐾 = (𝐸 ↾s 𝑉) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝐾 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ (𝜑 → 𝑉 ∈ (SubRing‘𝐹)) ⇒ ⊢ (𝜑 → (dim‘𝐴) = ((dim‘𝐵) ·e (dim‘𝐶))) | ||
Syntax | cfldext 33330 | Syntax for the field extension relation. |
class /FldExt | ||
Syntax | cfinext 33331 | Syntax for the finite field extension relation. |
class /FinExt | ||
Syntax | calgext 33332 | Syntax for the algebraic field extension relation. |
class /AlgExt | ||
Syntax | cextdg 33333 | Syntax for the field extension degree operation. |
class [:] | ||
Definition | df-fldext 33334* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /FldExt = {〈𝑒, 𝑓〉 ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
Definition | df-extdg 33335* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
Definition | df-finext 33336* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /FinExt = {〈𝑒, 𝑓〉 ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
Definition | df-algext 33337* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ /AlgExt = {〈𝑒, 𝑓〉 ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))} | ||
Theorem | relfldext 33338 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ Rel /FldExt | ||
Theorem | brfldext 33339 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
Theorem | ccfldextrr 33340 | 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 33341 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
Theorem | fldextfld2 33342 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
Theorem | fldextsubrg 33343 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
Theorem | fldextress 33344 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
Theorem | brfinext 33345 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
Theorem | extdgval 33346 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
Theorem | fldextsralvec 33347 | 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 33348 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
Theorem | extdggt0 33349 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
Theorem | fldexttr 33350 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
Theorem | fldextid 33351 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
Theorem | extdgid 33352 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
Theorem | extdgmul 33353 | 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 33354 | 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 33355 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
Theorem | extdg1b 33356 | The degree of the extension 𝐸/FldExt𝐹 is 1 iff 𝐸 and 𝐹 are the same structure. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
⊢ (𝐸/FldExt𝐹 → ((𝐸[:]𝐹) = 1 ↔ 𝐸 = 𝐹)) | ||
Theorem | fldextchr 33357 | 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 33358 | 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 33359 | 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 33360 | 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 33361 | Integral subring of a ring. |
class IntgRing | ||
Definition | df-irng 33362* | 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 33363* | 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 33364* | 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 33365 | 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 33367). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
Theorem | irngssv 33366 | 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 33367 | 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 33368 | 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 33369* | 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 33370 | Extend class notation with the minimal polynomial builder function. |
class minPoly | ||
Definition | df-minply 33371* | 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 33372* | 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 33373* | 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 33374* | 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 33375* | 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 33376* | 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 33375, 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 33377* | 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 33378* | 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 | minplyann 33379 | The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.) |
⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) ⇒ ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 ) | ||
Theorem | minplyirredlem 33380 | Lemma for minplyirred 33381. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) & ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃)) & ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃)) & ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴)) & ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸)) & ⊢ (𝜑 → 𝐺 ≠ 𝑍) & ⊢ (𝜑 → 𝐻 ≠ 𝑍) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃)) | ||
Theorem | minplyirred 33381 | A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃)) | ||
Theorem | irngnminplynz 33382 | Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
⊢ 𝑍 = (0g‘(Poly1‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) | ||
Theorem | minplym1p 33383 | A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝑍 = (0g‘(Poly1‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹)) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈) | ||
Theorem | irredminply 33384 | An irreductible, monic, annihilating polynomial is the minimal polynomial. (Contributed by Thierry Arnoux, 27-Apr-2025.) |
⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = 0 ) & ⊢ (𝜑 → 𝐺 ∈ (Irred‘𝑃)) & ⊢ (𝜑 → 𝐺 ∈ (Monic1p‘(𝐸 ↾s 𝐹))) ⇒ ⊢ (𝜑 → 𝐺 = (𝑀‘𝐴)) | ||
Theorem | algextdeglem1 33385 | Lemma for algextdeg 33393. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) ⇒ ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾) | ||
Theorem | algextdeglem2 33386* | Lemma for algextdeg 33393. Both the ring of polynomials 𝑃 and the field 𝐿 generated by 𝐾 and the algebraic element 𝐴 can be considered as modules over the elements of 𝐹. Then, the evaluation map 𝐺, mapping polynomials to their evaluation at 𝐴, is a module homomorphism between those modules. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) ⇒ ⊢ (𝜑 → 𝐺 ∈ (𝑃 LMHom ((subringAlg ‘𝐿)‘𝐹))) | ||
Theorem | algextdeglem3 33387* | Lemma for algextdeg 33393. The quotient 𝑃 / 𝑍 of the vector space 𝑃 of polynomials by the subspace 𝑍 of polynomials annihilating 𝐴 is itself a vector space. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) ⇒ ⊢ (𝜑 → 𝑄 ∈ LVec) | ||
Theorem | algextdeglem4 33388* | Lemma for algextdeg 33393. By lmhmqusker 33140, the surjective module homomorphism 𝐺 described in algextdeglem2 33386 induces an isomorphism with the quotient space. Therefore, the dimension of that quotient space 𝑃 / 𝑍 is the degree of the algebraic field extension. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) ⇒ ⊢ (𝜑 → (dim‘𝑄) = (𝐿[:]𝐾)) | ||
Theorem | algextdeglem5 33389* | Lemma for algextdeg 33393. The subspace 𝑍 of annihilators of 𝐴 is a principal ideal generated by the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) ⇒ ⊢ (𝜑 → 𝑍 = ((RSpan‘𝑃)‘{(𝑀‘𝐴)})) | ||
Theorem | algextdeglem6 33390* | Lemma for algextdeg 33393. By r1pquslmic 33281, the univariate polynomial remainder ring (𝐻 “s 𝑃) is isomorphic with the quotient ring 𝑄. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) & ⊢ 𝑅 = (rem1p‘𝐾) & ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴))) ⇒ ⊢ (𝜑 → (dim‘𝑄) = (dim‘(𝐻 “s 𝑃))) | ||
Theorem | algextdeglem7 33391* | Lemma for algextdeg 33393. The polynomials 𝑋 of lower degree than the minimal polynomial are left unchanged when taking the remainder of the division by that minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) & ⊢ 𝑅 = (rem1p‘𝐾) & ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴))) & ⊢ 𝑇 = (◡( deg1 ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) & ⊢ (𝜑 → 𝑋 ∈ 𝑈) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝑇 ↔ (𝐻‘𝑋) = 𝑋)) | ||
Theorem | algextdeglem8 33392* | Lemma for algextdeg 33393. The dimension of the univariate polynomial remainder ring (𝐻 “s 𝑃) is the degree of the minimal polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐺 = (𝑝 ∈ 𝑈 ↦ ((𝑂‘𝑝)‘𝐴)) & ⊢ 𝑁 = (𝑥 ∈ 𝑈 ↦ [𝑥](𝑃 ~QG 𝑍)) & ⊢ 𝑍 = (◡𝐺 “ {(0g‘𝐿)}) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝑍)) & ⊢ 𝐽 = (𝑝 ∈ (Base‘𝑄) ↦ ∪ (𝐺 “ 𝑝)) & ⊢ 𝑅 = (rem1p‘𝐾) & ⊢ 𝐻 = (𝑝 ∈ 𝑈 ↦ (𝑝𝑅(𝑀‘𝐴))) & ⊢ 𝑇 = (◡( deg1 ‘𝐾) “ (-∞[,)(𝐷‘(𝑀‘𝐴)))) ⇒ ⊢ (𝜑 → (dim‘(𝐻 “s 𝑃)) = (𝐷‘(𝑀‘𝐴))) | ||
Theorem | algextdeg 33393 | The degree of an algebraic field extension (noted [𝐿:𝐾]) is the degree of the minimal polynomial 𝑀(𝐴), whereas 𝐿 is the field generated by 𝐾 and the algebraic element 𝐴. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = ( deg1 ‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) ⇒ ⊢ (𝜑 → (𝐿[:]𝐾) = (𝐷‘(𝑀‘𝐴))) | ||
Syntax | csmat 33394 | Syntax for a function generating submatrices. |
class subMat1 | ||
Definition | df-smat 33395* | Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ((1...𝑀) × (1...𝑁)) into a new index in ((1...(𝑀 − 1)) × (1...(𝑁 − 1))). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 22492. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))〉)))) | ||
Theorem | smatfval 33396* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | ||
Theorem | smatrcl 33397 | Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) ⇒ ⊢ (𝜑 → 𝑆 ∈ (𝐵 ↑m ((1...(𝑀 − 1)) × (1...(𝑁 − 1))))) | ||
Theorem | smatlem 33398 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) & ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) | ||
Theorem | smattl 33399 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽)) | ||
Theorem | smattr 33400 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |