Metamath Proof Explorer

Theorem cpmidpmat

Description: 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)

Ref Expression
Hypotheses cpmidgsum.a ⊢ A = N Mat R
cpmidgsum.b ⊢ B = Base A
cpmidgsum.p ⊢ P = Poly 1 ⁡ R
cpmidgsum.y ⊢ Y = N Mat P
cpmidgsum.x ⊢ X = var 1 ⁡ R
cpmidgsum.e ⊢ × ˙ = ⋅ mulGrp P
cpmidgsum.m ⊢ · ˙ = ⋅ Y
cpmidgsum.1 ⊢ 1 ˙ = 1 Y
cpmidgsum.u ⊢ U = algSc ⁡ P
cpmidgsum.c ⊢ C = N CharPlyMat R
cpmidgsum.k ⊢ K = C ⁡ M
cpmidgsum.h ⊢ H = K · ˙ 1 ˙
cpmidgsumm2pm.o ⊢ O = 1 A
cpmidgsumm2pm.m ⊢ ∗ ˙ = ⋅ A
cpmidgsumm2pm.t ⊢ T = N matToPolyMat R
cpmidgsum.w ⊢ W = Base Y
cpmidpmat.p ⊢ Q = Poly 1 ⁡ A
cpmidpmat.z ⊢ Z = var 1 ⁡ A
cpmidpmat.m ⊢ ∙ ˙ = ⋅ Q
cpmidpmat.e ⊢ E = ⋅ mulGrp Q
cpmidpmat.i ⊢ I = N pMatToMatPoly R
Assertion cpmidpmat ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ H = ∑ Q n ∈ ℕ 0 coe 1 ⁡ K ⁡ n ∗ ˙ O ∙ ˙ n E Z

Proof

Step Hyp Ref Expression
1 cpmidgsum.a ⊢ A = N Mat R
2 cpmidgsum.b ⊢ B = Base A
3 cpmidgsum.p ⊢ P = Poly 1 ⁡ R
4 cpmidgsum.y ⊢ Y = N Mat P
5 cpmidgsum.x ⊢ X = var 1 ⁡ R
6 cpmidgsum.e ⊢ × ˙ = ⋅ mulGrp P
7 cpmidgsum.m ⊢ · ˙ = ⋅ Y
8 cpmidgsum.1 ⊢ 1 ˙ = 1 Y
9 cpmidgsum.u ⊢ U = algSc ⁡ P
10 cpmidgsum.c ⊢ C = N CharPlyMat R
11 cpmidgsum.k ⊢ K = C ⁡ M
12 cpmidgsum.h ⊢ H = K · ˙ 1 ˙
13 cpmidgsumm2pm.o ⊢ O = 1 A
14 cpmidgsumm2pm.m ⊢ ∗ ˙ = ⋅ A
15 cpmidgsumm2pm.t ⊢ T = N matToPolyMat R
16 cpmidgsum.w ⊢ W = Base Y
17 cpmidpmat.p ⊢ Q = Poly 1 ⁡ A
18 cpmidpmat.z ⊢ Z = var 1 ⁡ A
19 cpmidpmat.m ⊢ ∙ ˙ = ⋅ Q
20 cpmidpmat.e ⊢ E = ⋅ mulGrp Q
21 cpmidpmat.i ⊢ I = N pMatToMatPoly R
22 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 cpmidgsumm2pm ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → H = ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O
23 22 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ H = I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O
24 eqid ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O = k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O
25 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem1 ⊢ n ∈ ℕ 0 → k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = coe 1 ⁡ K ⁡ n ∗ ˙ O
26 25 eqcomd ⊢ n ∈ ℕ 0 → coe 1 ⁡ K ⁡ n ∗ ˙ O = k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
27 26 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ n ∈ ℕ 0 → coe 1 ⁡ K ⁡ n ∗ ˙ O = k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
28 27 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ n ∈ ℕ 0 → T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
29 28 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ n ∈ ℕ 0 → n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
30 29 mpteq2dva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → n ∈ ℕ 0 ⟼ n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = n ∈ ℕ 0 ⟼ n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
31 30 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
32 31 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n
33 3simpa ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ CRing
34 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ∈ B ℕ 0
35 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 24 cpmidpmatlem3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → finSupp 0 A⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O
36 fveq2 ⊢ k = x → coe 1 ⁡ K ⁡ k = coe 1 ⁡ K ⁡ x
37 36 oveq1d ⊢ k = x → coe 1 ⁡ K ⁡ k ∗ ˙ O = coe 1 ⁡ K ⁡ x ∗ ˙ O
38 37 cbvmptv ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O = x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O
39 38 eleq1i ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ∈ B ℕ 0 ↔ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ∈ B ℕ 0
40 38 breq1i ⊢ finSupp 0 A⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ↔ finSupp 0 A⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O
41 39 40 anbi12i ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ∈ B ℕ 0 ∧ finSupp 0 A⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ↔ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ∈ B ℕ 0 ∧ finSupp 0 A⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O
42 3 4 16 19 20 18 1 2 17 21 6 5 7 15 pm2mp ⊢ N ∈ Fin ∧ R ∈ CRing ∧ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ∈ B ℕ 0 ∧ finSupp 0 A⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n = ∑ Q n ∈ ℕ 0 x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
43 41 42 sylan2b ⊢ N ∈ Fin ∧ R ∈ CRing ∧ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ∈ B ℕ 0 ∧ finSupp 0 A⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n = ∑ Q n ∈ ℕ 0 x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
44 33 34 35 43 syl12anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n = ∑ Q n ∈ ℕ 0 x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
45 38 fveq1i ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
46 45 fveq2i ⊢ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
47 46 oveq2i ⊢ n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
48 47 mpteq2i ⊢ n ∈ ℕ 0 ⟼ n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = n ∈ ℕ 0 ⟼ n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
49 48 oveq2i ⊢ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
50 49 fveq2i ⊢ I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n
51 45 oveq1i ⊢ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
52 51 mpteq2i ⊢ n ∈ ℕ 0 ⟼ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = n ∈ ℕ 0 ⟼ x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
53 52 oveq2i ⊢ ∑ Q n ∈ ℕ 0 k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = ∑ Q n ∈ ℕ 0 x ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ x ∗ ˙ O ⁡ n ∙ ˙ n E Z
54 44 50 53 3eqtr4g ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = ∑ Q n ∈ ℕ 0 k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z
55 32 54 eqtrd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ ∑ Y n ∈ ℕ 0 n × ˙ X · ˙ T ⁡ coe 1 ⁡ K ⁡ n ∗ ˙ O = ∑ Q n ∈ ℕ 0 k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z
56 25 adantl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ n ∈ ℕ 0 → k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n = coe 1 ⁡ K ⁡ n ∗ ˙ O
57 56 oveq1d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ n ∈ ℕ 0 → k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = coe 1 ⁡ K ⁡ n ∗ ˙ O ∙ ˙ n E Z
58 57 mpteq2dva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → n ∈ ℕ 0 ⟼ k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = n ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ n ∗ ˙ O ∙ ˙ n E Z
59 58 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∑ Q n ∈ ℕ 0 k ∈ ℕ 0 ⟼ coe 1 ⁡ K ⁡ k ∗ ˙ O ⁡ n ∙ ˙ n E Z = ∑ Q n ∈ ℕ 0 coe 1 ⁡ K ⁡ n ∗ ˙ O ∙ ˙ n E Z
60 23 55 59 3eqtrd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I ⁡ H = ∑ Q n ∈ ℕ 0 coe 1 ⁡ K ⁡ n ∗ ˙ O ∙ ˙ n E Z