![]() |
Metamath
Proof Explorer Theorem List (p. 229 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
Statement | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | mp2pm2mplem3 22801* | Lemma 3 for mp2pm2mp 22804. (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 22802* | Lemma 4 for mp2pm2mp 22804. (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 22803* | Lemma 5 for mp2pm2mp 22804. (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 22804* | 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 22805* | Lemma 2 for pm2mpghm 22809. (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 22806 | 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 22807 | 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 22808 | 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 22809 | 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 22810 | 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 22811* | Lemma 1 for pm2mpmhm 22813. (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 22812* | Lemma 2 for pm2mpmhm 22813. (Contributed by AV, 22-Oct-2019.) (Revised by AV, 6-Dec-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐶 = (𝑁 Mat 𝑃) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝑄 = (Poly1‘𝐴) & ⊢ 𝑇 = (𝑁 pMatToMatPoly 𝑅) & ⊢ 𝐵 = (Base‘𝐶) ⇒ ⊢ ((𝑁 ∈ Fin ∧ 𝑅 ∈ Ring) → ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑇‘(𝑥(.r‘𝐶)𝑦)) = ((𝑇‘𝑥)(.r‘𝑄)(𝑇‘𝑦))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | pm2mpmhm 22813 | 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 22814 | 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 22815 | 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 22816 | 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 22817 | 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 22818* | 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) ∧ (𝑀 ∈ (𝐾 ↑m ℕ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 22820) the eigenvalues and corresponding eigenvectors can be defined. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
The characteristic polynomial of a matrix 𝐴 is the determinant of the characteristic matrix of 𝐴: (𝑡𝐼 − 𝐴). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | cchpmat 22819 | Extend class notation with the characteristic polynomial. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class CharPlyMat | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-chpmat 22820* | 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 22821 | 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 22822 | 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 22823* | 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 22824 | 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 22825 | 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 22826* | 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 22827 | The characteristic polynomial of the empty matrix. (Contributed by AV, 6-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (∅ CharPlyMat 𝑅) ⇒ ⊢ (𝑅 ∈ Ring → (𝐶‘∅) = (1r‘(Poly1‘𝑅))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1dlem 22828 | Lemma for chpmat1d 22829. (Contributed by AV, 7-Aug-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝑋 = (var1‘𝑅) & ⊢ − = (-g‘𝑃) & ⊢ 𝑆 = (algSc‘𝑃) & ⊢ 𝐺 = (𝑁 Mat 𝑃) & ⊢ 𝑇 = (𝑁 matToPolyMat 𝑅) ⇒ ⊢ ((𝑅 ∈ Ring ∧ (𝑁 = {𝐼} ∧ 𝐼 ∈ 𝑉) ∧ 𝑀 ∈ 𝐵) → (𝐼((𝑋( ·𝑠 ‘𝐺)(1r‘𝐺))(-g‘𝐺)(𝑇‘𝑀))𝐼) = (𝑋 − (𝑆‘(𝐼𝑀𝐼)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chpmat1d 22829 | 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 22830 | Lemma 0 for chpdmat 22834. (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 22831 | Lemma 1 for chpdmat 22834. (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 22832 | Lemma 2 for chpdmat 22834. (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 22833 | Lemma 3 for chpdmat 22834. (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 22834* | 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 22835* | 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 22836* | 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 22837* | 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 22838* | 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 22839 | 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 22840 | 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 22841 | The characteristic polynomial of a matrix multiplied with the identity matrix is a scalar matrix. (Contributed by AV, 30-Oct-2019.) (Revised by AV, 5-Jul-2022.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 𝐶 = (𝑁 CharPlyMat 𝑅) & ⊢ 𝑃 = (Poly1‘𝑅) & ⊢ 𝐸 = (Base‘𝑃) & ⊢ 𝑌 = (𝑁 Mat 𝑃) & ⊢ 𝐾 = (Base‘𝑌) & ⊢ · = ( ·𝑠 ‘𝑌) & ⊢ 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 22871. 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 22859, cayhamlem3 22880 and cayhamlem4 22881. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fvmptnn04if 22842* | 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 22843* | 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 22844* | 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 22845* | 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 22846* | 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 22847* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶(Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfisfcpmat 22848* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺:ℕ0⟶𝑆) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacffsupp 22849* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → 𝐺 finSupp (0g‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulcl 22850* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) ∈ (Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmul0 22851* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ 𝑋) · (𝐺‘𝐾)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulfsupp 22852* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖))) finSupp 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfscmulgsum 22853* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠)))) → (𝑌 Σg (𝑖 ∈ ℕ0 ↦ ((𝑖 ↑ 𝑋) · (𝐺‘𝑖)))) = ((𝑌 Σg (𝑖 ∈ (1...𝑠) ↦ ((𝑖 ↑ 𝑋) · ((𝑇‘(𝑏‘(𝑖 − 1))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘𝑖))))))) + ((((𝑠 + 1) ↑ 𝑋) · (𝑇‘(𝑏‘𝑠))) − ((𝑇‘𝑀) × (𝑇‘(𝑏‘0)))))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulcl 22854* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ ℕ0) → ((𝐾 ↑ (𝑇‘𝑀)) × (𝐺‘𝐾)) ∈ (Base‘𝑌)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmul0 22855* | 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 ∧ 𝑀 ∈ 𝐵) ∧ (𝑠 ∈ ℕ ∧ 𝑏 ∈ (𝐵 ↑m (0...𝑠))) ∧ 𝐾 ∈ (ℤ≥‘(𝑠 + 2))) → ((𝐾 ↑ (𝑇‘𝑀)) × (𝐺‘𝐾)) = 0 ) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chfacfpmmulfsupp 22856* | 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 22857* | 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 22858* | 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 22859* | Lemma 1 for cayleyhamilton 22883. (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 22860 | The right-hand fundamental relation of the adjugate (see madurid 22637) 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 22861* | 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 22862* | 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 22863* | Lemma 1 for cpmidpmat 22866. (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 22864* | Lemma 2 for cpmidpmat 22866. (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 22865* | Lemma 3 for cpmidpmat 22866. (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 22866* | 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 22867* | Lemma B for cpmadugsum 22871. (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 22868* | Lemma C for cpmadugsum 22871. (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 22869* | Lemma F for cpmadugsum 22871. (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 22870* | 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 22871* | 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 22872* | 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 22873* | 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 22874* | Lemma 1 for cpmadumatpoly 22876. (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 22875* | Lemma 2 for cpmadumatpoly 22876. (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 22876* | 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 22877 | Lemma for cayhamlem3 22880. (Contributed by AV, 24-Nov-2019.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝐾 = (Base‘𝑅) & ⊢ 𝐴 = (𝑁 Mat 𝑅) & ⊢ 𝐵 = (Base‘𝐴) & ⊢ 1 = (1r‘𝐴) & ⊢ ∗ = ( ·𝑠 ‘𝐴) & ⊢ ↑ = (.g‘(mulGrp‘𝐴)) & ⊢ · = (.r‘𝐴) ⇒ ⊢ (((𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵) ∧ (𝐻 ∈ (𝐾 ↑m ℕ0) ∧ 𝐿 ∈ ℕ0)) → ((𝐻‘𝐿) ∗ (𝐿 ↑ 𝑀)) = ((𝐿 ↑ 𝑀) · ((𝐻‘𝐿) ∗ 1 ))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | chcoeffeqlem 22878* | Lemma for chcoeffeq 22879. (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 22879* | 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 22880* | Lemma for cayhamlem4 22881. (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 22881* | Lemma for cayleyhamilton 22883. (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 22882* | The Cayley-Hamilton theorem: A matrix over a commutative ring "satisfies its own characteristic equation". This version of cayleyhamilton 22883 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 22884)! (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 22883* | 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 22884* | Alternate proof of cayleyhamilton 22883, the Cayley-Hamilton theorem. This proof does not use cayleyhamilton0 22882 directly, but has the same structure as the proof of cayleyhamilton0 22882. In contrast to the proof of cayleyhamilton0 22882, 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 22885* | 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 22883, 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 22907), 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 22887), then the function which associates with a set the set of topologies on it (df-topon 22904), and finally the class of topological spaces, as extensible structures having an underlying set and a topology on it (df-topsp 22926). Of course, a topology is the same thing as a topology on a set (see toprntopon 22918). | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Syntax | ctop 22886 | Syntax for the class of topologies. | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
class Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Definition | df-top 22887* |
Define the class of topologies. It is a proper class (see topnex 22990).
See istopg 22888 and istop2g 22889 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 22888* |
Express the predicate "𝐽 is a topology". See istop2g 22889 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 22889* | Express the predicate "𝐽 is a topology" using nonempty finite intersections instead of binary intersections as in istopg 22888. (Contributed by NM, 19-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ 𝐴 → (𝐽 ∈ Top ↔ (∀𝑥(𝑥 ⊆ 𝐽 → ∪ 𝑥 ∈ 𝐽) ∧ ∀𝑥((𝑥 ⊆ 𝐽 ∧ 𝑥 ≠ ∅ ∧ 𝑥 ∈ Fin) → ∩ 𝑥 ∈ 𝐽)))) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | uniopn 22890 | 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 22891* | The indexed union of a subset of a topology is an open set. (Contributed by NM, 5-Oct-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) → ∪ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | inopn 22892 | The intersection of two open sets of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∩ 𝐵) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fitop 22893 | A topology is closed under finite intersections. (Contributed by Jeff Hankins, 7-Oct-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → (fi‘𝐽) = 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | fiinopn 22894 | The intersection of a nonempty finite family of open sets is open. (Contributed by FL, 20-Apr-2012.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → ((𝐴 ⊆ 𝐽 ∧ 𝐴 ≠ ∅ ∧ 𝐴 ∈ Fin) → ∩ 𝐴 ∈ 𝐽)) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | iinopn 22895* | The intersection of a nonempty finite family of open sets is open. (Contributed by Mario Carneiro, 14-Sep-2014.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ (𝐴 ∈ Fin ∧ 𝐴 ≠ ∅ ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ 𝐽)) → ∩ 𝑥 ∈ 𝐴 𝐵 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | unopn 22896 | The union of two open sets is open. (Contributed by Jeff Madsen, 2-Sep-2009.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽 ∧ 𝐵 ∈ 𝐽) → (𝐴 ∪ 𝐵) ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0opn 22897 | The empty set is an open subset of any topology. (Contributed by Stefan Allan, 27-Feb-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ (𝐽 ∈ Top → ∅ ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | 0ntop 22898 | The empty set is not a topology. (Contributed by FL, 1-Jun-2008.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ ¬ ∅ ∈ Top | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | topopn 22899 | The underlying set of a topology is an open set. (Contributed by NM, 17-Jul-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ (𝐽 ∈ Top → 𝑋 ∈ 𝐽) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
Theorem | eltopss 22900 | A member of a topology is a subset of its underlying set. (Contributed by NM, 12-Sep-2006.) | ||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||||
⊢ 𝑋 = ∪ 𝐽 ⇒ ⊢ ((𝐽 ∈ Top ∧ 𝐴 ∈ 𝐽) → 𝐴 ⊆ 𝑋) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |