# Metamath Proof Explorer

## Theorem cpmatmcl

Description: The set of all constant polynomial matrices over a ring R is closed under multiplication. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s
`|- S = ( N ConstPolyMat R )`
cpmatsrngpmat.p
`|- P = ( Poly1 ` R )`
cpmatsrngpmat.c
`|- C = ( N Mat P )`
Assertion cpmatmcl
`|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S )`

### Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s
` |-  S = ( N ConstPolyMat R )`
2 cpmatsrngpmat.p
` |-  P = ( Poly1 ` R )`
3 cpmatsrngpmat.c
` |-  C = ( N Mat P )`
4 1 2 3 cpmatmcllem
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) )`
5 2 ply1ring
` |-  ( R e. Ring -> P e. Ring )`
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> P e. Ring )`
7 eqid
` |-  ( Base ` C ) = ( Base ` C )`
8 1 2 3 7 cpmatpmat
` |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) -> x e. ( Base ` C ) )`
9 8 3expa
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) -> x e. ( Base ` C ) )`
10 1 2 3 7 cpmatpmat
` |-  ( ( N e. Fin /\ R e. Ring /\ y e. S ) -> y e. ( Base ` C ) )`
11 10 3expa
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ y e. S ) -> y e. ( Base ` C ) )`
12 9 11 anim12dan
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) )`
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) )`
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) )`
15 simpr
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) -> i e. N )`
16 15 anim1i
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> ( i e. N /\ j e. N ) )`
17 eqid
` |-  ( .r ` C ) = ( .r ` C )`
18 3 7 17 matmulcell
` |-  ( ( P e. Ring /\ ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) /\ ( i e. N /\ j e. N ) ) -> ( i ( x ( .r ` C ) y ) j ) = ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) )`
19 6 14 16 18 syl3anc
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> ( i ( x ( .r ` C ) y ) j ) = ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) )`
20 19 fveq2d
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) = ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) )`
` |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) /\ c e. NN ) -> ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) = ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) )`
22 21 fveq1d
` |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) /\ c e. NN ) -> ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) )`
23 22 eqeq1d
` |-  ( ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) /\ c e. NN ) -> ( ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) <-> ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )`
24 23 ralbidva
` |-  ( ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) /\ j e. N ) -> ( A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) <-> A. c e. NN ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )`
25 24 ralbidva
` |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) -> ( A. j e. N A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) <-> A. j e. N A. c e. NN ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )`
26 25 ralbidva
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) <-> A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( P gsum ( k e. N |-> ( ( i x k ) ( .r ` P ) ( k y j ) ) ) ) ) ` c ) = ( 0g ` R ) ) )`
27 4 26 mpbird
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) )`
28 simpl
` |-  ( ( N e. Fin /\ R e. Ring ) -> N e. Fin )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> N e. Fin )`
30 simpr
` |-  ( ( N e. Fin /\ R e. Ring ) -> R e. Ring )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> R e. Ring )`
32 2 3 pmatring
` |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )`
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> C e. Ring )`
34 simpl
` |-  ( ( x e. S /\ y e. S ) -> x e. S )`
35 34 anim2i
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) )`
36 df-3an
` |-  ( ( N e. Fin /\ R e. Ring /\ x e. S ) <-> ( ( N e. Fin /\ R e. Ring ) /\ x e. S ) )`
37 35 36 sylibr
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( N e. Fin /\ R e. Ring /\ x e. S ) )`
38 37 8 syl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> x e. ( Base ` C ) )`
39 simpr
` |-  ( ( x e. S /\ y e. S ) -> y e. S )`
40 39 anim2i
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( N e. Fin /\ R e. Ring ) /\ y e. S ) )`
41 df-3an
` |-  ( ( N e. Fin /\ R e. Ring /\ y e. S ) <-> ( ( N e. Fin /\ R e. Ring ) /\ y e. S ) )`
42 40 41 sylibr
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( N e. Fin /\ R e. Ring /\ y e. S ) )`
43 42 10 syl
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> y e. ( Base ` C ) )`
44 7 17 ringcl
` |-  ( ( C e. Ring /\ x e. ( Base ` C ) /\ y e. ( Base ` C ) ) -> ( x ( .r ` C ) y ) e. ( Base ` C ) )`
45 33 38 43 44 syl3anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` C ) y ) e. ( Base ` C ) )`
46 1 2 3 7 cpmatel
` |-  ( ( N e. Fin /\ R e. Ring /\ ( x ( .r ` C ) y ) e. ( Base ` C ) ) -> ( ( x ( .r ` C ) y ) e. S <-> A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) ) )`
47 29 31 45 46 syl3anc
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( ( x ( .r ` C ) y ) e. S <-> A. i e. N A. j e. N A. c e. NN ( ( coe1 ` ( i ( x ( .r ` C ) y ) j ) ) ` c ) = ( 0g ` R ) ) )`
48 27 47 mpbird
` |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` C ) y ) e. S )`
49 48 ralrimivva
` |-  ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S )`