# Metamath Proof Explorer

## Theorem cpmatel

Description: Property of a constant polynomial matrix. (Contributed by AV, 15-Nov-2019)

Ref Expression
Hypotheses cpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
cpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
cpmat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
Assertion cpmatel ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\wedge {M}\in {B}\right)\to \left({M}\in {S}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$

### Proof

Step Hyp Ref Expression
1 cpmat.s ${⊢}{S}={N}\mathrm{ConstPolyMat}{R}$
2 cpmat.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
3 cpmat.c ${⊢}{C}={N}\mathrm{Mat}{P}$
4 cpmat.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
5 1 2 3 4 cpmat ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\right)\to {S}=\left\{{m}\in {B}|\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}\right\}$
6 5 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\wedge {M}\in {B}\right)\to {S}=\left\{{m}\in {B}|\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}\right\}$
7 6 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\wedge {M}\in {B}\right)\to \left({M}\in {S}↔{M}\in \left\{{m}\in {B}|\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}\right\}\right)$
8 oveq ${⊢}{m}={M}\to {i}{m}{j}={i}{M}{j}$
9 8 fveq2d ${⊢}{m}={M}\to {\mathrm{coe}}_{1}\left({i}{m}{j}\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)$
10 9 fveq1d ${⊢}{m}={M}\to {\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)$
11 10 eqeq1d ${⊢}{m}={M}\to \left({\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}↔{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
12 11 ralbidv ${⊢}{m}={M}\to \left(\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}↔\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
13 12 2ralbidv ${⊢}{m}={M}\to \left(\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
14 13 elrab ${⊢}{M}\in \left\{{m}\in {B}|\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{m}{j}\right)\left({k}\right)={0}_{{R}}\right\}↔\left({M}\in {B}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$
15 7 14 syl6bb ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\wedge {M}\in {B}\right)\to \left({M}\in {S}↔\left({M}\in {B}\wedge \forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)\right)$
16 15 3anibar ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in {V}\wedge {M}\in {B}\right)\to \left({M}\in {S}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}\forall {k}\in ℕ\phantom{\rule{.4em}{0ex}}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({k}\right)={0}_{{R}}\right)$