HomeTheorem List (p. 335 of 485)
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. 335 of 485) | < 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-30800) |
Hilbert Space Explorer
(30801-32323) |
Users' Mathboxes
(32324-48424) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | deg1addlt 33401 | If both factors have degree bounded by 𝐿, then the sum of the polynomials also has degree bounded by 𝐿. See also deg1addle 26081. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑌 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ 𝐵 = (Base‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ (𝜑 → 𝐺 ∈ 𝐵) & ⊢ (𝜑 → 𝐿 ∈ ℝ*) & ⊢ (𝜑 → (𝐷‘𝐹) < 𝐿) & ⊢ (𝜑 → (𝐷‘𝐺) < 𝐿) ⇒ ⊢ (𝜑 → (𝐷‘(𝐹 + 𝐺)) < 𝐿) | ||
| Theorem | ig1pnunit 33402 | The polynomial ideal generator is not a unit polynomial. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃)) & ⊢ (𝜑 → 𝐼 ≠ 𝑈) ⇒ ⊢ (𝜑 → ¬ (𝐺‘𝐼) ∈ (Unit‘𝑃)) | ||
| Theorem | ig1pmindeg 33403 | The polynomial ideal generator is of minimum degree. (Contributed by Thierry Arnoux, 19-Mar-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐺 = (idlGen1p‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑃)) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 0 = (0g‘𝑃) & ⊢ (𝜑 → 𝐹 ∈ 𝐼) & ⊢ (𝜑 → 𝐹 ≠ 0 ) ⇒ ⊢ (𝜑 → (𝐷‘(𝐺‘𝐼)) ≤ (𝐷‘𝐹)) | ||
| Theorem | q1pdir 33404 | Distribution of univariate polynomial quotient over addition. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ + = (+g‘𝑃) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) / 𝐶) = ((𝐴 / 𝐶) + (𝐵 / 𝐶))) | ||
| Theorem | q1pvsca 33405 | Scalar multiplication property of the polynomial division. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ / = (quot1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴) / 𝐶) = (𝐵 × (𝐴 / 𝐶))) | ||
| Theorem | r1pvsca 33406 | Scalar multiplication property of the polynomial remainder operation. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) ⇒ ⊢ (𝜑 → ((𝐵 × 𝐴)𝐸𝐷) = (𝐵 × (𝐴𝐸𝐷))) | ||
| Theorem | r1p0 33407 | Polynomial remainder operation of a division of the zero polynomial. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (𝜑 → ( 0 𝐸𝐷) = 0 ) | ||
| Theorem | r1pcyc 33408 | The polynomial remainder operation is periodic. See modcyc 13907. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + (𝐶 · 𝐵))𝐸𝐵) = (𝐴𝐸𝐵)) | ||
| Theorem | r1padd1 33409 | Addition property of the polynomial remainder operation, similar to modadd1 13909. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐷 ∈ 𝑁) & ⊢ (𝜑 → (𝐴𝐸𝐷) = (𝐵𝐸𝐷)) & ⊢ + = (+g‘𝑃) & ⊢ (𝜑 → 𝐵 ∈ 𝑈) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐶)𝐸𝐷) = ((𝐵 + 𝐶)𝐸𝐷)) | ||
| Theorem | r1pid2 33410 | Identity law for polynomial remainder operation: it leaves a polynomial 𝐴 unchanged iff the degree of 𝐴 is less than the degree of the divisor 𝐵. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ IDomn) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ (𝜑 → 𝐴 ∈ 𝑈) & ⊢ (𝜑 → 𝐵 ∈ 𝑁) ⇒ ⊢ (𝜑 → ((𝐴𝐸𝐵) = 𝐴 ↔ (𝐷‘𝐴) < (𝐷‘𝐵))) | ||
| Theorem | r1plmhm 33411* | The univariate polynomial remainder function 𝐹 is a module homomorphism. Its image (𝐹 “s 𝑃) is sometimes called the "ring of remainders" (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑁) ⇒ ⊢ (𝜑 → 𝐹 ∈ (𝑃 LMHom (𝐹 “s 𝑃))) | ||
| Theorem | r1pquslmic 33412* | The univariate polynomial remainder ring (𝐹 “s 𝑃) is module isomorphic with the quotient ring. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ 𝐸 = (rem1p‘𝑅) & ⊢ 𝑁 = (Unic1p‘𝑅) & ⊢ 𝐹 = (𝑓 ∈ 𝑈 ↦ (𝑓𝐸𝑀)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝑁) & ⊢ 0 = (0g‘𝑃) & ⊢ 𝐾 = (◡𝐹 “ { 0 }) & ⊢ 𝑄 = (𝑃 /s (𝑃 ~QG 𝐾)) ⇒ ⊢ (𝜑 → 𝑄 ≃𝑚 (𝐹 “s 𝑃)) | ||
| Theorem | sra1r 33413 | The unity element of a subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 1 = (1r‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 1 = (1r‘𝐴)) | ||
| Theorem | sradrng 33414 | Condition for a subring algebra to be a division ring. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝑅)‘𝑉) & ⊢ 𝐵 = (Base‘𝑅) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝑉 ⊆ 𝐵) → 𝐴 ∈ DivRing) | ||
| Theorem | srasubrg 33415 | A subring of the original structure is also a subring of the constructed subring algebra. (Contributed by Thierry Arnoux, 24-Jul-2023.) |
| ⊢ (𝜑 → 𝐴 = ((subringAlg ‘𝑊)‘𝑆)) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝑊)) & ⊢ (𝜑 → 𝑆 ⊆ (Base‘𝑊)) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐴)) | ||
| Theorem | sralvec 33416 | Given a sub division ring 𝐹 of a division ring 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ DivRing ∧ 𝐹 ∈ DivRing ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | srafldlvec 33417 | Given a subfield 𝐹 of a field 𝐸, 𝐸 may be considered as a vector space over 𝐹, which becomes the field of scalars. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐴 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) ⇒ ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field ∧ 𝑈 ∈ (SubRing‘𝐸)) → 𝐴 ∈ LVec) | ||
| Theorem | resssra 33418 | The subring algebra of a restricted structure is the restriction of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ⊆ 𝐴) & ⊢ (𝜑 → 𝐶 ⊆ 𝐵) & ⊢ (𝜑 → 𝑅 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((subringAlg ‘𝑆)‘𝐶) = (((subringAlg ‘𝑅)‘𝐶) ↾s 𝐵)) | ||
| Theorem | lsssra 33419 | A subring is a subspace of the subring algebra. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑊 = ((subringAlg ‘𝑅)‘𝐶) & ⊢ 𝐴 = (Base‘𝑅) & ⊢ 𝑆 = (𝑅 ↾s 𝐵) & ⊢ (𝜑 → 𝐵 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝐶 ∈ (SubRing‘𝑆)) ⇒ ⊢ (𝜑 → 𝐵 ∈ (LSubSp‘𝑊)) | ||
| Theorem | drgext0g 33420 | The additive neutral element of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐸) = (0g‘𝐵)) | ||
| Theorem | drgextvsca 33421 | The scalar multiplication operation of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (.r‘𝐸) = ( ·𝑠 ‘𝐵)) | ||
| Theorem | drgext0gsca 33422 | The additive neutral element of the scalar field of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) ⇒ ⊢ (𝜑 → (0g‘𝐵) = (0g‘(Scalar‘𝐵))) | ||
| Theorem | drgextsubrg 33423 | The scalar field is a subring of a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐵)) | ||
| Theorem | drgextlsp 33424 | The scalar field is a subspace of a subring algebra. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) ⇒ ⊢ (𝜑 → 𝑈 ∈ (LSubSp‘𝐵)) | ||
| Theorem | drgextgsum 33425* | Group sum in a division ring extension. (Contributed by Thierry Arnoux, 17-Jul-2023.) |
| ⊢ 𝐵 = ((subringAlg ‘𝐸)‘𝑈) & ⊢ (𝜑 → 𝐸 ∈ DivRing) & ⊢ (𝜑 → 𝑈 ∈ (SubRing‘𝐸)) & ⊢ 𝐹 = (𝐸 ↾s 𝑈) & ⊢ (𝜑 → 𝐹 ∈ DivRing) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) ⇒ ⊢ (𝜑 → (𝐸 Σg (𝑖 ∈ 𝑋 ↦ 𝑌)) = (𝐵 Σg (𝑖 ∈ 𝑋 ↦ 𝑌))) | ||
| Theorem | lvecdimfi 33426 | Finite version of lvecdim 21057 which does not require the axiom of choice. The axiom of choice is used in acsmapd 18549, which is required in the infinite case. Suggested by Gérard Lang. (Contributed by Thierry Arnoux, 24-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑆 ∈ 𝐽) & ⊢ (𝜑 → 𝑇 ∈ 𝐽) & ⊢ (𝜑 → 𝑆 ∈ Fin) ⇒ ⊢ (𝜑 → 𝑆 ≈ 𝑇) | ||
| Syntax | cldim 33427 | Extend class notation with the dimension of a vector space. |
| class dim | ||
| Definition | df-dim 33428 | Define the dimension of a vector space as the cardinality of its bases. Note that by lvecdim 21057, all bases are equinumerous. (Contributed by Thierry Arnoux, 6-May-2023.) |
| ⊢ dim = (𝑓 ∈ V ↦ ∪ (♯ “ (LBasis‘𝑓))) | ||
| Theorem | dimval 33429 | 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 33430 | The dimension of a vector space 𝐹 is the cardinality of one of its bases. This version of dimval 33429 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 33431 | Closure of the vector space dimension. (Contributed by Thierry Arnoux, 18-May-2023.) |
| ⊢ (𝑉 ∈ LVec → (dim‘𝑉) ∈ ℕ0*) | ||
| Theorem | lmimdim 33432 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Feb-2025.) |
| ⊢ (𝜑 → 𝐹 ∈ (𝑆 LMIso 𝑇)) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lmicdim 33433 | Module isomorphisms preserve vector space dimensions. (Contributed by Thierry Arnoux, 25-Mar-2025.) |
| ⊢ (𝜑 → 𝑆 ≃𝑚 𝑇) & ⊢ (𝜑 → 𝑆 ∈ LVec) ⇒ ⊢ (𝜑 → (dim‘𝑆) = (dim‘𝑇)) | ||
| Theorem | lvecdim0i 33434 | 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 33435 | 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 33436 | 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 33437* | 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 33438 | 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 33439 | Obsolete version of rlmdim 33438 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 33440 | Dimension of a free left module. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐹 = (𝑅 freeLMod 𝐼) ⇒ ⊢ ((𝑅 ∈ DivRing ∧ 𝐼 ∈ 𝑉) → (dim‘𝐹) = (♯‘𝐼)) | ||
| Theorem | tnglvec 33441 | Augmenting a structure with a norm conserves left vector spaces. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ (𝑁 ∈ 𝑉 → (𝐺 ∈ LVec ↔ 𝑇 ∈ LVec)) | ||
| Theorem | tngdim 33442 | Dimension of a left vector space augmented with a norm. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑇 = (𝐺 toNrmGrp 𝑁) ⇒ ⊢ ((𝐺 ∈ LVec ∧ 𝑁 ∈ 𝑉) → (dim‘𝐺) = (dim‘𝑇)) | ||
| Theorem | rrxdim 33443 | Dimension of the generalized Euclidean space. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → (dim‘𝐻) = (♯‘𝐼)) | ||
| Theorem | matdim 33444 | Dimension of the space of square matrices. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝐴 = (𝐼 Mat 𝑅) & ⊢ 𝑁 = (♯‘𝐼) ⇒ ⊢ ((𝐼 ∈ Fin ∧ 𝑅 ∈ DivRing) → (dim‘𝐴) = (𝑁 · 𝑁)) | ||
| Theorem | lbslsat 33445 | A nonzero vector 𝑋 is a basis of a line spanned by the singleton 𝑋. Spans of nonzero singletons are sometimes called "atoms", see df-lsatoms 38578 and for example lsatlspsn 38595. (Contributed by Thierry Arnoux, 20-May-2023.) |
| ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ 𝑌 = (𝑊 ↾s (𝑁‘{𝑋})) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝑋 ∈ 𝑉 ∧ 𝑋 ≠ 0 ) → {𝑋} ∈ (LBasis‘𝑌)) | ||
| Theorem | lsatdim 33446 | 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 33447 | 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 33448 | 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 33449 | 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 33450 | 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 33451* | Lemma for ply1degltdim 33452. (Contributed by Thierry Arnoux, 20-Feb-2025.) |
| ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐷 = ( deg1 ‘𝑅) & ⊢ 𝑆 = (◡𝐷 “ (-∞[,)𝑁)) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑅 ∈ DivRing) & ⊢ 𝐸 = (𝑃 ↾s 𝑆) & ⊢ 𝐹 = (𝑛 ∈ (0..^𝑁) ↦ (𝑛(.g‘(mulGrp‘𝑃))(var1‘𝑅))) ⇒ ⊢ (𝜑 → ran 𝐹 ∈ (LBasis‘𝐸)) | ||
| Theorem | ply1degltdim 33452 | 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 33453 | Lemma for lindsun 33454. (Contributed by Thierry Arnoux, 9-May-2023.) |
| ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ LVec) & ⊢ (𝜑 → 𝑈 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → 𝑉 ∈ (LIndS‘𝑊)) & ⊢ (𝜑 → ((𝑁‘𝑈) ∩ (𝑁‘𝑉)) = { 0 }) & ⊢ 𝑂 = (0g‘(Scalar‘𝑊)) & ⊢ 𝐹 = (Base‘(Scalar‘𝑊)) & ⊢ (𝜑 → 𝐶 ∈ 𝑈) & ⊢ (𝜑 → 𝐾 ∈ (𝐹 ∖ {𝑂})) & ⊢ (𝜑 → (𝐾( ·𝑠 ‘𝑊)𝐶) ∈ (𝑁‘((𝑈 ∪ 𝑉) ∖ {𝐶}))) ⇒ ⊢ (𝜑 → ⊥) | ||
| Theorem | lindsun 33454 | 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 33455 | The linear spans of two disjunct independent sets only have a trivial intersection. This can be seen as the opposite direction of lindsun 33454. (Contributed by Thierry Arnoux, 17-May-2023.) |
| ⊢ 𝐽 = (LBasis‘𝑊) & ⊢ 𝑁 = (LSpan‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ LVec ∧ 𝐵 ∈ 𝐽 ∧ 𝑉 ⊆ 𝐵) → ((𝑁‘(𝐵 ∖ 𝑉)) ∩ (𝑁‘𝑉)) = { 0 }) | ||
| Theorem | dimkerim 33456 | 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 33457 | 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 33458* | Lemma for fedgmul 33460. (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 33459* | Lemma for fedgmul 33460. (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 33460 | 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 33461 | Syntax for the field extension relation. |
| class /FldExt | ||
| Syntax | cfinext 33462 | Syntax for the finite field extension relation. |
| class /FinExt | ||
| Syntax | calgext 33463 | Syntax for the algebraic field extension relation. |
| class /AlgExt | ||
| Syntax | cextdg 33464 | Syntax for the field extension degree operation. |
| class [:] | ||
| Definition | df-fldext 33465* | Definition of the field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FldExt = {⟨𝑒, 𝑓⟩ ∣ ((𝑒 ∈ Field ∧ 𝑓 ∈ Field) ∧ (𝑓 = (𝑒 ↾s (Base‘𝑓)) ∧ (Base‘𝑓) ∈ (SubRing‘𝑒)))} | ||
| Definition | df-extdg 33466* | Definition of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ [:] = (𝑒 ∈ V, 𝑓 ∈ (/FldExt “ {𝑒}) ↦ (dim‘((subringAlg ‘𝑒)‘(Base‘𝑓)))) | ||
| Definition | df-finext 33467* | Definition of the finite field extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /FinExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ (𝑒[:]𝑓) ∈ ℕ0)} | ||
| Definition | df-algext 33468* | Definition of the algebraic extension relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ /AlgExt = {⟨𝑒, 𝑓⟩ ∣ (𝑒/FldExt𝑓 ∧ ∀𝑥 ∈ (Base‘𝑒)∃𝑝 ∈ (Poly1‘𝑓)(((eval1‘𝑓)‘𝑝)‘𝑥) = (0g‘𝑒))} | ||
| Theorem | relfldext 33469 | The field extension is a relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ Rel /FldExt | ||
| Theorem | brfldext 33470 | The field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸 ∈ Field ∧ 𝐹 ∈ Field) → (𝐸/FldExt𝐹 ↔ (𝐹 = (𝐸 ↾s (Base‘𝐹)) ∧ (Base‘𝐹) ∈ (SubRing‘𝐸)))) | ||
| Theorem | ccfldextrr 33471 | 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 33472 | A field extension is only defined if the extension is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐸 ∈ Field) | ||
| Theorem | fldextfld2 33473 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
| Theorem | fldextsubrg 33474 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
| Theorem | fldextress 33475 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
| Theorem | brfinext 33476 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
| Theorem | extdgval 33477 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
| Theorem | fldextsralvec 33478 | 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 33479 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
| Theorem | extdggt0 33480 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
| Theorem | fldexttr 33481 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
| Theorem | fldextid 33482 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
| Theorem | extdgid 33483 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
| ⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
| Theorem | extdgmul 33484 | 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 33485 | 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 33486 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
| Theorem | extdg1b 33487 | 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 33488 | 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 33489 | 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 33490 | 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 33491 | 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 33492 | Integral subring of a ring. |
| class IntgRing | ||
| Definition | df-irng 33493* | 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 33494* | 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 33495* | 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 33496 | 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 33498). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
| Theorem | irngssv 33497 | 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 33498 | 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 33499 | 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 33500* | 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 })) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |