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 eqtrid 
 |-  ( ( 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 ) } )