Metamath Proof Explorer

Theorem cpmidgsum2

Description: Representation of the identity matrix multiplied with the characteristic polynomial of a matrix as another group sum. (Contributed by AV, 10-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a ⊢ A = N Mat R
cpmadugsum.b ⊢ B = Base A
cpmadugsum.p ⊢ P = Poly 1 ⁡ R
cpmadugsum.y ⊢ Y = N Mat P
cpmadugsum.t ⊢ T = N matToPolyMat R
cpmadugsum.x ⊢ X = var 1 ⁡ R
cpmadugsum.e ⊢ × ˙ = ⋅ mulGrp P
cpmadugsum.m ⊢ · ˙ = ⋅ Y
cpmadugsum.r ⊢ × ˙ = ⋅ Y
cpmadugsum.1 ⊢ 1 ˙ = 1 Y
cpmadugsum.g ⊢ + ˙ = + Y
cpmadugsum.s ⊢ - ˙ = - Y
cpmadugsum.i ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M
cpmadugsum.j ⊢ J = N maAdju P
cpmadugsum.0 ⊢ 0 ˙ = 0 Y
cpmadugsum.g2 ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if n = s + 1 T ⁡ b ⁡ s if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n
cpmidgsum2.c ⊢ C = N CharPlyMat R
cpmidgsum2.k ⊢ K = C ⁡ M
cpmidgsum2.h ⊢ H = K · ˙ 1 ˙
Assertion cpmidgsum2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i

Proof

Step Hyp Ref Expression
1 cpmadugsum.a ⊢ A = N Mat R
2 cpmadugsum.b ⊢ B = Base A
3 cpmadugsum.p ⊢ P = Poly 1 ⁡ R
4 cpmadugsum.y ⊢ Y = N Mat P
5 cpmadugsum.t ⊢ T = N matToPolyMat R
6 cpmadugsum.x ⊢ X = var 1 ⁡ R
7 cpmadugsum.e ⊢ × ˙ = ⋅ mulGrp P
8 cpmadugsum.m ⊢ · ˙ = ⋅ Y
9 cpmadugsum.r ⊢ × ˙ = ⋅ Y
10 cpmadugsum.1 ⊢ 1 ˙ = 1 Y
11 cpmadugsum.g ⊢ + ˙ = + Y
12 cpmadugsum.s ⊢ - ˙ = - Y
13 cpmadugsum.i ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M
14 cpmadugsum.j ⊢ J = N maAdju P
15 cpmadugsum.0 ⊢ 0 ˙ = 0 Y
16 cpmadugsum.g2 ⊢ G = n ∈ ℕ 0 ⟼ if n = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if n = s + 1 T ⁡ b ⁡ s if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n
17 cpmidgsum2.c ⊢ C = N CharPlyMat R
18 cpmidgsum2.k ⊢ K = C ⁡ M
19 cpmidgsum2.h ⊢ H = K · ˙ 1 ˙
20 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 cpmadugsum ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
21 crngring ⊢ R ∈ CRing → R ∈ Ring
22 21 anim2i ⊢ N ∈ Fin ∧ R ∈ CRing → N ∈ Fin ∧ R ∈ Ring
23 22 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ Ring
24 3 4 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → Y ∈ Ring
25 ringgrp ⊢ Y ∈ Ring → Y ∈ Grp
26 23 24 25 3syl ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → Y ∈ Grp
27 3 4 pmatlmod ⊢ N ∈ Fin ∧ R ∈ Ring → Y ∈ LMod
28 21 27 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → Y ∈ LMod
29 21 adantl ⊢ N ∈ Fin ∧ R ∈ CRing → R ∈ Ring
30 eqid ⊢ Base P = Base P
31 6 3 30 vr1cl ⊢ R ∈ Ring → X ∈ Base P
32 29 31 syl ⊢ N ∈ Fin ∧ R ∈ CRing → X ∈ Base P
33 3 ply1crng ⊢ R ∈ CRing → P ∈ CRing
34 4 matsca2 ⊢ N ∈ Fin ∧ P ∈ CRing → P = Scalar ⁡ Y
35 33 34 sylan2 ⊢ N ∈ Fin ∧ R ∈ CRing → P = Scalar ⁡ Y
36 35 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing → Base P = Base Scalar ⁡ Y
37 32 36 eleqtrd ⊢ N ∈ Fin ∧ R ∈ CRing → X ∈ Base Scalar ⁡ Y
38 eqid ⊢ Base Y = Base Y
39 38 10 ringidcl ⊢ Y ∈ Ring → 1 ˙ ∈ Base Y
40 22 24 39 3syl ⊢ N ∈ Fin ∧ R ∈ CRing → 1 ˙ ∈ Base Y
41 eqid ⊢ Scalar ⁡ Y = Scalar ⁡ Y
42 eqid ⊢ Base Scalar ⁡ Y = Base Scalar ⁡ Y
43 38 41 8 42 lmodvscl ⊢ Y ∈ LMod ∧ X ∈ Base Scalar ⁡ Y ∧ 1 ˙ ∈ Base Y → X · ˙ 1 ˙ ∈ Base Y
44 28 37 40 43 syl3anc ⊢ N ∈ Fin ∧ R ∈ CRing → X · ˙ 1 ˙ ∈ Base Y
45 44 3adant3 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → X · ˙ 1 ˙ ∈ Base Y
46 5 1 2 3 4 mat2pmatbas ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B → T ⁡ M ∈ Base Y
47 21 46 syl3an2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → T ⁡ M ∈ Base Y
48 38 12 grpsubcl ⊢ Y ∈ Grp ∧ X · ˙ 1 ˙ ∈ Base Y ∧ T ⁡ M ∈ Base Y → X · ˙ 1 ˙ - ˙ T ⁡ M ∈ Base Y
49 26 45 47 48 syl3anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → X · ˙ 1 ˙ - ˙ T ⁡ M ∈ Base Y
50 33 3ad2ant2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → P ∈ CRing
51 eqid ⊢ N maDet P = N maDet P
52 4 38 14 51 10 9 8 madurid ⊢ X · ˙ 1 ˙ - ˙ T ⁡ M ∈ Base Y ∧ P ∈ CRing → X · ˙ 1 ˙ - ˙ T ⁡ M × ˙ J ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M · ˙ 1 ˙
53 49 50 52 syl2anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → X · ˙ 1 ˙ - ˙ T ⁡ M × ˙ J ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M · ˙ 1 ˙
54 id ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M → I = X · ˙ 1 ˙ - ˙ T ⁡ M
55 fveq2 ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M → J ⁡ I = J ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M
56 54 55 oveq12d ⊢ I = X · ˙ 1 ˙ - ˙ T ⁡ M → I × ˙ J ⁡ I = X · ˙ 1 ˙ - ˙ T ⁡ M × ˙ J ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M
57 13 56 mp1i ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I × ˙ J ⁡ I = X · ˙ 1 ˙ - ˙ T ⁡ M × ˙ J ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M
58 17 1 2 3 4 51 12 6 8 5 10 chpmatval ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → C ⁡ M = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M
59 18 58 syl5eq ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → K = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M
60 59 oveq1d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → K · ˙ 1 ˙ = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M · ˙ 1 ˙
61 19 60 syl5eq ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → H = N maDet P ⁡ X · ˙ 1 ˙ - ˙ T ⁡ M · ˙ 1 ˙
62 53 57 61 3eqtr4rd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → H = I × ˙ J ⁡ I
63 62 adantr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → H = I × ˙ J ⁡ I
64 simpr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
65 63 64 eqtrd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
66 65 ex ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
67 66 reximdv ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → ∃ b ∈ B 0 … s H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
68 67 reximdv ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I × ˙ J ⁡ I = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i → ∃ s ∈ ℕ ∃ b ∈ B 0 … s H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i
69 20 68 mpd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s H = ∑ Y i ∈ ℕ 0 i × ˙ X · ˙ G ⁡ i