# Metamath Proof Explorer

## Theorem mply1topmatcl

Description: A polynomial over matrices transformed into a polynomial matrix is a polynomial matrix. (Contributed by AV, 6-Oct-2019)

Ref Expression
Hypotheses mply1topmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mply1topmat.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
mply1topmat.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
mply1topmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
mply1topmat.m
mply1topmat.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
mply1topmat.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
mply1topmat.i
mply1topmatcl.c ${⊢}{C}={N}\mathrm{Mat}{P}$
mply1topmatcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion mply1topmatcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {I}\left({O}\right)\in {B}$

### Proof

Step Hyp Ref Expression
1 mply1topmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mply1topmat.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
3 mply1topmat.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
4 mply1topmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
5 mply1topmat.m
6 mply1topmat.e ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
7 mply1topmat.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
8 mply1topmat.i
9 mply1topmatcl.c ${⊢}{C}={N}\mathrm{Mat}{P}$
10 mply1topmatcl.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
11 1 2 3 4 5 6 7 8 mply1topmatval
13 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
14 simp1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {N}\in \mathrm{Fin}$
15 4 fvexi ${⊢}{P}\in \mathrm{V}$
16 15 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{V}$
17 eqid ${⊢}{0}_{{P}}={0}_{{P}}$
18 4 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
19 ringcmn ${⊢}{P}\in \mathrm{Ring}\to {P}\in \mathrm{CMnd}$
20 18 19 syl ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{CMnd}$
21 20 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{CMnd}$
22 21 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {P}\in \mathrm{CMnd}$
23 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
24 23 a1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {ℕ}_{0}\in \mathrm{V}$
25 4 ply1lmod ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{LMod}$
26 25 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{LMod}$
27 26 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {P}\in \mathrm{LMod}$
28 27 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {P}\in \mathrm{LMod}$
29 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
30 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
31 simpl2 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}\in {N}$
32 simpl3 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {j}\in {N}$
33 simpl13 ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {O}\in {L}$
34 eqid ${⊢}{\mathrm{coe}}_{1}\left({O}\right)={\mathrm{coe}}_{1}\left({O}\right)$
35 34 3 2 30 coe1f ${⊢}{O}\in {L}\to {\mathrm{coe}}_{1}\left({O}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{A}}$
36 33 35 syl ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right):{ℕ}_{0}⟶{\mathrm{Base}}_{{A}}$
37 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
38 36 37 ffvelrnd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
39 1 29 30 31 32 38 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{{R}}$
40 4 ply1sca ${⊢}{R}\in \mathrm{Ring}\to {R}=\mathrm{Scalar}\left({P}\right)$
41 40 eqcomd ${⊢}{R}\in \mathrm{Ring}\to \mathrm{Scalar}\left({P}\right)={R}$
42 41 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to \mathrm{Scalar}\left({P}\right)={R}$
43 42 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
44 43 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
45 44 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{{R}}$
46 39 45 eleqtrrd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {i}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){j}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
47 18 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {P}\in \mathrm{Ring}$
48 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
49 48 ringmgp ${⊢}{P}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
50 47 49 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
51 50 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
52 51 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
53 7 4 13 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {Y}\in {\mathrm{Base}}_{{P}}$
54 53 3ad2ant2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
55 54 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
56 55 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
57 48 13 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{P}}}$
58 57 6 mulgnn0cl ${⊢}\left({\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}\wedge {k}\in {ℕ}_{0}\wedge {Y}\in {\mathrm{Base}}_{{P}}\right)\to {k}{E}{Y}\in {\mathrm{Base}}_{{P}}$
59 52 37 56 58 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {i}\in {N}\wedge {j}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}{E}{Y}\in {\mathrm{Base}}_{{P}}$
60 eqid ${⊢}\mathrm{Scalar}\left({P}\right)=\mathrm{Scalar}\left({P}\right)$
61 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({P}\right)}$
62 13 60 5 61 lmodvscl
63 28 46 59 62 syl3anc
64 63 fmpttd
65 1 2 3 4 5 6 7 mply1topmatcllem
66 13 17 22 24 64 65 gsumcl
67 9 13 10 14 16 66 matbas2d
68 12 67 eqeltrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {I}\left({O}\right)\in {B}$