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 ConstPolyMat R
cpmat.p P = Poly 1 R
cpmat.c C = N Mat P
cpmat.b B = Base C
Assertion cpmatel N Fin R V M B M S i N j N k coe 1 i M j k = 0 R

Proof

Step Hyp Ref Expression
1 cpmat.s S = N ConstPolyMat R
2 cpmat.p P = Poly 1 R
3 cpmat.c C = N Mat P
4 cpmat.b B = Base C
5 1 2 3 4 cpmat N Fin R V S = m B | i N j N k coe 1 i m j k = 0 R
6 5 3adant3 N Fin R V M B S = m B | i N j N k coe 1 i m j k = 0 R
7 6 eleq2d N Fin R V M B M S M m B | i N j N k coe 1 i m j k = 0 R
8 oveq m = M i m j = i M j
9 8 fveq2d m = M coe 1 i m j = coe 1 i M j
10 9 fveq1d m = M coe 1 i m j k = coe 1 i M j k
11 10 eqeq1d m = M coe 1 i m j k = 0 R coe 1 i M j k = 0 R
12 11 ralbidv m = M k coe 1 i m j k = 0 R k coe 1 i M j k = 0 R
13 12 2ralbidv m = M i N j N k coe 1 i m j k = 0 R i N j N k coe 1 i M j k = 0 R
14 13 elrab M m B | i N j N k coe 1 i m j k = 0 R M B i N j N k coe 1 i M j k = 0 R
15 7 14 bitrdi N Fin R V M B M S M B i N j N k coe 1 i M j k = 0 R
16 15 3anibar N Fin R V M B M S i N j N k coe 1 i M j k = 0 R