Home | Metamath
Proof Explorer Theorem List (p. 205 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw2lem 20401* | Lemma for pmatcollpw2 20402. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑛 ∈ ℕ0 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑖(𝑀 decompPMat 𝑛)𝑗) × (𝑛 ↑ 𝑋)))) finSupp (0g‘𝐶)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw2 20402* | Write a polynomial matrix as sum of matrices whose entries are products of variable powers and constant polynomials collecting like powers. (Contributed by AV, 3-Oct-2019.) (Revised by AV, 3-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ × = ( ·𝑠 ‘𝑃) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((𝑖(𝑀 decompPMat 𝑛)𝑗) × (𝑛 ↑ 𝑋)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | monmatcollpw 20403 | The matrix consisting of the coefficients in the polynomial entries of a polynomial matrix having scaled monomials with the same power as entries is the matrix of the coefficients of the monomials or a zero matrix. Generalization of decpmatid 20394 (but requires 𝑅 to be commutative!). (Contributed by AV, 11-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐾 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0 ∧ 𝐼 ∈ ℕ0)) → (((𝐿 ↑ 𝑋) · (𝑇‘𝑀)) decompPMat 𝐼) = if(𝐼 = 𝐿, 𝑀, 0 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpwlem 20404 | Lemma for pmatcollpw 20405. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ 𝑛 ∈ ℕ0) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁) → ((𝑎(𝑀 decompPMat 𝑛)𝑏)( ·𝑠 ‘𝑃)(𝑛 ↑ 𝑋)) = (𝑎((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))𝑏)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw 20405* | Write a polynomial matrix (over a commutative ring) as sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 26-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpwfi 20406* | Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3lem 20407* | Lemma for pmatcollpw3 20408 and pmatcollpw3fi 20409: Write a polynomial matrix (over a commutative ring) as sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ⊆ ℕ0 ∧ 𝐼 ≠ ∅)) → (𝑀 = (𝐶 Σg (𝑛 ∈ 𝐼 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑀 decompPMat 𝑛))))) → ∃𝑓 ∈ (𝐷 ↑𝑚 𝐼)𝑀 = (𝐶 Σg (𝑛 ∈ 𝐼 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3 20408* | Write a polynomial matrix (over a commutative ring) as sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 27-Oct-2019.) (Revised by AV, 4-Dec-2019.) (Proof shortened by AV, 8-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑓 ∈ (𝐷 ↑𝑚 ℕ0)𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3fi 20409* | Write a polynomial matrix (over a commutative ring) as a finite sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 4-Nov-2019.) (Revised by AV, 4-Dec-2019.) (Proof shortened by AV, 8-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ0 ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3fi1lem1 20410* | Lemma 1 for pmatcollpw3fi1 20412. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) & ⊢ 0 = (0g‘𝐴) & ⊢ 𝐻 = (𝑙 ∈ (0...1) ↦ if(𝑙 = 0, (𝐺‘0), 0 )) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ 𝐺 ∈ (𝐷 ↑𝑚 {0}) ∧ 𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐺‘𝑛)))))) → 𝑀 = (𝐶 Σg (𝑛 ∈ (0...1) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝐻‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3fi1lem2 20411* | Lemma 2 for pmatcollpw3fi1 20412. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (∃𝑓 ∈ (𝐷 ↑𝑚 {0})𝑀 = (𝐶 Σg (𝑛 ∈ {0} ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpw3fi1 20412* | Write a polynomial matrix (over a commutative ring) as a finite sum of (at least two) products of variable powers and constant matrices with scalar entries. (Contributed by AV, 6-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ∃𝑠 ∈ ℕ ∃𝑓 ∈ (𝐷 ↑𝑚 (0...𝑠))𝑀 = (𝐶 Σg (𝑛 ∈ (0...𝑠) ↦ ((𝑛 ↑ 𝑋) ∗ (𝑇‘(𝑓‘𝑛)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpwscmatlem1 20413 | Lemma 1 for pmatcollpwscmat 20415. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 1 = (1r‘𝐶) & ⊢ 𝑀 = (𝑄 ∗ 1 ) ⇒ ⊢ ((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸)) ∧ (𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁)) → (((coe1‘(𝑎𝑀𝑏))‘𝐿)( ·𝑠 ‘𝑃)(0(.g‘(mulGrp‘𝑃))(var1‘𝑅))) = if(𝑎 = 𝑏, (𝑈‘((coe1‘𝑄)‘𝐿)), (0g‘𝑃))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpwscmatlem2 20414 | Lemma 2 for pmatcollpwscmat 20415. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 1 = (1r‘𝐶) & ⊢ 𝑀 = (𝑄 ∗ 1 ) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝐿 ∈ ℕ0 ∧ 𝑄 ∈ 𝐸)) → (𝑇‘(𝑀 decompPMat 𝐿)) = ((𝑈‘((coe1‘𝑄)‘𝐿)) ∗ 1 )) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmatcollpwscmat 20415* | Write a scalar matrix over polynomials (over a commutative ring) as sum of the product of variable powers and constant scalar matrices with scalar entries. (Contributed by AV, 2-Nov-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝐶) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐷 = (Base‘𝐴) & ⊢ 𝑈 = (algSc‘𝑃) & ⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 1 = (1r‘𝐶) & ⊢ 𝑀 = (𝑄 ∗ 1 ) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑄 ∈ 𝐸) → 𝑀 = (𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛 ↑ 𝑋) ∗ ((𝑈‘((coe1‘𝑄)‘𝑛)) ∗ 1 ))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The main result of this section is theorem pmmpric 20447, which shows that the
ring of polynomial matrices and the ring of polynomials having matrices as
coefficients (called "polynomials over matrices" in the following) are
isomorphic:
| ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cpm2mp 20416 | Extend class notation with the transformation of a polynomial matrix into a polynomial over matrices. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class pMatToMatPoly | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-pm2mp 20417* | Transformation of a polynomial matrix (over a ring) into a polynomial over matrices (over the same ring). (Contributed by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ pMatToMatPoly = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat (Poly1‘𝑟))) ↦ ⦋(𝑛 Mat 𝑟) / 𝑎⦌⦋(Poly1‘𝑎) / 𝑞⦌(𝑞 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘)( ·𝑠 ‘𝑞)(𝑘(.g‘(mulGrp‘𝑞))(var1‘𝑎))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf1lem 20418* | Lemma for pm2mpf1 20423. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑈 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0)) → ((coe1‘(𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑈 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))‘𝐾) = (𝑈 decompPMat 𝐾)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpval 20419* | Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝑇 = (𝑚 ∈ 𝐵 ↦ (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑚 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpfval 20420* | A polynomial matrix transformed into a polynomial over matrices. (Contributed by AV, 4-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) = (𝑄 Σg (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpcl 20421 | The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐿 = (Base‘𝑄) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑇‘𝑀) ∈ 𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf 20422 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 5-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐿 = (Base‘𝑄) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵⟶𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf1 20423 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices to polynomials over matrices. (Contributed by AV, 14-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐿 = (Base‘𝑄) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1→𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpcoe1 20424 | A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑀 ∈ 𝐵 ∧ 𝐾 ∈ ℕ0)) → ((coe1‘(𝑇‘𝑀))‘𝐾) = (𝑀 decompPMat 𝐾)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | idpm2idmp 20425 | The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑇‘(1r‘𝐶)) = (1r‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mptcoe1matfsupp 20426* | The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019.) (Proof shortened by AV, 23-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ (𝐼((coe1‘𝑂)‘𝑘)𝐽)) finSupp (0g‘𝑅)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcllem 20427* | Lemma for mply1topmatcl 20429. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁) → (𝑘 ∈ ℕ0 ↦ ((𝐼((coe1‘𝑂)‘𝑘)𝐽) · (𝑘𝐸𝑌))) finSupp (0g‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatval 20428* | A polynomial over matrices transformed into a polynomial matrix. 𝐼 is the inverse function of the transformation 𝑇 of polynomial matrices into polynomials over matrices: (𝑇‘(𝐼‘𝑂)) = 𝑂) (see mp2pm2mp 20435). (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) ⇒ ⊢ ((𝑁 ∈ 𝑉 ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mply1topmatcl 20429* | A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) ∈ 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem1 20430* | Lemma 1 for mp2pm2mp 20435. (Contributed by AV, 9-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝐼‘𝑂) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem2 20431* | Lemma 2 for mp2pm2mp 20435. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌))))) ∈ 𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem3 20432* | Lemma 3 for mp2pm2mp 20435. (Contributed by AV, 10-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ ((coe1‘(𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑂)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))‘𝐾))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem4 20433* | Lemma 4 for mp2pm2mp 20435. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝑃 = (Poly1‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) ∧ 𝐾 ∈ ℕ0) → ((𝐼‘𝑂) decompPMat 𝐾) = ((coe1‘𝑂)‘𝐾)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem5 20434* | Lemma 5 for mp2pm2mp 20435. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 5-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑘 ∈ ℕ0 ↦ (((𝐼‘𝑂) decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mp 20435* | A polynomial over matrices transformed into a polynomial matrix transformed back into the polynomial over matrices. (Contributed by AV, 12-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ 𝐼 = (𝑝 ∈ 𝐿 ↦ (𝑖 ∈ 𝑁, 𝑗 ∈ 𝑁 ↦ (𝑃 Σg (𝑘 ∈ ℕ0 ↦ ((𝑖((coe1‘𝑝)‘𝑘)𝑗) · (𝑘𝐸𝑌)))))) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑂 ∈ 𝐿) → (𝑇‘(𝐼‘𝑂)) = 𝑂) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghmlem2 20436* | Lemma 2 for pm2mpghm 20440. (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝑘 ∈ ℕ0 ↦ ((𝑀 decompPMat 𝑘) ∗ (𝑘 ↑ 𝑋))) finSupp (0g‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghmlem1 20437 | Lemma 1 for pm2mpghm . (Contributed by AV, 15-Oct-2019.) (Revised by AV, 4-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ ℕ0) → ((𝑀 decompPMat 𝐾) ∗ (𝐾 ↑ 𝑋)) ∈ 𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpfo 20438 | The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–onto→𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpf1o 20439 | The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇:𝐵–1-1-onto→𝐿) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpghm 20440 | The transformation of polynomial matrices into polynomials over matrices is an additive group homomorphism. (Contributed by AV, 16-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 GrpHom 𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpgrpiso 20441 | The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 GrpIso 𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhmlem1 20442* | Lemma 1 for pm2mpmhm 20444. (Contributed by AV, 21-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐿 = (Base‘𝑄) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) ∧ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵)) → (𝑙 ∈ ℕ0 ↦ ((𝐴 Σg (𝑘 ∈ (0...𝑙) ↦ ((𝑥 decompPMat 𝑘)(.r‘𝐴)(𝑦 decompPMat (𝑙 − 𝑘))))) ∗ (𝑙 ↑ 𝑋))) finSupp (0g‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhmlem2 20443* | Lemma 2 for pm2mpmhm 20444. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhm 20444 | The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ ((mulGrp‘𝐶) MndHom (mulGrp‘𝑄))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mprhm 20445 | The transformation of polynomial matrices into polynomials over matrices is a ring homomorphism. (Contributed by AV, 22-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 RingHom 𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mprngiso 20446 | The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝑇 ∈ (𝐶 RingIso 𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pmmpric 20447 | The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐶 ≃𝑟 𝑄) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | monmat2matmon 20448 | The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐾 = (Base‘𝐴) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐾 ∧ 𝐿 ∈ ℕ0)) → (𝐼‘((𝐿𝐸𝑌) · (𝑇‘𝑀))) = (𝑀 ∗ (𝐿 ↑ 𝑋))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mp 20449* | The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019.) (Revised by AV, 7-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐵 = (Base‘𝐶) & ⊢ ∗ = ( ·𝑠 ‘𝑄) & ⊢ ↑ = (.g‘(mulGrp‘𝑄)) & ⊢ 𝑋 = (var1‘𝐴) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐾 = (Base‘𝐴) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝐼 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐸 = (.g‘(mulGrp‘𝑃)) & ⊢ 𝑌 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝐶) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ (𝐾 ↑𝑚 ℕ0) ∧ 𝑀 finSupp (0g‘𝐴))) → (𝐼‘(𝐶 Σg (𝑛 ∈ ℕ0 ↦ ((𝑛𝐸𝑌) · (𝑇‘(𝑀‘𝑛)))))) = (𝑄 Σg (𝑛 ∈ ℕ0 ↦ ((𝑀‘𝑛) ∗ (𝑛 ↑ 𝑋))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "In linear algebra, the characteristic polynomial of a square matrix is a polynomial which is invariant under matrix similarity and has the eigenvalues as roots. It has the determinant and the trace of the matrix as coefficients.". Based on the definition of the characteristic polynomial of a square matrix (df-chpmat 20451) the eigenvalues and corresponding eigenvectors can be defined. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The characteristic polynomial of a matrix 𝐴 is the determinat of the characteristic matrix of 𝐴: (𝑡𝐼 − 𝐴). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cchpmat 20450 | Extend class notation with the characteristic polynomial. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class CharPlyMat | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-chpmat 20451* | Define the characteristic polynomial of a square matrix. According to Wikipedia ("Characteristic polynomial", 31-Jul-2019, https://en.wikipedia.org/wiki/Characteristic_polynomial): "The characteristic polynomial of [an n x n matrix] A, denoted by pA(t), is the polynomial defined by pA ( t ) = det ( t I - A ) where I denotes the n-by-n identity matrix.". In addition, however, the underlying ring must be commutative, see definition in [Lang], p. 561: " Let k be a commutative ring ... Let M be any n x n matrix in k ... We define the characteristic polynomial PM(t) to be the determinant det ( t In - M ) where In is the unit n x n matrix." To be more precise, the matrices A and I on the right hand side are matrices with coefficients of a polynomial ring. Therefore, the original matrix A over a given commutative ring must be transformed into corresponding matrices over the polynomial ring over the given ring. (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ CharPlyMat = (𝑛 ∈ Fin, 𝑟 ∈ V ↦ (𝑚 ∈ (Base‘(𝑛 Mat 𝑟)) ↦ ((𝑛 maDet (Poly1‘𝑟))‘(((var1‘𝑟)( ·𝑠 ‘(𝑛 Mat (Poly1‘𝑟)))(1r‘(𝑛 Mat (Poly1‘𝑟))))(-g‘(𝑛 Mat (Poly1‘𝑟)))((𝑛 matToPolyMat 𝑟)‘𝑚))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmatcl 20452 | Closure of the characteristic matrix of a matrix. (Contributed by AV, 25-Oct-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ − = (-g‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝐻 = ((𝑋 · 1 ) − (𝑇‘𝑀)) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → 𝐻 ∈ (Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmatval 20453 | The entries of the characteristic matrix of a matrix. (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 10-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ − = (-g‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝐻 = ((𝑋 · 1 ) − (𝑇‘𝑀)) & ⊢ ∼ = (-g‘𝑃) & ⊢ 0 = (0g‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝐼 ∈ 𝑁 ∧ 𝐽 ∈ 𝑁)) → (𝐼𝐻𝐽) = if(𝐼 = 𝐽, (𝑋 ∼ (𝐼(𝑇‘𝑀)𝐽)), ( 0 ∼ (𝐼(𝑇‘𝑀)𝐽)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatfval 20454* | Value of the characteristic polynomial function. (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝐷 = (𝑁 maDet 𝑃) & ⊢ − = (-g‘𝑌) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉) → 𝐶 = (𝑚 ∈ 𝐵 ↦ (𝐷‘((𝑋 · 1 ) − (𝑇‘𝑚))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatval 20455 | The characteristic polynomial of a (square) matrix (expressed with a determinant). (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝐷 = (𝑁 maDet 𝑃) & ⊢ − = (-g‘𝑌) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ 𝑉 ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝐷‘((𝑋 · 1 ) − (𝑇‘𝑀)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatply1 20456 | The characteristic polynomial of a (square) matrix over a commutative ring is a polynomial, see also the following remark in [Lang], p. 561: "[the characteristic polynomial] is an element of k[t]". (Contributed by AV, 2-Aug-2019.) (Proof shortened by AV, 29-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) ∈ 𝐸) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmatval2 20457* | The characteristic polynomial of a (square) matrix (expressed with the Leibnitz formula for the determinant). (Contributed by AV, 2-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ − = (-g‘𝑌) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝐺 = (SymGrp‘𝑁) & ⊢ 𝐻 = (Base‘𝐺) & ⊢ 𝑍 = (ℤRHom‘𝑃) & ⊢ 𝑆 = (pmSgn‘𝑁) & ⊢ 𝑈 = (mulGrp‘𝑃) & ⊢ × = (.r‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝑃 Σg (𝑝 ∈ 𝐻 ↦ (((𝑍 ∘ 𝑆)‘𝑝) × (𝑈 Σg (𝑥 ∈ 𝑁 ↦ ((𝑝‘𝑥)((𝑋 · 1 ) − (𝑇‘𝑀))𝑥))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat0d 20458 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (∅ CharPlyMat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐶‘∅) = (1r‘(Poly1‘𝑅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 20459 | Lemma for chpmat1d 20460. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼((𝑋( ·𝑠 ‘𝐺)(1r‘𝐺))(-g‘𝐺)(𝑇‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 20460 | The characteristic polynomial of a matrix with dimension 1. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) ⇒ ⊢ ((𝑅 ∈ CRing ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐶‘𝑀) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem0 20461 | Lemma 0 for chpdmat 20465. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝑄 = (𝑁 Mat 𝑃) & ⊢ 1 = (1r‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑄) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → (𝑋 · 1 ) ∈ (Base‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem1 20462 | Lemma 1 for chpdmat 20465. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝑄 = (𝑁 Mat 𝑃) & ⊢ 1 = (1r‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑄) & ⊢ 𝑍 = (-g‘𝑄) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) → ((𝑋 · 1 )𝑍(𝑇‘𝑀)) ∈ (Base‘𝑄)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem2 20463 | Lemma 2 for chpdmat 20465. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝑄 = (𝑁 Mat 𝑃) & ⊢ 1 = (1r‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑄) & ⊢ 𝑍 = (-g‘𝑄) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((((((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝑖 ∈ 𝑁) ∧ 𝑗 ∈ 𝑁) ∧ 𝑖 ≠ 𝑗) ∧ (𝑖𝑀𝑗) = 0 ) → (𝑖((𝑋 · 1 )𝑍(𝑇‘𝑀))𝑗) = (0g‘𝑃)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmatlem3 20464 | Lemma 3 for chpdmat 20465. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝑄 = (𝑁 Mat 𝑃) & ⊢ 1 = (1r‘𝑄) & ⊢ · = ( ·𝑠 ‘𝑄) & ⊢ 𝑍 = (-g‘𝑄) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ 𝐾 ∈ 𝑁) → (𝐾((𝑋 · 1 )𝑍(𝑇‘𝑀))𝐾) = (𝑋 − (𝑆‘(𝐾𝑀𝐾)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpdmat 20465* | The characteristic polynomial of a diagonal matrix. (Contributed by AV, 18-Aug-2019.) (Proof shortened by AV, 21-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 0 = (0g‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ ∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖 ≠ 𝑗 → (𝑖𝑀𝑗) = 0 )) → (𝐶‘𝑀) = (𝐺 Σg (𝑘 ∈ 𝑁 ↦ (𝑋 − (𝑆‘(𝑘𝑀𝑘)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmat 20466* | The characteristic polynomial of a (nonempty!) scalar matrix. (Contributed by AV, 21-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = 𝐸)) → (𝐶‘𝑀) = ((#‘𝑁) ↑ (𝑋 − (𝑆‘𝐸)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmat0 20467* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed with its diagonal element. (Contributed by AV, 21-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ − = (-g‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐼 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐼𝑀𝐼))) → (𝐶‘𝑀) = ((#‘𝑁) ↑ (𝑋 − (𝑆‘(𝐼𝑀𝐼))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmatgsumbin 20468* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of binomials. (Contributed by AV, 2-Sep-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐹 = (.g‘𝑃) & ⊢ 𝐻 = (mulGrp‘𝑅) & ⊢ 𝐸 = (.g‘𝐻) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈ (0...(#‘𝑁)) ↦ (((#‘𝑁)C𝑙)𝐹((((#‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽))) · (𝑙 ↑ 𝑋)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpscmatgsummon 20469* | The characteristic polynomial of a (nonempty!) scalar matrix, expressed as finite group sum of scaled monomials. (Contributed by AV, 2-Sep-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐷 = {𝑚 ∈ (Base‘𝐴) ∣ ∃𝑐 ∈ (Base‘𝑅)∀𝑖 ∈ 𝑁 ∀𝑗 ∈ 𝑁 (𝑖𝑚𝑗) = if(𝑖 = 𝑗, 𝑐, (0g‘𝑅))} & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ − = (-g‘𝑃) & ⊢ 𝐹 = (.g‘𝑃) & ⊢ 𝐻 = (mulGrp‘𝑅) & ⊢ 𝐸 = (.g‘𝐻) & ⊢ 𝐼 = (invg‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑃) & ⊢ 𝑍 = (.g‘𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) ∧ (𝑀 ∈ 𝐷 ∧ 𝐽 ∈ 𝑁 ∧ ∀𝑛 ∈ 𝑁 (𝑛𝑀𝑛) = (𝐽𝑀𝐽))) → (𝐶‘𝑀) = (𝑃 Σg (𝑙 ∈ (0...(#‘𝑁)) ↦ ((((#‘𝑁)C𝑙)𝑍(((#‘𝑁) − 𝑙)𝐸(𝐼‘(𝐽𝑀𝐽)))) · (𝑙 ↑ 𝑋))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chp0mat 20470 | The characteristic polynomial of the zero matrix. (Contributed by AV, 18-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 0 = (0g‘𝐴) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘ 0 ) = ((#‘𝑁) ↑ 𝑋)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpidmat 20471 | The characteristic polynomial of the identity matrix. (Contributed by AV, 19-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ 𝐺 = (mulGrp‘𝑃) & ⊢ ↑ = (.g‘𝐺) & ⊢ 𝐼 = (1r‘𝐴) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 1 = (1r‘𝑅) & ⊢ − = (-g‘𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing) → (𝐶‘𝐼) = ((#‘𝑁) ↑ (𝑋 − (𝑆‘ 1 )))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chmaidscmat 20472 | The characteristic polynomial of a matrix multiplied with the identity matrix is a scalar matrix. (Contributed by AV, 30-Oct-2019.) (Revised by AV, 19-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝐾 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 0 = (0g‘𝑃) & ⊢ 1 = (1r‘𝑌) & ⊢ 𝑆 = (𝑁 ScMat 𝑃) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) → ((𝐶‘𝑀) · 1 ) ∈ 𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
In this subsection the function 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) is discussed. This function is involved in the representation of the product of the characteristic matrix of a given matrix and its adjunct as an infinite sum, see cpmadugsum 20502. Therefore, this function is called "characteristic factor function" (in short "chfacf") in the following. It plays an important role in the proof of the Cayley-Hamilton theorem, see cayhamlem1 20490, cayhamlem3 20511 and cayhamlem4 20512. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 20473* | The function values of a mapping from the nonnegative integers with four distinct cases. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ ((𝜑 ∧ 𝑁 = 0) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐴) & ⊢ ((𝜑 ∧ 0 < 𝑁 ∧ 𝑁 < 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐵) & ⊢ ((𝜑 ∧ 𝑁 = 𝑆) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐶) & ⊢ ((𝜑 ∧ 𝑆 < 𝑁) → 𝑌 = ⦋𝑁 / 𝑛⦌𝐷) ⇒ ⊢ (𝜑 → (𝐺‘𝑁) = 𝑌) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifa 20474* | The function value of a mapping from the nonnegative integers with four distinct cases for the first case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝑁 = 0 ∧ ⦋𝑁 / 𝑛⦌𝐴 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐴) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifb 20475* | The function value of a mapping from the nonnegative integers with four distinct cases for the second case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ (0 < 𝑁 ∧ 𝑁 < 𝑆) ∧ ⦋𝑁 / 𝑛⦌𝐵 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐵) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifc 20476* | The function value of a mapping from the nonnegative integers with four distinct cases for the third case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝑁 = 𝑆 ∧ ⦋𝑁 / 𝑛⦌𝐶 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐶) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04ifd 20477* | The function value of a mapping from the nonnegative integers with four distinct cases for the forth case. (Contributed by AV, 10-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 𝐴, if(𝑛 = 𝑆, 𝐶, if(𝑆 < 𝑛, 𝐷, 𝐵)))) & ⊢ (𝜑 → 𝑆 ∈ ℕ) & ⊢ (𝜑 → 𝑁 ∈ ℕ0) ⇒ ⊢ ((𝜑 ∧ 𝑆 < 𝑁 ∧ ⦋𝑁 / 𝑛⦌𝐷 ∈ 𝑉) → (𝐺‘𝑁) = ⦋𝑁 / 𝑛⦌𝐷) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfisf 20478* | The "characteristic factor function" is a function from the nonnegative integers to polynomial matrices. (Contributed by AV, 8-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfisfcpmat 20479* | The "characteristic factor function" is a function from the nonnegative integers to constant polynomial matrices. (Contributed by AV, 19-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑆 = (𝑁 ConstPolyMat 𝑅) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺:ℕ0⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacffsupp 20480* | The "characteristic factor function" is finitely supported. (Contributed by AV, 20-Nov-2019.) (Proof shortened by AV, 23-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulcl 20481* | Closure of a scaled value of the "characteristic factor function". (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) ∈ (Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmul0 20482* | A scaled value of the "characteristic factor function" is zero almost always. (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulfsupp 20483* | A mapping of scaled values of the "characteristic factor function" is finitely supported. (Contributed by AV, 8-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulgsum 20484* | Breaking up a sum of values of the "characteristic factor function" scaled by a polynomial. (Contributed by AV, 9-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ × = (.r‘𝑌) & ⊢ − = (-g‘𝑌) & ⊢ 0 = (0g‘𝑌) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝐺 = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, ( 0 − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))), if(𝑛 = (𝑠 + 1), (𝑇‘(𝑏‘𝑠)), if((𝑠 + 1) < 𝑛, 0 , ((𝑇‘(𝑏‘(𝑛 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑛)))))))) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ + = (+g‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulcl 20485* | Closure of the value 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‘𝑌)) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ (𝑇‘𝑀)) × (𝐺‘𝐾)) ∈ (Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmul0 20486* | The value of the "characteristic factor function" multiplied with a constant polynomial matrix is zero almost always. (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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ (𝑇‘𝑀)) × (𝐺‘𝐾)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulfsupp 20487* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum 20488* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ (𝑇‘𝑀)) × ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulgsum2 20489* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ (𝑇‘𝑀)) × (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ (((𝑖 ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘(𝑖 − 1)))) − (((𝑖 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑖)))))) + ((((𝑠 + 1) ↑ (𝑇‘𝑀)) × (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cayhamlem1 20490* | Lemma 1 for cayleyhamilton 20514. (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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (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 20491 | The right-hand fundamental relation of the adjugate (see madurid 20269) 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 20492* | 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 20493* | 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 20494* | Lemma 1 for cpmidpmat 20497. (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 20495* | Lemma 2 for cpmidpmat 20497. (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 ∧ 𝑀 ∈ 𝐵) → 𝐺 ∈ (𝐵 ↑𝑚 ℕ0)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmidpmatlem3 20496* | Lemma 3 for cpmidpmat 20497. (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 20497* | 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 20498* | Lemma B for cpmadugsum 20502. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ (((𝑖 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemC 20499* | Lemma C for cpmadugsum 20502. (Contributed by AV, 2-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ0 ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) = (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | cpmadugsumlemF 20500* | Lemma F for cpmadugsum 20502. (Contributed by AV, 7-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ ↑ = (.g‘(mulGrp‘𝑃)) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ × = (.r‘𝑌) & ⊢ 1 = (1r‘𝑌) & ⊢ + = (+g‘𝑌) & ⊢ − = (-g‘𝑌) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑𝑚 (0...𝑠)))) → (((𝑋 · 1 ) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖)))))) − ((𝑇‘𝑀) × (𝑌 Σg (𝑖 ∈ (0...𝑠) ↦ ((𝑖 ↑ 𝑋) · (𝑇‘(𝑏‘𝑖))))))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |