# Metamath Proof Explorer

## Theorem cpmatmcl

Description: The set of all constant polynomial matrices over a ring R is closed under multiplication. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
cpmatsrngpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cpmatsrngpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
Assertion cpmatmcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{C}}{y}\in {S}$

### Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
2 cpmatsrngpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 cpmatsrngpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
4 1 2 3 cpmatmcllem ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}$
5 2 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
6 5 ad4antlr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to {P}\in \mathrm{Ring}$
7 eqid ${⊢}{\mathrm{Base}}_{{C}}={\mathrm{Base}}_{{C}}$
8 1 2 3 7 cpmatpmat ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {S}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
9 8 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {S}\right)\to {x}\in {\mathrm{Base}}_{{C}}$
10 1 2 3 7 cpmatpmat ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {S}\right)\to {y}\in {\mathrm{Base}}_{{C}}$
11 10 3expa ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {y}\in {S}\right)\to {y}\in {\mathrm{Base}}_{{C}}$
12 9 11 anim12dan ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)$
13 12 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\to \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)$
14 13 adantr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)$
15 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\to {i}\in {N}$
16 15 anim1i ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to \left({i}\in {N}\wedge {j}\in {N}\right)$
17 eqid ${⊢}{\cdot }_{{C}}={\cdot }_{{C}}$
18 3 7 17 matmulcell ${⊢}\left({P}\in \mathrm{Ring}\wedge \left({x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\left({x}{\cdot }_{{C}}{y}\right){j}=\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)$
19 6 14 16 18 syl3anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to {i}\left({x}{\cdot }_{{C}}{y}\right){j}=\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)$
20 19 fveq2d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)$
21 20 adantr ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\wedge {c}\in ℕ\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)$
22 21 fveq1d ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\wedge {c}\in ℕ\right)\to {\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)$
23 22 eqeq1d ${⊢}\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\wedge {c}\in ℕ\right)\to \left({\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
24 23 ralbidva ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\wedge {j}\in {N}\right)\to \left(\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}↔\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
25 24 ralbidva ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\wedge {i}\in {N}\right)\to \left(\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}↔\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
26 25 ralbidva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left(\underset{{k}\in {N}}{{\sum }_{{P}}}\left(\left({i}{x}{k}\right){\cdot }_{{P}}\left({k}{y}{j}\right)\right)\right)\left({c}\right)={0}_{{R}}\right)$
27 4 26 mpbird ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}$
28 simpl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {N}\in \mathrm{Fin}$
29 28 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {N}\in \mathrm{Fin}$
30 simpr ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {R}\in \mathrm{Ring}$
31 30 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {R}\in \mathrm{Ring}$
32 2 3 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
33 32 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {C}\in \mathrm{Ring}$
34 simpl ${⊢}\left({x}\in {S}\wedge {y}\in {S}\right)\to {x}\in {S}$
35 34 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {S}\right)$
36 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {S}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {x}\in {S}\right)$
37 35 36 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}\in {S}\right)$
38 37 8 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}\in {\mathrm{Base}}_{{C}}$
39 simpr ${⊢}\left({x}\in {S}\wedge {y}\in {S}\right)\to {y}\in {S}$
40 39 anim2i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {y}\in {S}\right)$
41 df-3an ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {S}\right)↔\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {y}\in {S}\right)$
42 40 41 sylibr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {y}\in {S}\right)$
43 42 10 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {y}\in {\mathrm{Base}}_{{C}}$
44 7 17 ringcl ${⊢}\left({C}\in \mathrm{Ring}\wedge {x}\in {\mathrm{Base}}_{{C}}\wedge {y}\in {\mathrm{Base}}_{{C}}\right)\to {x}{\cdot }_{{C}}{y}\in {\mathrm{Base}}_{{C}}$
45 33 38 43 44 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{\cdot }_{{C}}{y}\in {\mathrm{Base}}_{{C}}$
46 1 2 3 7 cpmatel ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {x}{\cdot }_{{C}}{y}\in {\mathrm{Base}}_{{C}}\right)\to \left({x}{\cdot }_{{C}}{y}\in {S}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}\right)$
47 29 31 45 46 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to \left({x}{\cdot }_{{C}}{y}\in {S}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {c}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}\left({x}{\cdot }_{{C}}{y}\right){j}\right)\left({c}\right)={0}_{{R}}\right)$
48 27 47 mpbird ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{\cdot }_{{C}}{y}\in {S}$
49 48 ralrimivva ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \forall {x}\in {S}\phantom{\rule{.4em}{0ex}}\forall {y}\in {S}\phantom{\rule{.4em}{0ex}}{x}{\cdot }_{{C}}{y}\in {S}$