Metamath Proof Explorer

Theorem cpmatel

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

Ref Expression
Hypotheses cpmat.s ⊢S=NConstPolyMatR
cpmat.p ⊢P=Poly1⁡R
cpmat.c ⊢C=NMatP
cpmat.b ⊢B=BaseC
Assertion cpmatel ⊢N∈Fin∧R∈V∧M∈B→M∈S↔∀i∈N∀j∈N∀k∈ℕcoe1⁡iMj⁡k=0R

Proof

Step Hyp Ref Expression
1 cpmat.s ⊢S=NConstPolyMatR
2 cpmat.p ⊢P=Poly1⁡R
3 cpmat.c ⊢C=NMatP
4 cpmat.b ⊢B=BaseC
5 1 2 3 4 cpmat ⊢N∈Fin∧R∈V→S=m∈B|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R
6 5 3adant3 ⊢N∈Fin∧R∈V∧M∈B→S=m∈B|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R
7 6 eleq2d ⊢N∈Fin∧R∈V∧M∈B→M∈S↔M∈m∈B|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R
8 oveq ⊢m=M→imj=iMj
9 8 fveq2d ⊢m=M→coe1⁡imj=coe1⁡iMj
10 9 fveq1d ⊢m=M→coe1⁡imj⁡k=coe1⁡iMj⁡k
11 10 eqeq1d ⊢m=M→coe1⁡imj⁡k=0R↔coe1⁡iMj⁡k=0R
12 11 ralbidv ⊢m=M→∀k∈ℕcoe1⁡imj⁡k=0R↔∀k∈ℕcoe1⁡iMj⁡k=0R
13 12 2ralbidv ⊢m=M→∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R↔∀i∈N∀j∈N∀k∈ℕcoe1⁡iMj⁡k=0R
14 13 elrab ⊢M∈m∈B|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R↔M∈B∧∀i∈N∀j∈N∀k∈ℕcoe1⁡iMj⁡k=0R
15 7 14 bitrdi ⊢N∈Fin∧R∈V∧M∈B→M∈S↔M∈B∧∀i∈N∀j∈N∀k∈ℕcoe1⁡iMj⁡k=0R
16 15 3anibar ⊢N∈Fin∧R∈V∧M∈B→M∈S↔∀i∈N∀j∈N∀k∈ℕcoe1⁡iMj⁡k=0R