| Metamath
Proof Explorer Theorem List (p. 338 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | fldextfld2 33701 | A field extension is only defined if the subfield is a field. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 ∈ Field) | ||
| Theorem | fldextsubrg 33702 | Field extension implies a subring relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ 𝑈 = (Base‘𝐹) ⇒ ⊢ (𝐸/FldExt𝐹 → 𝑈 ∈ (SubRing‘𝐸)) | ||
| Theorem | fldextress 33703 | Field extension implies a structure restriction relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 𝐹 = (𝐸 ↾s (Base‘𝐹))) | ||
| Theorem | brfinext 33704 | The finite field extension relation explicited. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸/FinExt𝐹 ↔ (𝐸[:]𝐹) ∈ ℕ0)) | ||
| Theorem | extdgval 33705 | Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) = (dim‘((subringAlg ‘𝐸)‘(Base‘𝐹)))) | ||
| Theorem | fldextsralvec 33706 | 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 33707 | Closure of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → (𝐸[:]𝐹) ∈ ℕ0*) | ||
| Theorem | extdggt0 33708 | Degrees of field extension are greater than zero. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐸/FldExt𝐹 → 0 < (𝐸[:]𝐹)) | ||
| Theorem | fldexttr 33709 | Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ 𝐹/FldExt𝐾) → 𝐸/FldExt𝐾) | ||
| Theorem | fldextid 33710 | The field extension relation is reflexive. (Contributed by Thierry Arnoux, 30-Jul-2023.) |
| ⊢ (𝐹 ∈ Field → 𝐹/FldExt𝐹) | ||
| Theorem | extdgid 33711 | A trivial field extension has degree one. (Contributed by Thierry Arnoux, 4-Aug-2023.) |
| ⊢ (𝐸 ∈ Field → (𝐸[:]𝐸) = 1) | ||
| Theorem | fldsdrgfldext 33712 | A sub-division-ring of a field forms a field extension. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐺 = (𝐹 ↾s 𝐴) & ⊢ (𝜑 → 𝐹 ∈ Field) & ⊢ (𝜑 → 𝐴 ∈ (SubDRing‘𝐹)) ⇒ ⊢ (𝜑 → 𝐹/FldExt𝐺) | ||
| Theorem | fldsdrgfldext2 33713 | 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 33714 | 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 33715 | 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 33716 | If the degree of the extension 𝐸/FldExt𝐹 is 1, then 𝐸 and 𝐹 are identical. (Contributed by Thierry Arnoux, 6-Aug-2023.) |
| ⊢ ((𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 1) → 𝐸 = 𝐹) | ||
| Theorem | extdg1b 33717 | 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 33718 | 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 33719 | 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 33720 | 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 33721 | 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 33722 | 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 33723* | Lemma for fldextrspunlsp 33724: 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 33724 | Lemma for fldextrspunfld 33726. 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 33725 | Lemma for fldextrspunfld 33726. 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 33726 | 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 33727 | 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 33728 | 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 33729 | 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 33730 | Lemma for fldextrspundgdvds 33731. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐾 = (𝐿 ↾s 𝐹) & ⊢ 𝐼 = (𝐿 ↾s 𝐺) & ⊢ 𝐽 = (𝐿 ↾s 𝐻) & ⊢ (𝜑 → 𝐿 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐼)) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐽)) & ⊢ (𝜑 → 𝐺 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → 𝐻 ∈ (SubDRing‘𝐿)) & ⊢ (𝜑 → (𝐽[:]𝐾) ∈ ℕ0) & ⊢ 𝐸 = (𝐿 ↾s (𝐿 fldGen (𝐺 ∪ 𝐻))) & ⊢ (𝜑 → (𝐼[:]𝐾) ∈ ℕ) ⇒ ⊢ (𝜑 → (𝐸[:]𝐼) ∈ ℕ0) | ||
| Theorem | fldextrspundgdvds 33731 | 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 33732* | 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 33733 | Integral subring of a ring. |
| class IntgRing | ||
| Definition | df-irng 33734* | 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 33735* | 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 33736* | 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 33737 | 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 33739). (Contributed by Thierry Arnoux, 28-Jan-2025.) |
| ⊢ 𝑂 = (𝑅 evalSub1 𝑆) & ⊢ 𝑈 = (𝑅 ↾s 𝑆) & ⊢ 𝐵 = (Base‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑆 ∈ (SubRing‘𝑅)) & ⊢ (𝜑 → 𝑅 ∈ NzRing) ⇒ ⊢ (𝜑 → 𝑆 ⊆ (𝑅 IntgRing 𝑆)) | ||
| Theorem | irngssv 33738 | 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 33739 | 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 33740 | 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 33741* | 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 33742 | Extend class notation with the minimal polynomial builder function. |
| class minPoly | ||
| Definition | df-minply 33743* | 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 33744* | 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 33745* | 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 33746* | 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 33747* | 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 33748* | 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 33747, 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 33749* | 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 33750* | The set 𝑄 of polynomials annihilating an element 𝐴 is a prime ideal. (Contributed by Thierry Arnoux, 9-Feb-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑄 = {𝑞 ∈ dom 𝑂 ∣ ((𝑂‘𝑞)‘𝐴) = 0 } ⇒ ⊢ (𝜑 → 𝑄 ∈ (PrmIdeal‘𝑃)) | ||
| Theorem | minplymindeg 33751 | The minimal polynomial of 𝐴 is minimal among the nonzero annihilators of 𝐴 with regard to degree. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝐷 = (deg1‘(𝐸 ↾s 𝐹)) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ 𝑈 = (Base‘𝑃) & ⊢ (𝜑 → ((𝑂‘𝐻)‘𝐴) = 0 ) & ⊢ (𝜑 → 𝐻 ∈ 𝑈) & ⊢ (𝜑 → 𝐻 ≠ 𝑍) ⇒ ⊢ (𝜑 → (𝐷‘(𝑀‘𝐴)) ≤ (𝐷‘𝐻)) | ||
| Theorem | minplyann 33752 | The minimal polynomial for 𝐴 annihilates 𝐴 (Contributed by Thierry Arnoux, 25-Apr-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) ⇒ ⊢ (𝜑 → ((𝑂‘(𝑀‘𝐴))‘𝐴) = 0 ) | ||
| Theorem | minplyirredlem 33753 | Lemma for minplyirred 33754. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) & ⊢ (𝜑 → 𝐺 ∈ (Base‘𝑃)) & ⊢ (𝜑 → 𝐻 ∈ (Base‘𝑃)) & ⊢ (𝜑 → (𝐺(.r‘𝑃)𝐻) = (𝑀‘𝐴)) & ⊢ (𝜑 → ((𝑂‘𝐺)‘𝐴) = (0g‘𝐸)) & ⊢ (𝜑 → 𝐺 ≠ 𝑍) & ⊢ (𝜑 → 𝐻 ≠ 𝑍) ⇒ ⊢ (𝜑 → 𝐻 ∈ (Unit‘𝑃)) | ||
| Theorem | minplyirred 33754 | A nonzero minimal polynomial is irreducible. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑂 = (𝐸 evalSub1 𝐹) & ⊢ 𝑃 = (Poly1‘(𝐸 ↾s 𝐹)) & ⊢ 𝐵 = (Base‘𝐸) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ 𝐵) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ 𝑍 = (0g‘𝑃) & ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ (Irred‘𝑃)) | ||
| Theorem | irngnminplynz 33755 | Integral elements have nonzero minimal polynomials. (Contributed by Thierry Arnoux, 22-Mar-2025.) |
| ⊢ 𝑍 = (0g‘(Poly1‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ≠ 𝑍) | ||
| Theorem | minplym1p 33756 | A minimal polynomial is monic. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝑍 = (0g‘(Poly1‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) & ⊢ 𝑈 = (Monic1p‘(𝐸 ↾s 𝐹)) ⇒ ⊢ (𝜑 → (𝑀‘𝐴) ∈ 𝑈) | ||
| Theorem | irredminply 33757 | An irreducible, 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 33758 | Lemma for algextdeg 33766. (Contributed by Thierry Arnoux, 2-Apr-2025.) |
| ⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝐴}))) & ⊢ 𝐷 = (deg1‘𝐸) & ⊢ 𝑀 = (𝐸 minPoly 𝐹) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝐴 ∈ (𝐸 IntgRing 𝐹)) ⇒ ⊢ (𝜑 → (𝐿 ↾s 𝐹) = 𝐾) | ||
| Theorem | algextdeglem2 33759* | Lemma for algextdeg 33766. 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 33760* | Lemma for algextdeg 33766. 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 33761* | Lemma for algextdeg 33766. By lmhmqusker 33445, the surjective module homomorphism 𝐺 described in algextdeglem2 33759 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 33762* | Lemma for algextdeg 33766. 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 33763* | Lemma for algextdeg 33766. By r1pquslmic 33631, 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 33764* | Lemma for algextdeg 33766. 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 33765* | Lemma for algextdeg 33766. 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 33766 | 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 𝐹)) ⇒ ⊢ (𝜑 → (𝐿[:]𝐾) = (𝐷‘(𝑀‘𝐴))) | ||
| Theorem | rtelextdg2lem 33767 | Lemma for rtelextdg2 33768: If an element 𝑋 is a solution of a quadratic equation, then the degree of its field extension is at most 2. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝑋}))) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑉 = (Base‘𝐸) & ⊢ · = (.r‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ ↑ = (.g‘(mulGrp‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐹) & ⊢ (𝜑 → 𝐵 ∈ 𝐹) & ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 ) & ⊢ 𝑌 = (var1‘𝐾) & ⊢ ⊕ = (+g‘𝑃) & ⊢ ⊗ = (.r‘𝑃) & ⊢ ∧ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐺 = ((2 ∧ 𝑌) ⊕ (((𝑈‘𝐴) ⊗ 𝑌) ⊕ (𝑈‘𝐵))) ⇒ ⊢ (𝜑 → (𝐿[:]𝐾) ≤ 2) | ||
| Theorem | rtelextdg2 33768 | If an element 𝑋 is a solution of a quadratic equation, then it is either in the base field, or the degree of its field extension is exactly 2. (Contributed by Thierry Arnoux, 22-Jun-2025.) |
| ⊢ 𝐾 = (𝐸 ↾s 𝐹) & ⊢ 𝐿 = (𝐸 ↾s (𝐸 fldGen (𝐹 ∪ {𝑋}))) & ⊢ 0 = (0g‘𝐸) & ⊢ 𝑃 = (Poly1‘𝐾) & ⊢ 𝑉 = (Base‘𝐸) & ⊢ · = (.r‘𝐸) & ⊢ + = (+g‘𝐸) & ⊢ ↑ = (.g‘(mulGrp‘𝐸)) & ⊢ (𝜑 → 𝐸 ∈ Field) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘𝐸)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝐴 ∈ 𝐹) & ⊢ (𝜑 → 𝐵 ∈ 𝐹) & ⊢ (𝜑 → ((2 ↑ 𝑋) + ((𝐴 · 𝑋) + 𝐵)) = 0 ) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) | ||
| Theorem | fldext2chn 33769* | In a non-empty chain 𝑇 of quadratic field extensions, the degree of the final extension is always a power of two. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐸 = (𝑊 ↾s 𝑒) & ⊢ 𝐹 = (𝑊 ↾s 𝑓) & ⊢ < = {〈𝑓, 𝑒〉 ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)} & ⊢ (𝜑 → 𝑇 ∈ ( < Chain(SubDRing‘𝑊))) & ⊢ (𝜑 → 𝑊 ∈ Field) & ⊢ (𝜑 → (𝑊 ↾s (𝑇‘0)) = 𝑄) & ⊢ (𝜑 → (𝑊 ↾s (lastS‘𝑇)) = 𝐿) & ⊢ (𝜑 → 0 < (♯‘𝑇)) ⇒ ⊢ (𝜑 → (𝐿/FldExt𝑄 ∧ ∃𝑛 ∈ ℕ0 (𝐿[:]𝑄) = (2↑𝑛))) | ||
This section defines the set of constructible points as complex numbers which can be drawn starting from two points (we take 0 and 1), and taking intersections of circles and lines. This construction is useful for proving the impossibility of doubling the cube ( * imp2cube ), and of angle trisection ( * imp3ang ) | ||
| Syntax | cconstr 33770 | Extend class notation with the set of constructible points. |
| class Constr | ||
| Definition | df-constr 33771* | Define the set of geometrically constructible points, by recursively adding the line-line, line-circle and circle-circle intersections constructions using points in a previous iteration. (Contributed by Saveliy Skresanov, 19-Jan-2025.) |
| ⊢ Constr = ∪ (rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) “ ω) | ||
| Theorem | constrrtll 33772 | In the construction of constructible numbers, line-line intersections are solutions of linear equations, and can therefore be completely constructed. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑅 ∈ ℝ) & ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴)))) & ⊢ (𝜑 → 𝑋 = (𝐶 + (𝑅 · (𝐷 − 𝐶)))) & ⊢ (𝜑 → (ℑ‘((∗‘(𝐵 − 𝐴)) · (𝐷 − 𝐶))) ≠ 0) & ⊢ 𝑁 = (𝐴 + (((((𝐴 − 𝐶) · ((∗‘𝐷) − (∗‘𝐶))) − (((∗‘𝐴) − (∗‘𝐶)) · (𝐷 − 𝐶))) / ((((∗‘𝐵) − (∗‘𝐴)) · (𝐷 − 𝐶)) − ((𝐵 − 𝐴) · ((∗‘𝐷) − (∗‘𝐶))))) · (𝐵 − 𝐴))) ⇒ ⊢ (𝜑 → 𝑋 = 𝑁) | ||
| Theorem | constrrtlc1 33773 | In the construction of constructible numbers, line-circle intersections are roots of a quadratic equation, non-degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴)))) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) = (abs‘(𝐸 − 𝐹))) & ⊢ 𝑄 = (((∗‘𝐵) − (∗‘𝐴)) / (𝐵 − 𝐴)) & ⊢ 𝑀 = (((((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶)) − (𝐶 · 𝑄)) / 𝑄) & ⊢ 𝑁 = (-((𝐶 · (((∗‘𝐴) − (𝐴 · 𝑄)) − (∗‘𝐶))) + ((𝐸 − 𝐹) · ((∗‘𝐸) − (∗‘𝐹)))) / 𝑄) & ⊢ (𝜑 → 𝐴 ≠ 𝐵) ⇒ ⊢ (𝜑 → (((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0 ∧ 𝑄 ≠ 0)) | ||
| Theorem | constrrtlc2 33774 | In the construction of constructible numbers, line-circle intersections are one of the original points, in a degenerate case. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝑇 ∈ ℝ) & ⊢ (𝜑 → 𝑋 = (𝐴 + (𝑇 · (𝐵 − 𝐴)))) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐶)) = (abs‘(𝐸 − 𝐹))) & ⊢ (𝜑 → 𝐴 = 𝐵) ⇒ ⊢ (𝜑 → 𝑋 = 𝐴) | ||
| Theorem | constrrtcclem 33775 | In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. Case of non-degenerate circles. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) & ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) & ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) & ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) & ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) & ⊢ (𝜑 → 𝐵 ≠ 𝐶) & ⊢ (𝜑 → 𝐸 ≠ 𝐹) ⇒ ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) | ||
| Theorem | constrrtcc 33776 | In the construction of constructible numbers, circle-circle intersections are roots of a quadratic equation. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ (𝜑 → 𝑆 ⊆ ℂ) & ⊢ (𝜑 → 𝐴 ∈ 𝑆) & ⊢ (𝜑 → 𝐵 ∈ 𝑆) & ⊢ (𝜑 → 𝐶 ∈ 𝑆) & ⊢ (𝜑 → 𝐷 ∈ 𝑆) & ⊢ (𝜑 → 𝐸 ∈ 𝑆) & ⊢ (𝜑 → 𝐹 ∈ 𝑆) & ⊢ (𝜑 → 𝑋 ∈ ℂ) & ⊢ (𝜑 → 𝐴 ≠ 𝐷) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐴)) = (abs‘(𝐵 − 𝐶))) & ⊢ (𝜑 → (abs‘(𝑋 − 𝐷)) = (abs‘(𝐸 − 𝐹))) & ⊢ 𝑃 = ((𝐵 − 𝐶) · (∗‘(𝐵 − 𝐶))) & ⊢ 𝑄 = ((𝐸 − 𝐹) · (∗‘(𝐸 − 𝐹))) & ⊢ 𝑀 = (((𝑄 − ((∗‘𝐷) · (𝐷 + 𝐴))) − (𝑃 − ((∗‘𝐴) · (𝐷 + 𝐴)))) / ((∗‘𝐷) − (∗‘𝐴))) & ⊢ 𝑁 = -(((((∗‘𝐴) · (𝐷 · 𝐴)) − (𝑃 · 𝐷)) − (((∗‘𝐷) · (𝐷 · 𝐴)) − (𝑄 · 𝐴))) / ((∗‘𝐷) − (∗‘𝐴))) ⇒ ⊢ (𝜑 → ((𝑋↑2) + ((𝑀 · 𝑋) + 𝑁)) = 0) | ||
| Theorem | isconstr 33777* | Property of being a constructible number. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) ⇒ ⊢ (𝐴 ∈ Constr ↔ ∃𝑚 ∈ ω 𝐴 ∈ (𝐶‘𝑚)) | ||
| Theorem | constr0 33778 | The first step of the construction of constructible numbers is the pair {0, 1}. In this theorem and the following, we use (𝐶‘𝑁) for the 𝑁-th intermediate iteration of the constructible number. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) ⇒ ⊢ (𝐶‘∅) = {0, 1} | ||
| Theorem | constrsuc 33779* | Membership in the successor step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) & ⊢ 𝑆 = (𝐶‘𝑁) ⇒ ⊢ (𝜑 → (𝑋 ∈ (𝐶‘suc 𝑁) ↔ (𝑋 ∈ ℂ ∧ (∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑑 ∈ 𝑆 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑋 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑒 ∈ 𝑆 ∃𝑓 ∈ 𝑆 ∃𝑡 ∈ ℝ (𝑋 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑋 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑆 ∃𝑏 ∈ 𝑆 ∃𝑐 ∈ 𝑆 ∃𝑑 ∈ 𝑆 ∃𝑒 ∈ 𝑆 ∃𝑓 ∈ 𝑆 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑋 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑋 − 𝑑)) = (abs‘(𝑒 − 𝑓))))))) | ||
| Theorem | constrlim 33780* | Limit step of the construction of constructible numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ 𝑉) & ⊢ (𝜑 → Lim 𝑁) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) = ∪ 𝑛 ∈ 𝑁 (𝐶‘𝑛)) | ||
| Theorem | constrsscn 33781* | Closure of the constructible points in the complex numbers. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ⊆ ℂ) | ||
| Theorem | constrsslem 33782* | Lemma for constrss 33784. This lemma requires the additional condition that 0 is the constructible number; that condition is removed in constrss 33784. (Proposed by Saveliy Skresanov, 23-JUn-2025.) (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) & ⊢ (𝜑 → 0 ∈ (𝐶‘𝑁)) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (𝐶‘suc 𝑁)) | ||
| Theorem | constr01 33783* | 0 and 1 are in all steps of the construction of constructible points. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) ⇒ ⊢ (𝜑 → {0, 1} ⊆ (𝐶‘𝑁)) | ||
| Theorem | constrss 33784* | Constructed points are in the next generation constructed points. (Contributed by Thierry Arnoux, 25-Jun-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (𝐶‘suc 𝑁)) | ||
| Theorem | constrmon 33785* | The construction of constructible numbers is monotonous, i.e. if the ordinal 𝑀 is less than the ordinal 𝑁, which is denoted by 𝑀 ∈ 𝑁, then the 𝑀-th step of the constructible numbers is included in the 𝑁-th step. (Contributed by Thierry Arnoux, 1-Jul-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) & ⊢ (𝜑 → 𝑀 ∈ 𝑁) ⇒ ⊢ (𝜑 → (𝐶‘𝑀) ⊆ (𝐶‘𝑁)) | ||
| Theorem | constrconj 33786* | If a point 𝑋 of the complex plane is constructible, so is its conjugate (∗‘𝑋). (Proposed by Saveliy Skresanov, 25-Jun-2025.) (Contributed by Thierry Arnoux, 1-Jul-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ On) & ⊢ (𝜑 → 𝑋 ∈ (𝐶‘𝑁)) ⇒ ⊢ (𝜑 → (∗‘𝑋) ∈ (𝐶‘𝑁)) | ||
| Theorem | constrfin 33787* | Each step of the construction of constructible numbers is finite. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → (𝐶‘𝑁) ∈ Fin) | ||
| Theorem | constrelextdg2 33788* | If the 𝑁-th step (𝐶‘𝑁) of the construction of constuctible numbers is included in a subfield 𝐹 of the complex numbers, then any element 𝑋 of the next step (𝐶‘suc 𝑁) is either in 𝐹 or in a quadratic extension of 𝐹. (Contributed by Thierry Arnoux, 6-Jul-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ 𝐾 = (ℂfld ↾s 𝐹) & ⊢ 𝐿 = (ℂfld ↾s (ℂfld fldGen (𝐹 ∪ {𝑋}))) & ⊢ (𝜑 → 𝐹 ∈ (SubDRing‘ℂfld)) & ⊢ (𝜑 → 𝑁 ∈ On) & ⊢ (𝜑 → (𝐶‘𝑁) ⊆ 𝐹) & ⊢ (𝜑 → 𝑋 ∈ (𝐶‘suc 𝑁)) ⇒ ⊢ (𝜑 → (𝑋 ∈ 𝐹 ∨ (𝐿[:]𝐾) = 2)) | ||
| Theorem | constrextdg2lem 33789* | Lemma for constrextdg2 33790 (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ 𝐸 = (ℂfld ↾s 𝑒) & ⊢ 𝐹 = (ℂfld ↾s 𝑓) & ⊢ < = {〈𝑓, 𝑒〉 ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)} & ⊢ (𝜑 → 𝑁 ∈ ω) & ⊢ (𝜑 → 𝑅 ∈ ( < Chain(SubDRing‘ℂfld))) & ⊢ (𝜑 → (𝑅‘0) = ℚ) & ⊢ (𝜑 → (𝐶‘𝑁) ⊆ (lastS‘𝑅)) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ ( < Chain(SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘suc 𝑁) ⊆ (lastS‘𝑣))) | ||
| Theorem | constrextdg2 33790* | Any step (𝐶‘𝑁) of the construction of constructible numbers is contained in the last field of a tower of quadratic field extensions starting with ℚ. (Contributed by Thierry Arnoux, 19-Oct-2025.) |
| ⊢ 𝐶 = rec((𝑠 ∈ V ↦ {𝑥 ∈ ℂ ∣ (∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑡 ∈ ℝ ∃𝑟 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ 𝑥 = (𝑐 + (𝑟 · (𝑑 − 𝑐))) ∧ (ℑ‘((∗‘(𝑏 − 𝑎)) · (𝑑 − 𝑐))) ≠ 0) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 ∃𝑡 ∈ ℝ (𝑥 = (𝑎 + (𝑡 · (𝑏 − 𝑎))) ∧ (abs‘(𝑥 − 𝑐)) = (abs‘(𝑒 − 𝑓))) ∨ ∃𝑎 ∈ 𝑠 ∃𝑏 ∈ 𝑠 ∃𝑐 ∈ 𝑠 ∃𝑑 ∈ 𝑠 ∃𝑒 ∈ 𝑠 ∃𝑓 ∈ 𝑠 (𝑎 ≠ 𝑑 ∧ (abs‘(𝑥 − 𝑎)) = (abs‘(𝑏 − 𝑐)) ∧ (abs‘(𝑥 − 𝑑)) = (abs‘(𝑒 − 𝑓))))}), {0, 1}) & ⊢ 𝐸 = (ℂfld ↾s 𝑒) & ⊢ 𝐹 = (ℂfld ↾s 𝑓) & ⊢ < = {〈𝑓, 𝑒〉 ∣ (𝐸/FldExt𝐹 ∧ (𝐸[:]𝐹) = 2)} & ⊢ (𝜑 → 𝑁 ∈ ω) ⇒ ⊢ (𝜑 → ∃𝑣 ∈ ( < Chain(SubDRing‘ℂfld))((𝑣‘0) = ℚ ∧ (𝐶‘𝑁) ⊆ (lastS‘𝑣))) | ||
| Theorem | 2sqr3minply 33791 | The polynomial ((𝑋↑3) − 2) is the minimal polynomial for (2↑𝑐(1 / 3)) over ℚ, and its degree is 3. (Contributed by Thierry Arnoux, 14-Jun-2025.) |
| ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ − = (-g‘𝑃) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑃 = (Poly1‘𝑄) & ⊢ 𝐾 = (algSc‘𝑃) & ⊢ 𝑋 = (var1‘𝑄) & ⊢ 𝐷 = (deg1‘𝑄) & ⊢ 𝐹 = ((3 ↑ 𝑋) − (𝐾‘2)) & ⊢ 𝐴 = (2↑𝑐(1 / 3)) & ⊢ 𝑀 = (ℂfld minPoly ℚ) ⇒ ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3) | ||
| Syntax | csmat 33792 | Syntax for a function generating submatrices. |
| class subMat1 | ||
| Definition | df-smat 33793* | 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 22583. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
| ⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))〉)))) | ||
| Theorem | smatfval 33794* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ 〈if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))〉))) | ||
| Theorem | smatrcl 33795 | 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 33796 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) & ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) | ||
| Theorem | smattl 33797 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽)) | ||
| Theorem | smattr 33798 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽)) | ||
| Theorem | smatbl 33799 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1))) | ||
| Theorem | smatbr 33800 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |