Metamath Proof Explorer


Theorem cpmat

Description: Value of the constructor of the set of all constant polynomial matrices, i.e. the set of all N x N matrices of polynomials over a ring R . (Contributed by AV, 15-Nov-2019)

Ref Expression
Hypotheses cpmat.s
|- S = ( N ConstPolyMat R )
cpmat.p
|- P = ( Poly1 ` R )
cpmat.c
|- C = ( N Mat P )
cpmat.b
|- B = ( Base ` C )
Assertion cpmat
|- ( ( N e. Fin /\ R e. V ) -> S = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )

Proof

Step Hyp Ref Expression
1 cpmat.s
 |-  S = ( N ConstPolyMat R )
2 cpmat.p
 |-  P = ( Poly1 ` R )
3 cpmat.c
 |-  C = ( N Mat P )
4 cpmat.b
 |-  B = ( Base ` C )
5 df-cpmat
 |-  ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } )
6 5 a1i
 |-  ( ( N e. Fin /\ R e. V ) -> ConstPolyMat = ( n e. Fin , r e. _V |-> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } ) )
7 simpl
 |-  ( ( n = N /\ r = R ) -> n = N )
8 fveq2
 |-  ( r = R -> ( Poly1 ` r ) = ( Poly1 ` R ) )
9 8 adantl
 |-  ( ( n = N /\ r = R ) -> ( Poly1 ` r ) = ( Poly1 ` R ) )
10 7 9 oveq12d
 |-  ( ( n = N /\ r = R ) -> ( n Mat ( Poly1 ` r ) ) = ( N Mat ( Poly1 ` R ) ) )
11 10 fveq2d
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = ( Base ` ( N Mat ( Poly1 ` R ) ) ) )
12 2 oveq2i
 |-  ( N Mat P ) = ( N Mat ( Poly1 ` R ) )
13 3 12 eqtri
 |-  C = ( N Mat ( Poly1 ` R ) )
14 13 fveq2i
 |-  ( Base ` C ) = ( Base ` ( N Mat ( Poly1 ` R ) ) )
15 4 14 eqtri
 |-  B = ( Base ` ( N Mat ( Poly1 ` R ) ) )
16 11 15 eqtr4di
 |-  ( ( n = N /\ r = R ) -> ( Base ` ( n Mat ( Poly1 ` r ) ) ) = B )
17 fveq2
 |-  ( r = R -> ( 0g ` r ) = ( 0g ` R ) )
18 17 adantl
 |-  ( ( n = N /\ r = R ) -> ( 0g ` r ) = ( 0g ` R ) )
19 18 eqeq2d
 |-  ( ( n = N /\ r = R ) -> ( ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) )
20 19 ralbidv
 |-  ( ( n = N /\ r = R ) -> ( A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) )
21 7 20 raleqbidv
 |-  ( ( n = N /\ r = R ) -> ( A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) )
22 7 21 raleqbidv
 |-  ( ( n = N /\ r = R ) -> ( A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) <-> A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) ) )
23 16 22 rabeqbidv
 |-  ( ( n = N /\ r = R ) -> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
24 23 adantl
 |-  ( ( ( N e. Fin /\ R e. V ) /\ ( n = N /\ r = R ) ) -> { m e. ( Base ` ( n Mat ( Poly1 ` r ) ) ) | A. i e. n A. j e. n A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` r ) } = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
25 simpl
 |-  ( ( N e. Fin /\ R e. V ) -> N e. Fin )
26 elex
 |-  ( R e. V -> R e. _V )
27 26 adantl
 |-  ( ( N e. Fin /\ R e. V ) -> R e. _V )
28 4 fvexi
 |-  B e. _V
29 rabexg
 |-  ( B e. _V -> { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } e. _V )
30 28 29 mp1i
 |-  ( ( N e. Fin /\ R e. V ) -> { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } e. _V )
31 6 24 25 27 30 ovmpod
 |-  ( ( N e. Fin /\ R e. V ) -> ( N ConstPolyMat R ) = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
32 1 31 syl5eq
 |-  ( ( N e. Fin /\ R e. V ) -> S = { m e. B | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )