Metamath Proof Explorer

Theorem cpmadumatpoly

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

Ref Expression
Hypotheses cpmadumatpoly.a ⊢ A = N Mat R
cpmadumatpoly.b ⊢ B = Base A
cpmadumatpoly.p ⊢ P = Poly 1 ⁡ R
cpmadumatpoly.y ⊢ Y = N Mat P
cpmadumatpoly.t ⊢ T = N matToPolyMat R
cpmadumatpoly.r ⊢ × ˙ = ⋅ Y
cpmadumatpoly.m0 ⊢ - ˙ = - Y
cpmadumatpoly.0 ⊢ 0 ˙ = 0 Y
cpmadumatpoly.g ⊢ 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
cpmadumatpoly.s ⊢ S = N ConstPolyMat R
cpmadumatpoly.m1 ⊢ · ˙ = ⋅ Y
cpmadumatpoly.1 ⊢ 1 ˙ = 1 Y
cpmadumatpoly.z ⊢ Z = var 1 ⁡ R
cpmadumatpoly.d ⊢ D = Z · ˙ 1 ˙ - ˙ T ⁡ M
cpmadumatpoly.j ⊢ J = N maAdju P
cpmadumatpoly.w ⊢ W = Base Y
cpmadumatpoly.q ⊢ Q = Poly 1 ⁡ A
cpmadumatpoly.x ⊢ X = var 1 ⁡ A
cpmadumatpoly.m2 ⊢ ∗ ˙ = ⋅ Q
cpmadumatpoly.e ⊢ × ˙ = ⋅ mulGrp Q
cpmadumatpoly.u ⊢ U = N cPolyMatToMat R
cpmadumatpoly.i ⊢ I = N pMatToMatPoly R
Assertion cpmadumatpoly ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X

Proof

