Metamath Proof Explorer


Theorem pm2mpval

Description: Value of the transformation of a polynomial matrix into a polynomial over matrices. (Contributed by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p P = Poly 1 R
pm2mpval.c C = N Mat P
pm2mpval.b B = Base C
pm2mpval.m ˙ = Q
pm2mpval.e × ˙ = mulGrp Q
pm2mpval.x X = var 1 A
pm2mpval.a A = N Mat R
pm2mpval.q Q = Poly 1 A
pm2mpval.t T = N pMatToMatPoly R
Assertion pm2mpval N Fin R V T = m B Q k 0 m decompPMat k ˙ k × ˙ X

Proof

Step Hyp Ref Expression
1 pm2mpval.p P = Poly 1 R
2 pm2mpval.c C = N Mat P
3 pm2mpval.b B = Base C
4 pm2mpval.m ˙ = Q
5 pm2mpval.e × ˙ = mulGrp Q
6 pm2mpval.x X = var 1 A
7 pm2mpval.a A = N Mat R
8 pm2mpval.q Q = Poly 1 A
9 pm2mpval.t T = N pMatToMatPoly R
10 df-pm2mp pMatToMatPoly = n Fin , r V m Base n Mat Poly 1 r n Mat r / a Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a
11 10 a1i N Fin R V pMatToMatPoly = n Fin , r V m Base n Mat Poly 1 r n Mat r / a Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a
12 simpl n = N r = R n = N
13 fveq2 r = R Poly 1 r = Poly 1 R
14 13 adantl n = N r = R Poly 1 r = Poly 1 R
15 12 14 oveq12d n = N r = R n Mat Poly 1 r = N Mat Poly 1 R
16 15 fveq2d n = N r = R Base n Mat Poly 1 r = Base N Mat Poly 1 R
17 1 oveq2i N Mat P = N Mat Poly 1 R
18 2 17 eqtri C = N Mat Poly 1 R
19 18 fveq2i Base C = Base N Mat Poly 1 R
20 3 19 eqtri B = Base N Mat Poly 1 R
21 16 20 syl6eqr n = N r = R Base n Mat Poly 1 r = B
22 21 adantl N Fin R V n = N r = R Base n Mat Poly 1 r = B
23 ovex n Mat r V
24 fvexd a = n Mat r Poly 1 a V
25 simpr a = n Mat r q = Poly 1 a q = Poly 1 a
26 fveq2 a = n Mat r Poly 1 a = Poly 1 n Mat r
27 26 adantr a = n Mat r q = Poly 1 a Poly 1 a = Poly 1 n Mat r
28 25 27 eqtrd a = n Mat r q = Poly 1 a q = Poly 1 n Mat r
29 28 fveq2d a = n Mat r q = Poly 1 a q = Poly 1 n Mat r
30 eqidd a = n Mat r q = Poly 1 a m decompPMat k = m decompPMat k
31 28 fveq2d a = n Mat r q = Poly 1 a mulGrp q = mulGrp Poly 1 n Mat r
32 31 fveq2d a = n Mat r q = Poly 1 a mulGrp q = mulGrp Poly 1 n Mat r
33 eqidd a = n Mat r q = Poly 1 a k = k
34 fveq2 a = n Mat r var 1 a = var 1 n Mat r
35 34 adantr a = n Mat r q = Poly 1 a var 1 a = var 1 n Mat r
36 32 33 35 oveq123d a = n Mat r q = Poly 1 a k mulGrp q var 1 a = k mulGrp Poly 1 n Mat r var 1 n Mat r
37 29 30 36 oveq123d a = n Mat r q = Poly 1 a m decompPMat k q k mulGrp q var 1 a = m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r
38 37 mpteq2dv a = n Mat r q = Poly 1 a k 0 m decompPMat k q k mulGrp q var 1 a = k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r
39 28 38 oveq12d a = n Mat r q = Poly 1 a q k 0 m decompPMat k q k mulGrp q var 1 a = Poly 1 n Mat r k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r
40 24 39 csbied a = n Mat r Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a = Poly 1 n Mat r k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r
41 23 40 csbie n Mat r / a Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a = Poly 1 n Mat r k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r
42 oveq12 n = N r = R n Mat r = N Mat R
43 42 fveq2d n = N r = R Poly 1 n Mat r = Poly 1 N Mat R
44 7 fveq2i Poly 1 A = Poly 1 N Mat R
45 8 44 eqtri Q = Poly 1 N Mat R
46 43 45 syl6eqr n = N r = R Poly 1 n Mat r = Q
47 43 fveq2d n = N r = R Poly 1 n Mat r = Poly 1 N Mat R
48 45 fveq2i Q = Poly 1 N Mat R
49 4 48 eqtri ˙ = Poly 1 N Mat R
50 47 49 syl6eqr n = N r = R Poly 1 n Mat r = ˙
51 eqidd n = N r = R m decompPMat k = m decompPMat k
52 43 fveq2d n = N r = R mulGrp Poly 1 n Mat r = mulGrp Poly 1 N Mat R
53 52 fveq2d n = N r = R mulGrp Poly 1 n Mat r = mulGrp Poly 1 N Mat R
54 45 fveq2i mulGrp Q = mulGrp Poly 1 N Mat R
55 54 fveq2i mulGrp Q = mulGrp Poly 1 N Mat R
56 5 55 eqtri × ˙ = mulGrp Poly 1 N Mat R
57 53 56 syl6eqr n = N r = R mulGrp Poly 1 n Mat r = × ˙
58 eqidd n = N r = R k = k
59 42 fveq2d n = N r = R var 1 n Mat r = var 1 N Mat R
60 7 fveq2i var 1 A = var 1 N Mat R
61 6 60 eqtri X = var 1 N Mat R
62 59 61 syl6eqr n = N r = R var 1 n Mat r = X
63 57 58 62 oveq123d n = N r = R k mulGrp Poly 1 n Mat r var 1 n Mat r = k × ˙ X
64 50 51 63 oveq123d n = N r = R m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r = m decompPMat k ˙ k × ˙ X
65 64 mpteq2dv n = N r = R k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r = k 0 m decompPMat k ˙ k × ˙ X
66 46 65 oveq12d n = N r = R Poly 1 n Mat r k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r = Q k 0 m decompPMat k ˙ k × ˙ X
67 66 adantl N Fin R V n = N r = R Poly 1 n Mat r k 0 m decompPMat k Poly 1 n Mat r k mulGrp Poly 1 n Mat r var 1 n Mat r = Q k 0 m decompPMat k ˙ k × ˙ X
68 41 67 syl5eq N Fin R V n = N r = R n Mat r / a Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a = Q k 0 m decompPMat k ˙ k × ˙ X
69 22 68 mpteq12dv N Fin R V n = N r = R m Base n Mat Poly 1 r n Mat r / a Poly 1 a / q q k 0 m decompPMat k q k mulGrp q var 1 a = m B Q k 0 m decompPMat k ˙ k × ˙ X
70 simpl N Fin R V N Fin
71 elex R V R V
72 71 adantl N Fin R V R V
73 3 fvexi B V
74 73 mptex m B Q k 0 m decompPMat k ˙ k × ˙ X V
75 74 a1i N Fin R V m B Q k 0 m decompPMat k ˙ k × ˙ X V
76 11 69 70 72 75 ovmpod N Fin R V N pMatToMatPoly R = m B Q k 0 m decompPMat k ˙ k × ˙ X
77 9 76 syl5eq N Fin R V T = m B Q k 0 m decompPMat k ˙ k × ˙ X