# Metamath Proof Explorer

## Theorem idpm2idmp

Description: The transformation of the identity polynomial matrix into polynomials over matrices results in the identity of the polynomials over matrices. (Contributed by AV, 18-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpval.m
pm2mpval.e
pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion idpm2idmp ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\left({1}_{{C}}\right)={1}_{{Q}}$

### Proof

Step Hyp Ref Expression
1 pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpval.m
5 pm2mpval.e
6 pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
10 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
11 eqid ${⊢}{1}_{{C}}={1}_{{C}}$
12 3 11 ringidcl ${⊢}{C}\in \mathrm{Ring}\to {1}_{{C}}\in {B}$
13 10 12 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{C}}\in {B}$
14 1 2 3 4 5 6 7 8 9 pm2mpfval
15 13 14 mpd3an3
16 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
17 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
18 1 2 11 7 16 17 decpmatid ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {k}\in {ℕ}_{0}\right)\to {1}_{{C}}\mathrm{decompPMat}{k}=if\left({k}=0,{1}_{{A}},{0}_{{A}}\right)$
19 18 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {k}\in {ℕ}_{0}\right)\to {1}_{{C}}\mathrm{decompPMat}{k}=if\left({k}=0,{1}_{{A}},{0}_{{A}}\right)$
20 19 oveq1d
21 20 mpteq2dva
22 21 oveq2d
23 ovif
24 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
25 8 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
26 24 25 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
27 26 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
28 27 fveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {k}\in {ℕ}_{0}\right)\to {1}_{{A}}={1}_{\mathrm{Scalar}\left({Q}\right)}$
29 28 oveq1d
30 8 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
31 24 30 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
32 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
33 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
34 8 6 32 5 33 ply1moncl
35 24 34 sylan
36 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
37 eqid ${⊢}{1}_{\mathrm{Scalar}\left({Q}\right)}={1}_{\mathrm{Scalar}\left({Q}\right)}$
38 33 36 4 37 lmodvs1
39 31 35 38 syl2an2r
40 29 39 eqtrd
41 27 fveq2d ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {k}\in {ℕ}_{0}\right)\to {0}_{{A}}={0}_{\mathrm{Scalar}\left({Q}\right)}$
42 41 oveq1d
43 eqid ${⊢}{0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{\mathrm{Scalar}\left({Q}\right)}$
44 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
45 33 36 4 43 44 lmod0vs
46 31 35 45 syl2an2r
47 42 46 eqtrd
48 40 47 ifeq12d
49 23 48 syl5eq
50 49 mpteq2dva
51 50 oveq2d
52 8 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
53 ringmnd ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{Mnd}$
54 24 52 53 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Mnd}$
55 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
56 55 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {ℕ}_{0}\in \mathrm{V}$
57 0nn0 ${⊢}0\in {ℕ}_{0}$
58 57 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to 0\in {ℕ}_{0}$
59 eqid
60 35 ralrimiva
61 44 54 56 58 59 60 gsummpt1n0
62 c0ex ${⊢}0\in \mathrm{V}$
63 csbov1g
64 62 63 mp1i
65 csbvarg
66 62 65 mp1i
67 66 oveq1d
68 8 6 32 5 ply1idvr1
69 24 68 syl
70 64 67 69 3eqtrd
71 51 61 70 3eqtrd
72 15 22 71 3eqtrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\left({1}_{{C}}\right)={1}_{{Q}}$