Step Hyp Ref Expression
1 cpmadumatpoly.a ⊢ A = N Mat R
2 cpmadumatpoly.b ⊢ B = Base A
3 cpmadumatpoly.p ⊢ P = Poly 1 ⁡ R
4 cpmadumatpoly.y ⊢ Y = N Mat P
5 cpmadumatpoly.t ⊢ T = N matToPolyMat R
6 cpmadumatpoly.r ⊢ × ˙ = ⋅ Y
7 cpmadumatpoly.m0 ⊢ - ˙ = - Y
8 cpmadumatpoly.0 ⊢ 0 ˙ = 0 Y
9 cpmadumatpoly.g ⊢ 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
10 cpmadumatpoly.s ⊢ S = N ConstPolyMat R
11 cpmadumatpoly.m1 ⊢ · ˙ = ⋅ Y
12 cpmadumatpoly.1 ⊢ 1 ˙ = 1 Y
13 cpmadumatpoly.z ⊢ Z = var 1 ⁡ R
14 cpmadumatpoly.d ⊢ D = Z · ˙ 1 ˙ - ˙ T ⁡ M
15 cpmadumatpoly.j ⊢ J = N maAdju P
16 cpmadumatpoly.w ⊢ W = Base Y
17 cpmadumatpoly.q ⊢ Q = Poly 1 ⁡ A
18 cpmadumatpoly.x ⊢ X = var 1 ⁡ A
19 cpmadumatpoly.m2 ⊢ ∗ ˙ = ⋅ Q
20 cpmadumatpoly.e ⊢ × ˙ = ⋅ mulGrp Q
21 cpmadumatpoly.u ⊢ U = N cPolyMatToMat R
22 cpmadumatpoly.i ⊢ I = N pMatToMatPoly R
23 eqid ⊢ ⋅ mulGrp P = ⋅ mulGrp P
24 eqid ⊢ + Y = + Y
25 eqeq1 ⊢ n = z → n = 0 ↔ z = 0
26 eqeq1 ⊢ n = z → n = s + 1 ↔ z = s + 1
27 breq2 ⊢ n = z → s + 1 < n ↔ s + 1 < z
28 fvoveq1 ⊢ n = z → b ⁡ n − 1 = b ⁡ z − 1
29 28 fveq2d ⊢ n = z → T ⁡ b ⁡ n − 1 = T ⁡ b ⁡ z − 1
30 2fveq3 ⊢ n = z → T ⁡ b ⁡ n = T ⁡ b ⁡ z
31 30 oveq2d ⊢ n = z → T ⁡ M × ˙ T ⁡ b ⁡ n = T ⁡ M × ˙ T ⁡ b ⁡ z
32 29 31 oveq12d ⊢ n = z → T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n = T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
33 27 32 ifbieq2d ⊢ n = z → if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n = if s + 1 < z 0 ˙ T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
34 26 33 ifbieq2d ⊢ n = z → if n = s + 1 T ⁡ b ⁡ s if s + 1 < n 0 ˙ T ⁡ b ⁡ n − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ n = if z = s + 1 T ⁡ b ⁡ s if s + 1 < z 0 ˙ T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
35 25 34 ifbieq2d ⊢ n = z → 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 = if z = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if z = s + 1 T ⁡ b ⁡ s if s + 1 < z 0 ˙ T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
36 35 cbvmptv ⊢ 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 = z ∈ ℕ 0 ⟼ if z = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if z = s + 1 T ⁡ b ⁡ s if s + 1 < z 0 ˙ T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
37 9 36 eqtri ⊢ G = z ∈ ℕ 0 ⟼ if z = 0 0 ˙ - ˙ T ⁡ M × ˙ T ⁡ b ⁡ 0 if z = s + 1 T ⁡ b ⁡ s if s + 1 < z 0 ˙ T ⁡ b ⁡ z − 1 - ˙ T ⁡ M × ˙ T ⁡ b ⁡ z
38 1 2 3 4 5 13 23 11 6 12 24 7 14 15 8 37 cpmadugsum ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n
39 simp1 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin
40 39 ad3antrrr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → N ∈ Fin
41 crngring ⊢ R ∈ CRing → R ∈ Ring
42 41 3ad2ant2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → R ∈ Ring
43 42 ad3antrrr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → R ∈ Ring
44 1 2 3 4 6 7 8 5 9 10 chfacfisfcpmat ⊢ N ∈ Fin ∧ R ∈ Ring ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → G : ℕ 0 ⟶ S
45 41 44 syl3anl2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → G : ℕ 0 ⟶ S
46 45 anassrs ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → G : ℕ 0 ⟶ S
47 46 ffvelcdmda ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → G ⁡ n ∈ S
48 10 21 5 m2cpminvid2 ⊢ N ∈ Fin ∧ R ∈ Ring ∧ G ⁡ n ∈ S → T ⁡ U ⁡ G ⁡ n = G ⁡ n
49 40 43 47 48 syl3anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → T ⁡ U ⁡ G ⁡ n = G ⁡ n
50 49 eqcomd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → G ⁡ n = T ⁡ U ⁡ G ⁡ n
51 50 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → n ⋅ mulGrp P Z · ˙ G ⁡ n = n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n
52 51 mpteq2dva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → n ∈ ℕ 0 ⟼ n ⋅ mulGrp P Z · ˙ G ⁡ n = n ∈ ℕ 0 ⟼ n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n
53 52 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n
54 53 eqeq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n ↔ D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n
55 fveq2 ⊢ D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n → I ⁡ D × ˙ J ⁡ D = I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n
56 3simpa ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ CRing
57 56 ad2antrr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → N ∈ Fin ∧ R ∈ CRing
58 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 cpmadumatpolylem1 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → U ∘ G ∈ B ℕ 0
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 cpmadumatpolylem2 ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → finSupp 0 A⁡ U ∘ G
60 3 4 16 19 20 18 1 2 17 22 23 13 11 5 pm2mp ⊢ N ∈ Fin ∧ R ∈ CRing ∧ U ∘ G ∈ B ℕ 0 ∧ finSupp 0 A⁡ U ∘ G → I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n = ∑ Q n ∈ ℕ 0 U ∘ G ⁡ n ∗ ˙ n × ˙ X
61 57 58 59 60 syl12anc ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n = ∑ Q n ∈ ℕ 0 U ∘ G ⁡ n ∗ ˙ n × ˙ X
62 fvco3 ⊢ G : ℕ 0 ⟶ S ∧ n ∈ ℕ 0 → U ∘ G ⁡ n = U ⁡ G ⁡ n
63 62 eqcomd ⊢ G : ℕ 0 ⟶ S ∧ n ∈ ℕ 0 → U ⁡ G ⁡ n = U ∘ G ⁡ n
64 46 63 sylan ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → U ⁡ G ⁡ n = U ∘ G ⁡ n
65 64 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → T ⁡ U ⁡ G ⁡ n = T ⁡ U ∘ G ⁡ n
66 65 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n = n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n
67 66 mpteq2dva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → n ∈ ℕ 0 ⟼ n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n = n ∈ ℕ 0 ⟼ n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n
68 67 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n
69 68 fveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n = I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ∘ G ⁡ n
70 64 oveq1d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ n ∈ ℕ 0 → U ⁡ G ⁡ n ∗ ˙ n × ˙ X = U ∘ G ⁡ n ∗ ˙ n × ˙ X
71 70 mpteq2dva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → n ∈ ℕ 0 ⟼ U ⁡ G ⁡ n ∗ ˙ n × ˙ X = n ∈ ℕ 0 ⟼ U ∘ G ⁡ n ∗ ˙ n × ˙ X
72 71 oveq2d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X = ∑ Q n ∈ ℕ 0 U ∘ G ⁡ n ∗ ˙ n × ˙ X
73 61 69 72 3eqtr4d ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → I ⁡ ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
74 55 73 sylan9eqr ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s ∧ D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n → I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
75 74 ex ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ T ⁡ U ⁡ G ⁡ n → I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
76 54 75 sylbid ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ ∧ b ∈ B 0 … s → D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n → I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
77 76 reximdva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B ∧ s ∈ ℕ → ∃ b ∈ B 0 … s D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n → ∃ b ∈ B 0 … s I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
78 77 reximdva ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s D × ˙ J ⁡ D = ∑ Y n ∈ ℕ 0 n ⋅ mulGrp P Z · ˙ G ⁡ n → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X
79 38 78 mpd ⊢ N ∈ Fin ∧ R ∈ CRing ∧ M ∈ B → ∃ s ∈ ℕ ∃ b ∈ B 0 … s I ⁡ D × ˙ J ⁡ D = ∑ Q n ∈ ℕ 0 U ⁡ G ⁡ n ∗ ˙ n × ˙ X