Home | Metamath
Proof Explorer Theorem List (p. 215 of 449) | < 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-28623) |
Hilbert Space Explorer
(28624-30146) |
Users' Mathboxes
(30147-44804) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulfsupp 21401* | A mapping of values of the "characteristic factor function" multiplied with a constant polynomial matrix is finitely supported. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ ↑ = (.g‘(mulGrp‘𝑌)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum 21402* | Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ ↑ = (.g‘(mulGrp‘𝑌)) & ⊢ + = (+g‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum2 21403* | Breaking up a sum of values of the "characteristic factor function" multiplied with a constant polynomial matrix. (Contributed by AV, 23-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ ↑ = (.g‘(mulGrp‘𝑌)) & ⊢ + = (+g‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem1 21404* | Lemma 1 for cayleyhamilton 21428. (Contributed by AV, 11-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ ↑ = (.g‘(mulGrp‘𝑌)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In this section, a direct algebraic proof for the Cayley-Hamilton theorem is
provided, according to Wikipedia ("Cayley-Hamilton theorem", 09-Nov-2019,
https://en.wikipedia.org/wiki/Cayley%E2%80%93Hamilton_theorem, section
"A direct algebraic proof" (this approach is also used for proving Lemma 1.9 in
[Hefferon] p. 427):
Using this notation, we have:
Following the proof shown in Wikipedia, the following steps are performed:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadurid 21405 | The right-hand fundamental relation of the adjugate (see madurid 21183) applied to the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ − = (-g‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ × = (.r‘𝑌) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐼 × (𝐽‘𝐼)) = ((𝐶‘𝑀) · 1 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsum 21406* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum. (Contributed by AV, 7-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐻 = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑛)) · 1 ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsumm2pm 21407* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as group sum with a matrix to polynomial matrix transformation. (Contributed by AV, 13-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) & ⊢ 𝑂 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐻 = (𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) · (𝑇‘(((coe1‘𝐾)‘𝑛) ∗ 𝑂)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem1 21408* | Lemma 1 for cpmidpmat 21411. (Contributed by AV, 13-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) & ⊢ 𝑂 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑘) ∗ 𝑂)) ⇒ ⊢ (𝐿 ∈ ℕ0 → (𝐺‘𝐿) = (((coe1‘𝐾)‘𝐿) ∗ 𝑂)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem2 21409* | Lemma 2 for cpmidpmat 21411. (Contributed by AV, 14-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) & ⊢ 𝑂 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑘) ∗ 𝑂)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ (𝐵 ↑m ℕ0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem3 21410* | Lemma 3 for cpmidpmat 21411. (Contributed by AV, 14-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) & ⊢ 𝑂 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑘 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑘) ∗ 𝑂)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝐺 finSupp (0g‘𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmat 21411* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as polynomial over the ring of matrices. (Contributed by AV, 14-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) & ⊢ 𝑂 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑍 = (var1‘𝐴) & ⊢ ∙ = ( ·𝑠 ‘𝑄) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑄)) & ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐼‘𝐻) = (𝑄 Σg (𝑛 ∈ ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 𝑂) ∙ (𝑛𝐸𝑍))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemB 21412* | Lemma B for cpmadugsum 21416. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemC 21413* | Lemma C for cpmadugsum 21416. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemF 21414* | Lemma F for cpmadugsum 21416. (Contributed by AV, 7-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) − ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumfi 21415* | The product of the characteristic matrix of a given matrix and its adjunct represented as finite sum. (Contributed by AV, 7-Nov-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐼 × (𝐽‘𝐼)) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsum 21416* | The product of the characteristic matrix of a given matrix and its adjunct represented as an infinite sum. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐼 × (𝐽‘𝐼)) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidgsum2 21417* | Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐻 = (𝐾 · 1 ) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))𝐻 = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidg2sum 21418* | Equality of two sums representing the identity matrix multiplied with the characteristic polynomial of a matrix. (Contributed by AV, 11-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝐼 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝑈 = (algSc‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · ((𝑈‘((coe1‘𝐾)‘𝑖)) · 1 )))) = (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpolylem1 21419* | Lemma 1 for cpmadumatpoly 21421. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑍 = (var1‘𝑅) & ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) ⇒ ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) ∈ (𝐵 ↑m ℕ0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpolylem2 21420* | Lemma 2 for cpmadumatpoly 21421. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑍 = (var1‘𝑅) & ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) ⇒ ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑠 ∈ ℕ) ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) → (𝑈 ∘ 𝐺) finSupp (0g‘𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadumatpoly 21421* | The product of the characteristic matrix of a given matrix and its adjunct represented as a polynomial over matrices. (Contributed by AV, 20-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑍 = (var1‘𝑅) & ⊢ 𝐷 = ((𝑍 · 1 ) − (𝑇‘𝑀)) & ⊢ 𝐽 = (𝑁 maAdju 𝑃) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) & ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐼‘(𝐷 × (𝐽‘𝐷))) = (𝑄 Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛)) ∗ (𝑛 ↑ 𝑋))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem2 21422 | Lemma for cayhamlem3 21425. (Contributed by AV, 24-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ · = (.r‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑m ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀)) = ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeqlem 21423* | Lemma for chcoeffeq 21424. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 7-Dec-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((𝑈‘(𝐺‘𝑛))( ·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) = ((Poly1‘𝐴) Σg (𝑛 ∈ ℕ0 ↦ ((((coe1‘𝐾)‘𝑛) ∗ 1 )( ·𝑠 ‘(Poly1‘𝐴))(𝑛(.g‘(mulGrp‘(Poly1‘𝐴)))(var1‘𝐴))))) → ∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeq 21424* | The coefficients of the characteristic polynomial multiplied with the identity matrix represented by (transformed) ring elements obtained from the adjunct of the characteristic matrix. (Contributed by AV, 21-Nov-2019.) (Proof shortened by AV, 8-Dec-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))∀𝑛 ∈ ℕ0 (𝑈‘(𝐺‘𝑛)) = (((coe1‘𝐾)‘𝑛) ∗ 1 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem3 21425* | Lemma for cayhamlem4 21426. (Contributed by AV, 24-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ · = (.r‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑀) · (𝑈‘(𝐺‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem4 21426* | Lemma for cayleyhamilton 21428. (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (𝐶‘𝑀) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑌)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑏 ∈ (𝐵 ↑m (0...𝑠))(𝐴 Σg (𝑛 ∈ ℕ0 ↦ (((coe1‘𝐾)‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = (𝑈‘(𝑌 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸(𝑇‘𝑀)) × (𝐺‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton0 21427* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 21428 provides definitions not used in the theorem itself, but in its proof to make it clearer, more readable and shorter compared with a proof without them (see cayleyhamiltonALT 21429)! (Contributed by AV, 25-Nov-2019.) (Revised by AV, 15-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (coe1‘(𝐶‘𝑀)) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 𝑍 = (0g‘𝑌) & ⊢ 𝑊 = (Base‘𝑌) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑌)) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, (𝑍 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 𝑍, ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑈 = (𝑁 cPolyMatToMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton 21428* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", see theorem 7.8 in [Roman] p. 170 (without proof!), or theorem 3.1 in [Lang] p. 561. In other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. This is Metamath 100 proof #49. (Contributed by Alexander van der Vekens, 25-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (coe1‘(𝐶‘𝑀)) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamiltonALT 21429* | Alternate proof of cayleyhamilton 21428, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 21427 directly, but has the same structure as the proof of cayleyhamilton0 21427. In contrast to the proof of cayleyhamilton0 21427, only the definitions required to formulate the theorem itself are used, causing the definitions used in the lemmas being expanded, which makes the proof longer and more difficult to read. (Contributed by AV, 25-Nov-2019.) (New usage is discouraged.) (Proof modification is discouraged.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (coe1‘(𝐶‘𝑀)) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐾‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayleyhamilton1 21430* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation", or, in other words, a matrix over a commutative ring "inserted" into its characteristic polynomial results in zero. In this variant of cayleyhamilton 21428, the meaning of "inserted" is made more transparent: If the characteristic polynomial is a polynomial with coefficients (𝐹‘𝑛), then a matrix over a commutative ring "inserted" into its characteristic polynomial is the sum of these coefficients multiplied with the corresponding power of the matrix. (Contributed by AV, 25-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐾 = (coe1‘(𝐶‘𝑀)) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ 𝐿 = (Base‘𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑍 = (0g‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐹 ∈ (𝐿 ↑m ℕ0) ∧ 𝐹 finSupp 𝑍)) → ((𝐶‘𝑀) = (𝑃 Σg (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) · (𝑛𝐸𝑋)))) → (𝐴 Σg (𝑛 ∈ ℕ0 ↦ ((𝐹‘𝑛) ∗ (𝑛 ↑ 𝑀)))) = 0 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
A topology on a set is a set of subsets of that set, called open sets, which satisfy certain conditions. One condition is that the whole set be an open set. Therefore, a set is recoverable from a topology on it (as its union, see toponuni 21452), and it may sometimes be more convenient to consider topologies without reference to the underlying set. This is why we define successively the class of topologies (df-top 21432), then the function which associates with a set the set of topologies on it (df-topon 21449), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp 21471). Of course, a topology is the same thing as a topology on a set (see toprntopon 21463). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctop 21431 | Syntax for the class of topologies. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-top 21432* |
Define the class of topologies. It is a proper class (see topnex 21534).
See istopg 21433 and istop2g 21434 for the corresponding characterizations,
using respectively binary intersections like in this definition and
nonempty finite intersections.
The final form of the definition is due to Bourbaki (Def. 1 of [BourbakiTop1] p. I.1), while the idea of defining a topology in terms of its open sets is due to Aleksandrov. For the convoluted history of the definitions of these notions, see Gregory H. Moore, The emergence of open sets, closed sets, and limit points in analysis and topology, Historia Mathematica 35 (2008) 220--241. (Contributed by NM, 3-Mar-2006.) (Revised by BJ, 20-Oct-2018.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Top = {𝑥 ∣ (∀𝑦 ∈ 𝒫 𝑥∪ 𝑦 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ∈ 𝑥)} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istopg 21433* |
Express the predicate "𝐽 is a topology". See istop2g 21434 for another
characterization using nonempty finite intersections instead of binary
intersections.
Note: In the literature, a topology is often represented by a calligraphic letter T, which resembles the letter J. This confusion may have led to J being used by some authors (e.g., K. D. Joshi, Introduction to General Topology (1983), p. 114) and it is convenient for us since we later use 𝑇 to represent linear transformations (operators). (Contributed by Stefan Allan, 3-Mar-2006.) (Revised by Mario Carneiro, 11-Nov-2013.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥 ∈ 𝐽 ∀𝑦 ∈ 𝐽 (𝑥 ∩ 𝑦) ∈ 𝐽))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istop2g 21434* | Express the predicate "𝐽 is a topology" using nonempty finite intersections instead of binary intersections as in istopg 21433. (Contributed by NM, 19-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uniopn 21435 | The union of a subset of a topology (that is, the union of any family of open sets of a topology) is an open set. (Contributed by Stefan Allan, 27-Feb-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽) → ∪ 𝐴 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iunopn 21436* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | inopn 21437 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fitop 21438 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → (fi‘𝐽) = 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fiinopn 21439 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iinopn 21440* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | unopn 21441 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0opn 21442 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0ntop 21443 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ¬ ∅ ∈ Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topopn 21444 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltopss 21445 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | riinopn 21446* | A finite indexed relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ Fin ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → (𝑋 ∩ ∩ 𝑥 ∈ 𝐴 𝐵) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | rintopn 21447 | A finite relative intersection of open sets is open. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝐽 ∧ 𝐴 ∈ Fin) → (𝑋 ∩ ∩ 𝐴) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctopon 21448 | Syntax for the function of topologies on sets. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-topon 21449* | Define the function that associates with a set the set of topologies on it. (Contributed by Stefan O'Rear, 31-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ TopOn = (𝑏 ∈ V ↦ {𝑗 ∈ Top ∣ 𝑏 = ∪ 𝑗}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istopon 21450 | Property of being a topology with a given base set. (Contributed by Stefan O'Rear, 31-Jan-2015.) (Revised by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝐵) ↔ (𝐽 ∈ Top ∧ 𝐵 = ∪ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontop 21451 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐽 ∈ Top) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponuni 21452 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 = ∪ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontopi 21453 | A topology on a given base set is a topology. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐽 ∈ Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponunii 21454 | The base set of a topology on a given base set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐽 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐵 = ∪ 𝐽 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toptopon 21455 | Alternative definition of Top in terms of TopOn. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘𝑋)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toptopon2 21456 | A topology is the same thing as a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top ↔ 𝐽 ∈ (TopOn‘∪ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontopon 21457 | A topology on a set is a topology on the union of its open sets. (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝑋) → 𝐽 ∈ (TopOn‘∪ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | funtopon 21458 | The class TopOn is a function. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Fun TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponrestid 21459 | Given a topology on a set, restricting it to that same set has no effect. (Contributed by Jim Kingdon, 6-Jul-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 ∈ (TopOn‘𝐵) ⇒ ⊢ 𝐴 = (𝐴 ↾t 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponsspwpw 21460 | The set of topologies on a set is included in the double power set of that set. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (TopOn‘𝐴) ⊆ 𝒫 𝒫 𝐴 | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | dmtopon 21461 | The domain of TopOn is V. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ dom TopOn = V | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fntopon 21462 | The class TopOn is a function with domain V. Analogue for topologies of fnmre 16852 for Moore collections. (Contributed by BJ, 29-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ TopOn Fn V | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toprntopon 21463 | A topology is the same thing as a topology on a set (variable-free version). (Contributed by BJ, 27-Apr-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ Top = ∪ ran TopOn | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponmax 21464 | The base set of a topology is an open set. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝐵) → 𝐵 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponss 21465 | A member of a topology is a subset of its underlying set. (Contributed by Mario Carneiro, 21-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ (TopOn‘𝑋) ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponcom 21466 | If 𝐾 is a topology on the base set of topology 𝐽, then 𝐽 is a topology on the base of 𝐾. (Contributed by Mario Carneiro, 22-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ (TopOn‘∪ 𝐽)) → 𝐽 ∈ (TopOn‘∪ 𝐾)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | toponcomb 21467 | Biconditional form of toponcom 21466. (Contributed by BJ, 5-Dec-2021.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐾 ∈ Top) → (𝐽 ∈ (TopOn‘∪ 𝐾) ↔ 𝐾 ∈ (TopOn‘∪ 𝐽))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topgele 21468 | The topologies over the same set have the greatest element (the discrete topology) and the least element (the indiscrete topology). (Contributed by FL, 18-Apr-2010.) (Revised by Mario Carneiro, 16-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘𝑋) → ({∅, 𝑋} ⊆ 𝐽 ∧ 𝐽 ⊆ 𝒫 𝑋)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topsn 21469 | The only topology on a singleton is the discrete topology (which is also the indiscrete topology by pwsn 4824). (Contributed by FL, 5-Jan-2009.) (Revised by Mario Carneiro, 16-Sep-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ (TopOn‘{𝐴}) → 𝐽 = 𝒫 {𝐴}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctps 21470 | Syntax for the class of topological spaces. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class TopSp | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-topsp 21471 | Define the class of topological spaces (as extensible structures). (Contributed by Stefan O'Rear, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ TopSp = {𝑓 ∣ (TopOpen‘𝑓) ∈ (TopOn‘(Base‘𝑓))} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istps 21472 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ 𝐽 ∈ (TopOn‘𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istps2 21473 | Express the predicate "is a topological space." (Contributed by NM, 20-Oct-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp ↔ (𝐽 ∈ Top ∧ 𝐴 = ∪ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tpsuni 21474 | The base set of a topological space. (Contributed by FL, 27-Jun-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐴 = ∪ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tpstop 21475 | The topology extractor on a topological space is a topology. (Contributed by FL, 27-Jun-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐽 = (TopOpen‘𝐾) ⇒ ⊢ (𝐾 ∈ TopSp → 𝐽 ∈ Top) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tpspropd 21476 | A topological space depends only on the base and topology components. (Contributed by NM, 18-Jul-2006.) (Revised by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tpsprop2d 21477 | A topological space depends only on the base and topology components. (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) & ⊢ (𝜑 → (TopSet‘𝐾) = (TopSet‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ TopSp ↔ 𝐿 ∈ TopSp)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topontopn 21478 | Express the predicate "is a topological space." (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐽 = (TopOpen‘𝐾)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tsettps 21479 | If the topology component is already correctly truncated, then it forms a topological space (with the topology extractor function coming out the same as the component). (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (Base‘𝐾) & ⊢ 𝐽 = (TopSet‘𝐾) ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | istpsi 21480 | Properties that determine a topological space. (Contributed by NM, 20-Oct-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (Base‘𝐾) = 𝐴 & ⊢ (TopOpen‘𝐾) = 𝐽 & ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈ Top ⇒ ⊢ 𝐾 ∈ TopSp | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltpsg 21481 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} ⇒ ⊢ (𝐽 ∈ (TopOn‘𝐴) → 𝐾 ∈ TopSp) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltpsi 21482 | Properties that determine a topological space from a construction (using no explicit indices). (Contributed by NM, 20-Oct-2012.) (Revised by Mario Carneiro, 13-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = {〈(Base‘ndx), 𝐴〉, 〈(TopSet‘ndx), 𝐽〉} & ⊢ 𝐴 = ∪ 𝐽 & ⊢ 𝐽 ∈ Top ⇒ ⊢ 𝐾 ∈ TopSp | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctb 21483 | Syntax for the class of topological bases. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class TopBases | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-bases 21484* | Define the class of topological bases. Equivalent to definition of basis in [Munkres] p. 78 (see isbasis2g 21486). Note that "bases" is the plural of "basis". (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ TopBases = {𝑥 ∣ ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦 ∩ 𝑧) ⊆ ∪ (𝑥 ∩ 𝒫 (𝑦 ∩ 𝑧))} | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isbasisg 21485* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ⊆ ∪ (𝐵 ∩ 𝒫 (𝑥 ∩ 𝑦)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isbasis2g 21486* | Express the predicate "the set 𝐵 is a basis for a topology". (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | isbasis3g 21487* | Express the predicate "the set 𝐵 is a basis for a topology". Definition of basis in [Munkres] p. 78. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝐶 → (𝐵 ∈ TopBases ↔ (∀𝑥 ∈ 𝐵 𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ ∪ 𝐵∃𝑦 ∈ 𝐵 𝑥 ∈ 𝑦 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 ∀𝑧 ∈ (𝑥 ∩ 𝑦)∃𝑤 ∈ 𝐵 (𝑧 ∈ 𝑤 ∧ 𝑤 ⊆ (𝑥 ∩ 𝑦))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basis1 21488 | Property of a basis. (Contributed by NM, 16-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵 ∧ 𝐷 ∈ 𝐵) → (𝐶 ∩ 𝐷) ⊆ ∪ (𝐵 ∩ 𝒫 (𝐶 ∩ 𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basis2 21489* | Property of a basis. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (((𝐵 ∈ TopBases ∧ 𝐶 ∈ 𝐵) ∧ (𝐷 ∈ 𝐵 ∧ 𝐴 ∈ (𝐶 ∩ 𝐷))) → ∃𝑥 ∈ 𝐵 (𝐴 ∈ 𝑥 ∧ 𝑥 ⊆ (𝐶 ∩ 𝐷))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fiinbas 21490* | If a set is closed under finite intersection, then it is a basis for a topology. (Contributed by Jeff Madsen, 2-Sep-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐵 ∈ 𝐶 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ∩ 𝑦) ∈ 𝐵) → 𝐵 ∈ TopBases) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | basdif0 21491 | A basis is not affected by the addition or removal of the empty set. (Contributed by Mario Carneiro, 28-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐵 ∖ {∅}) ∈ TopBases ↔ 𝐵 ∈ TopBases) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | baspartn 21492* | A disjoint system of sets is a basis for a topology. (Contributed by Stefan O'Rear, 22-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝑃 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝑃 ∀𝑦 ∈ 𝑃 (𝑥 = 𝑦 ∨ (𝑥 ∩ 𝑦) = ∅)) → 𝑃 ∈ TopBases) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tgval 21493* | The topology generated by a basis. See also tgval2 21494 and tgval3 21501. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ 𝑥 ⊆ ∪ (𝐵 ∩ 𝒫 𝑥)}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | tgval2 21494* | Definition of a topology generated by a basis in [Munkres] p. 78. Later we show (in tgcl 21507) that (topGen‘𝐵) is indeed a topology (on ∪ 𝐵, see unitg 21505). See also tgval 21493 and tgval3 21501. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (topGen‘𝐵) = {𝑥 ∣ (𝑥 ⊆ ∪ 𝐵 ∧ ∀𝑦 ∈ 𝑥 ∃𝑧 ∈ 𝐵 (𝑦 ∈ 𝑧 ∧ 𝑧 ⊆ 𝑥))}) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg 21495 | Membership in a topology generated by a basis. (Contributed by NM, 16-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ 𝐴 ⊆ ∪ (𝐵 ∩ 𝒫 𝐴))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg2 21496* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Revised by Mario Carneiro, 10-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ (𝐴 ⊆ ∪ 𝐵 ∧ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg2b 21497* | Membership in a topology generated by a basis. (Contributed by Mario Carneiro, 17-Jun-2014.) (Revised by Mario Carneiro, 10-Jan-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∀𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 (𝑥 ∈ 𝑦 ∧ 𝑦 ⊆ 𝐴))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg4i 21498 | An open set in a topology generated by a basis is the union of all basic open sets contained in it. (Contributed by Stefan O'Rear, 22-Feb-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐴 ∈ (topGen‘𝐵) → 𝐴 = ∪ (𝐵 ∩ 𝒫 𝐴)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg3i 21499 | The union of a set of basic open sets is in the generated topology. (Contributed by Mario Carneiro, 30-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐵 ∈ 𝑉 ∧ 𝐴 ⊆ 𝐵) → ∪ 𝐴 ∈ (topGen‘𝐵)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltg3 21500* | Membership in a topology generated by a basis. (Contributed by NM, 15-Jul-2006.) (Proof shortened by Mario Carneiro, 30-Aug-2015.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐵 ∈ 𝑉 → (𝐴 ∈ (topGen‘𝐵) ↔ ∃𝑥(𝑥 ⊆ 𝐵 ∧ 𝐴 = ∪ 𝑥))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |