HomeTheorem List (p. 339 of 500)
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. 339 of 500) | < 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-30900) |
Hilbert Space Explorer
(30901-32423) |
Users' Mathboxes
(32424-49930) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | constrremulcl 33801 | If two real numbers 𝑋 and 𝑌 are constructible, then, so is their product. (Contributed by Thierry Arnoux, 2-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) & ⊢ (𝜑 → 𝑌 ∈ Constr) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 𝑌 ∈ ℝ) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ Constr) | ||
| Theorem | constrcjcl 33802 | Constructible numbers are closed under complex conjugate. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) ⇒ ⊢ (𝜑 → (∗‘𝑋) ∈ Constr) | ||
| Theorem | constrrecl 33803 | Constructible numbers are closed under taking the real part. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) ⇒ ⊢ (𝜑 → (ℜ‘𝑋) ∈ Constr) | ||
| Theorem | constrimcl 33804 | Constructible numbers are closed under taking the imaginary part. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) ⇒ ⊢ (𝜑 → (ℑ‘𝑋) ∈ Constr) | ||
| Theorem | constrmulcl 33805 | Constructible numbers are closed under complex multiplication. Item (3) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) & ⊢ (𝜑 → 𝑌 ∈ Constr) ⇒ ⊢ (𝜑 → (𝑋 · 𝑌) ∈ Constr) | ||
| Theorem | constrreinvcl 33806 | If a real number 𝑋 is constructible, then, so is its inverse. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) & ⊢ (𝜑 → 𝑋 ≠ 0) & ⊢ (𝜑 → 𝑋 ∈ ℝ) ⇒ ⊢ (𝜑 → (1 / 𝑋) ∈ Constr) | ||
| Theorem | constrinvcl 33807 | Constructible numbers are closed under complex inverse. Item (4) of Theorem 7.10 of [Stewart] p. 96 (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) & ⊢ (𝜑 → 𝑋 ≠ 0) ⇒ ⊢ (𝜑 → (1 / 𝑋) ∈ Constr) | ||
| Theorem | constrcon 33808* | Contradiction of constructibility: If a complex number 𝐴 has minimal polynomial 𝐹 over ℚ of a degree that is not a power of 2, then 𝐴 is not constructible. (Contributed by Thierry Arnoux, 26-Oct-2025.) |
| ⊢ 𝐷 = (deg1‘(ℂfld ↾s ℚ)) & ⊢ 𝑀 = (ℂfld minPoly ℚ) & ⊢ (𝜑 → 𝐴 ∈ ℂ) & ⊢ (𝜑 → 𝐹 = (𝑀‘𝐴)) & ⊢ (𝜑 → (𝐷‘𝐹) ∈ ℕ0) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ0) → (𝐷‘𝐹) ≠ (2↑𝑛)) ⇒ ⊢ (𝜑 → ¬ 𝐴 ∈ Constr) | ||
| Theorem | constrsdrg 33809 | Constructible numbers form a subfield of the complex numbers. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ Constr ∈ (SubDRing‘ℂfld) | ||
| Theorem | constrfld 33810 | The constructible numbers form a field. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (ℂfld ↾s Constr) ∈ Field | ||
| Theorem | constrresqrtcl 33811 | If a positive real number 𝑋 is constructible, then, so is its square root. (Contributed by Thierry Arnoux, 5-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) & ⊢ (𝜑 → 𝑋 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝑋) ⇒ ⊢ (𝜑 → (√‘𝑋) ∈ Constr) | ||
| Theorem | constrabscl 33812 | Constructible numbers are closed under absolute value (modulus). (Contributed by Thierry Arnoux, 6-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) ⇒ ⊢ (𝜑 → (abs‘𝑋) ∈ Constr) | ||
| Theorem | constrsqrtcl 33813 | Constructible numbers are closed under taking the square root. This is not generally the case for the cubic root operation, see 2sqr3nconstr 33815. Item (5) of Theorem 7.10 of [Stewart] p. 96 (Proposed by Saveliy Skresanov, 3-Nov-2025.) (Contributed by Thierry Arnoux, 6-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ Constr) ⇒ ⊢ (𝜑 → (√‘𝑋) ∈ Constr) | ||
| Theorem | 2sqr3minply 33814 | 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) | ||
| Theorem | 2sqr3nconstr 33815 | Doubling the cube is an impossible construction, i.e. the cube root of 2 is not constructible with straightedge and compass. Given a cube of edge of length one, a cube of double volume would have an edge of length (2↑𝑐(1 / 3)), however that number is not constructible. This is the first part of Metamath 100 proof #8. Theorem 7.13 of [Stewart] p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 26-Oct-2025.) |
| ⊢ (2↑𝑐(1 / 3)) ∉ Constr | ||
| Theorem | cos9thpiminplylem1 33816 | The polynomial ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) has no integer roots. (Contributed by Thierry Arnoux, 9-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ℤ) ⇒ ⊢ (𝜑 → ((𝑋↑3) + ((-3 · (𝑋↑2)) + 1)) ≠ 0) | ||
| Theorem | cos9thpiminplylem2 33817 | The polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)) has no rational roots. (Contributed by Thierry Arnoux, 9-Nov-2025.) |
| ⊢ (𝜑 → 𝑋 ∈ ℚ) ⇒ ⊢ (𝜑 → ((𝑋↑3) + ((-3 · 𝑋) + 1)) ≠ 0) | ||
| Theorem | cos9thpiminplylem3 33818 | Lemma for cos9thpiminply 33822. (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) ⇒ ⊢ ((𝑂↑2) + (𝑂 + 1)) = 0 | ||
| Theorem | cos9thpiminplylem4 33819 | Lemma for cos9thpiminply 33822. (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) ⇒ ⊢ ((𝑍↑6) + (𝑍↑3)) = -1 | ||
| Theorem | cos9thpiminplylem5 33820 | The constructed complex number 𝐴 is a root of the polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)). (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) & ⊢ 𝐴 = (𝑍 + (1 / 𝑍)) ⇒ ⊢ ((𝐴↑3) + ((-3 · 𝐴) + 1)) = 0 | ||
| Theorem | cos9thpiminplylem6 33821 | Evaluation of the polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)). (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) & ⊢ 𝐴 = (𝑍 + (1 / 𝑍)) & ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑃 = (Poly1‘𝑄) & ⊢ 𝐾 = (algSc‘𝑃) & ⊢ 𝑋 = (var1‘𝑄) & ⊢ 𝐷 = (deg1‘𝑄) & ⊢ 𝐹 = ((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))) & ⊢ (𝜑 → 𝑌 ∈ ℂ) ⇒ ⊢ (𝜑 → (((ℂfld evalSub1 ℚ)‘𝐹)‘𝑌) = ((𝑌↑3) + ((-3 · 𝑌) + 1))) | ||
| Theorem | cos9thpiminply 33822 | The polynomial ((𝑋↑3) + ((-3 · 𝑋) + 1)) is the minimal polynomial for 𝐴 over ℚ, and its degree is 3. (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) & ⊢ 𝐴 = (𝑍 + (1 / 𝑍)) & ⊢ 𝑄 = (ℂfld ↾s ℚ) & ⊢ + = (+g‘𝑃) & ⊢ · = (.r‘𝑃) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑃 = (Poly1‘𝑄) & ⊢ 𝐾 = (algSc‘𝑃) & ⊢ 𝑋 = (var1‘𝑄) & ⊢ 𝐷 = (deg1‘𝑄) & ⊢ 𝐹 = ((3 ↑ 𝑋) + (((𝐾‘-3) · 𝑋) + (𝐾‘1))) & ⊢ 𝑀 = (ℂfld minPoly ℚ) ⇒ ⊢ (𝐹 = (𝑀‘𝐴) ∧ (𝐷‘𝐹) = 3) | ||
| Theorem | cos9thpinconstrlem1 33823 | The complex number 𝑂, representing an angle of (2 · π) / 3, is constructible. (Contributed by Thierry Arnoux, 14-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) ⇒ ⊢ 𝑂 ∈ Constr | ||
| Theorem | cos9thpinconstrlem2 33824 | The complex number 𝐴 is not constructible. (Contributed by Thierry Arnoux, 15-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) & ⊢ 𝐴 = (𝑍 + (1 / 𝑍)) ⇒ ⊢ ¬ 𝐴 ∈ Constr | ||
| Theorem | cos9thpinconstr 33825 | Trisecting an angle is an impossible construction. Given for example 𝑂 = (exp‘((i · (2 · π)) / 3)), which represents an angle of ((2 · π) / 3), the cube root of 𝑂 is not constructible with straightedge and compass, while 𝑂 itself is constructible. This is the second part of Metamath 100 proof #8. Theorem 7.14 of [Stewart] p. 99. (Contributed by Thierry Arnoux and Saveliy Skresanov, 15-Nov-2025.) |
| ⊢ 𝑂 = (exp‘((i · (2 · π)) / 3)) & ⊢ 𝑍 = (𝑂↑𝑐(1 / 3)) ⇒ ⊢ (𝑂 ∈ Constr ∧ 𝑍 ∉ Constr) | ||
| Theorem | trisecnconstr 33826 | Not all angles can be trisected. (Contributed by Thierry Arnoux, 15-Nov-2025.) |
| ⊢ ¬ ∀𝑜 ∈ Constr (𝑜↑𝑐(1 / 3)) ∈ Constr | ||
| Syntax | csmat 33827 | Syntax for a function generating submatrices. |
| class subMat1 | ||
| Definition | df-smat 33828* | 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 22493. (Contributed by Thierry Arnoux, 18-Aug-2020.) |
| ⊢ subMat1 = (𝑚 ∈ V ↦ (𝑘 ∈ ℕ, 𝑙 ∈ ℕ ↦ (𝑚 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝑘, 𝑖, (𝑖 + 1)), if(𝑗 < 𝑙, 𝑗, (𝑗 + 1))⟩)))) | ||
| Theorem | smatfval 33829* | Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ ((𝐾 ∈ ℕ ∧ 𝐿 ∈ ℕ ∧ 𝑀 ∈ 𝑉) → (𝐾(subMat1‘𝑀)𝐿) = (𝑀 ∘ (𝑖 ∈ ℕ, 𝑗 ∈ ℕ ↦ ⟨if(𝑖 < 𝐾, 𝑖, (𝑖 + 1)), if(𝑗 < 𝐿, 𝑗, (𝑗 + 1))⟩))) | ||
| Theorem | smatrcl 33830 | 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 33831 | Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ ℕ) & ⊢ (𝜑 → 𝐽 ∈ ℕ) & ⊢ (𝜑 → if(𝐼 < 𝐾, 𝐼, (𝐼 + 1)) = 𝑋) & ⊢ (𝜑 → if(𝐽 < 𝐿, 𝐽, (𝐽 + 1)) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝑋𝐴𝑌)) | ||
| Theorem | smattl 33832 | Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴𝐽)) | ||
| Theorem | smattr 33833 | Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (1..^𝐿)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴𝐽)) | ||
| Theorem | smatbl 33834 | Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (1..^𝐾)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = (𝐼𝐴(𝐽 + 1))) | ||
| Theorem | smatbr 33835 | Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝑆 = (𝐾(subMat1‘𝐴)𝐿) & ⊢ (𝜑 → 𝑀 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑀)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐴 ∈ (𝐵 ↑m ((1...𝑀) × (1...𝑁)))) & ⊢ (𝜑 → 𝐼 ∈ (𝐾...𝑀)) & ⊢ (𝜑 → 𝐽 ∈ (𝐿...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑆𝐽) = ((𝐼 + 1)𝐴(𝐽 + 1))) | ||
| Theorem | smatcl 33836 | Closure of the square submatrix: if 𝑀 is a square matrix of dimension 𝑁 with indices in (1...𝑁), then a submatrix of 𝑀 is of dimension (𝑁 − 1). (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐶 = (Base‘((1...(𝑁 − 1)) Mat 𝑅)) & ⊢ 𝑆 = (𝐾(subMat1‘𝑀)𝐿) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐿 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐶) | ||
| Theorem | matmpo 33837* | Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ (𝑀 ∈ 𝐵 → 𝑀 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀𝑗))) | ||
| Theorem | 1smat1 33838 | The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 22499. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 1 = (1r‘((1...𝑁) Mat 𝑅)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘ 1 )𝐼) = (1r‘((1...(𝑁 − 1)) Mat 𝑅))) | ||
| Theorem | submat1n 33839 | One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑁(((1...𝑁) subMat 𝑅)‘𝑀)𝑁)) | ||
| Theorem | submatres 33840 | Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝑀 ∈ 𝐵) → (𝑁(subMat1‘𝑀)𝑁) = (𝑀 ↾ ((1...(𝑁 − 1)) × (1...(𝑁 − 1))))) | ||
| Theorem | submateqlem1 33841 | Lemma for submateq 33843. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝐾 ≤ 𝑀) ⇒ ⊢ (𝜑 → (𝑀 ∈ (𝐾...𝑁) ∧ (𝑀 + 1) ∈ ((1...𝑁) ∖ {𝐾}))) | ||
| Theorem | submateqlem2 33842 | Lemma for submateq 33843. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐾 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ (1...(𝑁 − 1))) & ⊢ (𝜑 → 𝑀 < 𝐾) ⇒ ⊢ (𝜑 → (𝑀 ∈ (1..^𝐾) ∧ 𝑀 ∈ ((1...𝑁) ∖ {𝐾}))) | ||
| Theorem | submateq 33843* | Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐸 ∈ 𝐵) & ⊢ (𝜑 → 𝐹 ∈ 𝐵) & ⊢ ((𝜑 ∧ 𝑖 ∈ ((1...𝑁) ∖ {𝐼}) ∧ 𝑗 ∈ ((1...𝑁) ∖ {𝐽})) → (𝑖𝐸𝑗) = (𝑖𝐹𝑗)) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝐸)𝐽) = (𝐼(subMat1‘𝐹)𝐽)) | ||
| Theorem | submatminr1 33844 | If we take a submatrix by removing the row 𝐼 and column 𝐽, then the result is the same on the matrix with row 𝐼 and column 𝐽 modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.) |
| ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑅 ∈ Ring) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝐸 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝑀)𝐽) = (𝐼(subMat1‘𝐸)𝐽)) | ||
| Syntax | clmat 33845 | Extend class notation with the literal matrix conversion function. |
| class litMat | ||
| Definition | df-lmat 33846* | Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ litMat = (𝑚 ∈ V ↦ (𝑖 ∈ (1...(♯‘𝑚)), 𝑗 ∈ (1...(♯‘(𝑚‘0))) ↦ ((𝑚‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
| Theorem | lmatval 33847* | Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ (𝑀 ∈ 𝑉 → (litMat‘𝑀) = (𝑖 ∈ (1...(♯‘𝑀)), 𝑗 ∈ (1...(♯‘(𝑀‘0))) ↦ ((𝑀‘(𝑖 − 1))‘(𝑗 − 1)))) | ||
| Theorem | lmatfval 33848* | Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (♯‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = ((𝑊‘(𝐼 − 1))‘(𝐽 − 1))) | ||
| Theorem | lmatfvlem 33849* | Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (♯‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝐾 ∈ ℕ0 & ⊢ 𝐿 ∈ ℕ0 & ⊢ 𝐼 ≤ 𝑁 & ⊢ 𝐽 ≤ 𝑁 & ⊢ (𝐾 + 1) = 𝐼 & ⊢ (𝐿 + 1) = 𝐽 & ⊢ (𝑊‘𝐾) = 𝑋 & ⊢ (𝜑 → (𝑋‘𝐿) = 𝑌) ⇒ ⊢ (𝜑 → (𝐼𝑀𝐽) = 𝑌) | ||
| Theorem | lmatcl 33850* | Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘𝑊) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑊 ∈ Word Word 𝑉) & ⊢ (𝜑 → (♯‘𝑊) = 𝑁) & ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^𝑁)) → (♯‘(𝑊‘𝑖)) = 𝑁) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝑂 = ((1...𝑁) Mat 𝑅) & ⊢ 𝑃 = (Base‘𝑂) & ⊢ (𝜑 → 𝑅 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝑀 ∈ 𝑃) | ||
| Theorem | lmat22lem 33851* | Lemma for lmat22e11 33852 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ ((𝜑 ∧ 𝑖 ∈ (0..^2)) → (♯‘(⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩‘𝑖)) = 2) | ||
| Theorem | lmat22e11 33852 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀1) = 𝐴) | ||
| Theorem | lmat22e12 33853 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (1𝑀2) = 𝐵) | ||
| Theorem | lmat22e21 33854 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀1) = 𝐶) | ||
| Theorem | lmat22e22 33855 | Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → (2𝑀2) = 𝐷) | ||
| Theorem | lmat22det 33856 | The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.) |
| ⊢ 𝑀 = (litMat‘⟨“⟨“𝐴𝐵”⟩⟨“𝐶𝐷”⟩”⟩) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) & ⊢ · = (.r‘𝑅) & ⊢ − = (-g‘𝑅) & ⊢ 𝑉 = (Base‘𝑅) & ⊢ 𝐽 = ((1...2) maDet 𝑅) & ⊢ (𝜑 → 𝑅 ∈ Ring) ⇒ ⊢ (𝜑 → (𝐽‘𝑀) = ((𝐴 · 𝐷) − (𝐶 · 𝐵))) | ||
| Theorem | mdetpmtr1 33857* | The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀𝑗)) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr2 33858* | The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑖𝑀(𝑃‘𝑗))) ⇒ ⊢ (((𝑅 ∈ CRing ∧ 𝑁 ∈ Fin) ∧ (𝑀 ∈ 𝐵 ∧ 𝑃 ∈ 𝐺)) → (𝐷‘𝑀) = (((𝑍 ∘ 𝑆)‘𝑃) · (𝐷‘𝐸))) | ||
| Theorem | mdetpmtr12 33859* | The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐺 = (Base‘(SymGrp‘𝑁)) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝐸 = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑃‘𝑖)𝑀(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝑁 ∈ Fin) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐷‘𝐸))) | ||
| Theorem | mdetlap1 33860* | A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐷 = (𝑁 maDet 𝑅) & ⊢ 𝐾 = (𝑁 maAdju 𝑅) & ⊢ · = (.r‘𝑅) ⇒ ⊢ ((𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝐼 ∈ 𝑁) → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ 𝑁 ↦ ((𝐼𝑀𝑗) · (𝑗(𝐾‘𝑀)𝐼))))) | ||
| Theorem | madjusmdetlem1 33861* | Lemma for madjusmdet 33865. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝐺 = (Base‘(SymGrp‘(1...𝑁))) & ⊢ 𝑆 = (pmSgn‘(1...𝑁)) & ⊢ 𝑈 = (𝐼(((1...𝑁) minMatR1 𝑅)‘𝑀)𝐽) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ ((𝑃‘𝑖)𝑈(𝑄‘𝑗))) & ⊢ (𝜑 → 𝑃 ∈ 𝐺) & ⊢ (𝜑 → 𝑄 ∈ 𝐺) & ⊢ (𝜑 → (𝑃‘𝑁) = 𝐼) & ⊢ (𝜑 → (𝑄‘𝑁) = 𝐽) & ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘((𝑆‘𝑃) · (𝑆‘𝑄))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdetlem2 33862* | Lemma for madjusmdet 33865. (Contributed by Thierry Arnoux, 26-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ (1...(𝑁 − 1))) → if(𝑋 < 𝐼, 𝑋, (𝑋 + 1)) = ((𝑃 ∘ ◡𝑆)‘𝑋)) | ||
| Theorem | madjusmdetlem3 33863* | Lemma for madjusmdet 33865. (Contributed by Thierry Arnoux, 27-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) & ⊢ 𝑊 = (𝑖 ∈ (1...𝑁), 𝑗 ∈ (1...𝑁) ↦ (((𝑃 ∘ ◡𝑆)‘𝑖)𝑈((𝑄 ∘ ◡𝑇)‘𝑗))) & ⊢ (𝜑 → 𝑈 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐼(subMat1‘𝑈)𝐽) = (𝑁(subMat1‘𝑊)𝑁)) | ||
| Theorem | madjusmdetlem4 33864* | Lemma for madjusmdet 33865. (Contributed by Thierry Arnoux, 22-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) & ⊢ 𝑃 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝐼, if(𝑖 ≤ 𝐼, (𝑖 − 1), 𝑖))) & ⊢ 𝑆 = (𝑖 ∈ (1...𝑁) ↦ if(𝑖 = 1, 𝑁, if(𝑖 ≤ 𝑁, (𝑖 − 1), 𝑖))) & ⊢ 𝑄 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝐽, if(𝑗 ≤ 𝐽, (𝑗 − 1), 𝑗))) & ⊢ 𝑇 = (𝑗 ∈ (1...𝑁) ↦ if(𝑗 = 1, 𝑁, if(𝑗 ≤ 𝑁, (𝑗 − 1), 𝑗))) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | madjusmdet 33865 | Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrices. (Contributed by Thierry Arnoux, 23-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐽(𝐾‘𝑀)𝐼) = ((𝑍‘(-1↑(𝐼 + 𝐽))) · (𝐸‘(𝐼(subMat1‘𝑀)𝐽)))) | ||
| Theorem | mdetlap 33866* | Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.) |
| ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐴 = ((1...𝑁) Mat 𝑅) & ⊢ 𝐷 = ((1...𝑁) maDet 𝑅) & ⊢ 𝐾 = ((1...𝑁) maAdju 𝑅) & ⊢ · = (.r‘𝑅) & ⊢ 𝑍 = (ℤRHom‘𝑅) & ⊢ 𝐸 = ((1...(𝑁 − 1)) maDet 𝑅) & ⊢ (𝜑 → 𝑁 ∈ ℕ) & ⊢ (𝜑 → 𝑅 ∈ CRing) & ⊢ (𝜑 → 𝐼 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝐽 ∈ (1...𝑁)) & ⊢ (𝜑 → 𝑀 ∈ 𝐵) ⇒ ⊢ (𝜑 → (𝐷‘𝑀) = (𝑅 Σg (𝑗 ∈ (1...𝑁) ↦ ((𝑍‘(-1↑(𝐼 + 𝑗))) · ((𝐼𝑀𝑗) · (𝐸‘(𝐼(subMat1‘𝑀)𝑗))))))) | ||
| Theorem | ist0cld 33867* | The predicate "is a T0 space", using closed sets. (Contributed by Thierry Arnoux, 16-Aug-2020.) |
| ⊢ (𝜑 → 𝐵 = ∪ 𝐽) & ⊢ (𝜑 → 𝐷 = (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 ∈ Kol2 ↔ (𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (∀𝑑 ∈ 𝐷 (𝑥 ∈ 𝑑 ↔ 𝑦 ∈ 𝑑) → 𝑥 = 𝑦)))) | ||
| Theorem | txomap 33868* | Given two open maps 𝐹 and 𝐺, 𝐻 mapping pairs of sets, is also an open map for the product topology. (Contributed by Thierry Arnoux, 29-Dec-2019.) |
| ⊢ (𝜑 → 𝐹:𝑋⟶𝑍) & ⊢ (𝜑 → 𝐺:𝑌⟶𝑇) & ⊢ (𝜑 → 𝐽 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑍)) & ⊢ (𝜑 → 𝑀 ∈ (TopOn‘𝑇)) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ 𝐿) & ⊢ ((𝜑 ∧ 𝑦 ∈ 𝐾) → (𝐺 “ 𝑦) ∈ 𝑀) & ⊢ (𝜑 → 𝐴 ∈ (𝐽 ×t 𝐾)) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ ⟨(𝐹‘𝑥), (𝐺‘𝑦)⟩) ⇒ ⊢ (𝜑 → (𝐻 “ 𝐴) ∈ (𝐿 ×t 𝑀)) | ||
| Theorem | qtopt1 33869* | If every equivalence class is closed, then the quotient space is T1 . (Contributed by Thierry Arnoux, 5-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝐽 ∈ Fre) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (◡𝐹 “ {𝑥}) ∈ (Clsd‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Fre) | ||
| Theorem | qtophaus 33870* | If an open map's graph in the product space (𝐽 ×t 𝐽) is closed, then its quotient topology is Hausdorff. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ ∼ = (◡𝐹 ∘ 𝐹) & ⊢ 𝐻 = (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑋 ↦ ⟨(𝐹‘𝑥), (𝐹‘𝑦)⟩) & ⊢ (𝜑 → 𝐽 ∈ Haus) & ⊢ (𝜑 → 𝐹:𝑋–onto→𝑌) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝐽) → (𝐹 “ 𝑥) ∈ (𝐽 qTop 𝐹)) & ⊢ (𝜑 → ∼ ∈ (Clsd‘(𝐽 ×t 𝐽))) ⇒ ⊢ (𝜑 → (𝐽 qTop 𝐹) ∈ Haus) | ||
| Theorem | circtopn 33871* | The topology of the unit circle is generated by open intervals of the polar coordinate. (Contributed by Thierry Arnoux, 4-Jan-2020.) |
| ⊢ 𝐼 = (0[,](2 · π)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ (𝐽 qTop 𝐹) = (TopOpen‘(𝐹 “s ℝfld)) | ||
| Theorem | circcn 33872* | The function gluing the real line into the unit circle is continuous. (Contributed by Thierry Arnoux, 5-Jan-2020.) |
| ⊢ 𝐼 = (0[,](2 · π)) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐹 = (𝑥 ∈ ℝ ↦ (exp‘(i · 𝑥))) & ⊢ 𝐶 = (◡abs “ {1}) ⇒ ⊢ 𝐹 ∈ (𝐽 Cn (𝐽 qTop 𝐹)) | ||
| Theorem | reff 33873* | For any cover refinement, there exists a function associating with each set in the refinement a set in the original cover containing it. This is sometimes used as a definition of refinement. Note that this definition uses the axiom of choice through ac6sg 10386. (Contributed by Thierry Arnoux, 12-Jan-2020.) |
| ⊢ (𝐴 ∈ 𝑉 → (𝐴Ref𝐵 ↔ (∪ 𝐵 ⊆ ∪ 𝐴 ∧ ∃𝑓(𝑓:𝐴⟶𝐵 ∧ ∀𝑣 ∈ 𝐴 𝑣 ⊆ (𝑓‘𝑣))))) | ||
| Theorem | locfinreflem 33874* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. The solution is constructed by building unions, so the same method can be used to prove a similar theorem about closed covers. (Contributed by Thierry Arnoux, 29-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ⊆ 𝐽) & ⊢ (𝜑 → 𝑉Ref𝑈) & ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑓((Fun 𝑓 ∧ dom 𝑓 ⊆ 𝑈 ∧ ran 𝑓 ⊆ 𝐽) ∧ (ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽)))) | ||
| Theorem | locfinref 33875* | A locally finite refinement of an open cover induces a locally finite open cover with the original index set. This is fact 2 of http://at.yorku.ca/p/a/c/a/02.pdf, it is expressed by exposing a function 𝑓 from the original cover 𝑈, which is taken as the index set. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ (𝜑 → 𝑈 ⊆ 𝐽) & ⊢ (𝜑 → 𝑋 = ∪ 𝑈) & ⊢ (𝜑 → 𝑉 ⊆ 𝐽) & ⊢ (𝜑 → 𝑉Ref𝑈) & ⊢ (𝜑 → 𝑉 ∈ (LocFin‘𝐽)) ⇒ ⊢ (𝜑 → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) | ||
| Syntax | ccref 33876 | The "every open cover has an 𝐴 refinement" predicate. |
| class CovHasRef𝐴 | ||
| Definition | df-cref 33877* | Define a statement "every open cover has an 𝐴 refinement" , where 𝐴 is a property for refinements like "finite", "countable", "point finite" or "locally finite". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ CovHasRef𝐴 = {𝑗 ∈ Top ∣ ∀𝑦 ∈ 𝒫 𝑗(∪ 𝑗 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝑗 ∩ 𝐴)𝑧Ref𝑦)} | ||
| Theorem | iscref 33878* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ CovHasRef𝐴 ↔ (𝐽 ∈ Top ∧ ∀𝑦 ∈ 𝒫 𝐽(𝑋 = ∪ 𝑦 → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝑦))) | ||
| Theorem | crefeq 33879 | Equality theorem for the "every open cover has an A refinement" predicate. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 = 𝐵 → CovHasRef𝐴 = CovHasRef𝐵) | ||
| Theorem | creftop 33880 | A space where every open cover has an 𝐴 refinement is a topological space. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ CovHasRef𝐴 → 𝐽 ∈ Top) | ||
| Theorem | crefi 33881* | The property that every open cover has an 𝐴 refinement for the topological space 𝐽. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ CovHasRef𝐴 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ (𝒫 𝐽 ∩ 𝐴)𝑧Ref𝐶) | ||
| Theorem | crefdf 33882* | A formulation of crefi 33881 easier to use for definitions. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 & ⊢ 𝐵 = CovHasRef𝐴 & ⊢ (𝑧 ∈ 𝐴 → 𝜑) ⇒ ⊢ ((𝐽 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝐶) → ∃𝑧 ∈ 𝒫 𝐽(𝜑 ∧ 𝑧Ref𝐶)) | ||
| Theorem | crefss 33883 | The "every open cover has an 𝐴 refinement" predicate respects inclusion. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐴 ⊆ 𝐵 → CovHasRef𝐴 ⊆ CovHasRef𝐵) | ||
| Theorem | cmpcref 33884 | Equivalent definition of compact space in terms of open cover refinements. Compact spaces are topologies with finite open cover refinements. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ Comp = CovHasRefFin | ||
| Theorem | cmpfiref 33885* | Every open cover of a Compact space has a finite refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Comp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ Fin ∧ 𝑣Ref𝑈)) | ||
| Syntax | cldlf 33886 | Extend class notation with the class of all Lindelöf spaces. |
| class Ldlf | ||
| Definition | df-ldlf 33887 | Definition of a Lindelöf space. A Lindelöf space is a topological space in which every open cover has a countable subcover. Definition 1 of [BourbakiTop2] p. 195. (Contributed by Thierry Arnoux, 30-Jan-2020.) |
| ⊢ Ldlf = CovHasRef{𝑥 ∣ 𝑥 ≼ ω} | ||
| Theorem | ldlfcntref 33888* | Every open cover of a Lindelöf space has a countable refinement. (Contributed by Thierry Arnoux, 1-Feb-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Ldlf ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ≼ ω ∧ 𝑣Ref𝑈)) | ||
| Syntax | cpcmp 33889 | Extend class notation with the class of all paracompact topologies. |
| class Paracomp | ||
| Definition | df-pcmp 33890 | Definition of a paracompact topology. A topology is said to be paracompact iff every open cover has an open refinement that is locally finite. The definition 6 of [BourbakiTop1] p. I.69. also requires the topology to be Hausdorff, but this is dropped here. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ Paracomp = {𝑗 ∣ 𝑗 ∈ CovHasRef(LocFin‘𝑗)} | ||
| Theorem | ispcmp 33891 | The predicate "is a paracompact topology". (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Paracomp ↔ 𝐽 ∈ CovHasRef(LocFin‘𝐽)) | ||
| Theorem | cmppcmp 33892 | Every compact space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Paracomp) | ||
| Theorem | dispcmp 33893 | Every discrete space is paracompact. (Contributed by Thierry Arnoux, 7-Jan-2020.) |
| ⊢ (𝑋 ∈ 𝑉 → 𝒫 𝑋 ∈ Paracomp) | ||
| Theorem | pcmplfin 33894* | Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement 𝑣 that is locally finite. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑣 ∈ 𝒫 𝐽(𝑣 ∈ (LocFin‘𝐽) ∧ 𝑣Ref𝑈)) | ||
| Theorem | pcmplfinf 33895* | Given a paracompact topology 𝐽 and an open cover 𝑈, there exists an open refinement ran 𝑓 that is locally finite, using the same index as the original cover 𝑈. (Contributed by Thierry Arnoux, 31-Jan-2020.) |
| ⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Paracomp ∧ 𝑈 ⊆ 𝐽 ∧ 𝑋 = ∪ 𝑈) → ∃𝑓(𝑓:𝑈⟶𝐽 ∧ ran 𝑓Ref𝑈 ∧ ran 𝑓 ∈ (LocFin‘𝐽))) | ||
The prime ideals of a ring 𝑅 can be endowed with the Zariski topology. This is done by defining a function 𝑉 which maps ideals of 𝑅 to closed sets (see for example zarcls0 33902 for the definition of 𝑉). The closed sets of the topology are in the range of 𝑉 (see zartopon 33911). The correspondence with the open sets is made in zarcls 33908. As proved in zart0 33913, the Zariski topology is T0 , but generally not T1 . | ||
| Syntax | crspec 33896 | Extend class notation with the spectrum of a ring. |
| class Spec | ||
| Definition | df-rspec 33897 | Define the spectrum of a ring. (Contributed by Thierry Arnoux, 21-Jan-2024.) |
| ⊢ Spec = (𝑟 ∈ Ring ↦ ((IDLsrg‘𝑟) ↾s (PrmIdeal‘𝑟))) | ||
| Theorem | rspecval 33898 | Value of the spectrum of the ring 𝑅. Notation 1.1.1 of [EGA] p. 80. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ (𝑅 ∈ Ring → (Spec‘𝑅) = ((IDLsrg‘𝑅) ↾s (PrmIdeal‘𝑅))) | ||
| Theorem | rspecbas 33899 | The prime ideals form the base of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (PrmIdeal‘𝑅) = (Base‘𝑆)) | ||
| Theorem | rspectset 33900* | Topology component of the spectrum of a ring. (Contributed by Thierry Arnoux, 2-Jun-2024.) |
| ⊢ 𝑆 = (Spec‘𝑅) & ⊢ 𝐼 = (LIdeal‘𝑅) & ⊢ 𝐽 = ran (𝑖 ∈ 𝐼 ↦ {𝑗 ∈ 𝐼 ∣ ¬ 𝑖 ⊆ 𝑗}) ⇒ ⊢ (𝑅 ∈ Ring → 𝐽 = (TopSet‘𝑆)) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |