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 )
6 5 ad4antlr 
 |-  ( ( ( ( ( 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 ) ) )
13 12 adantr 
 |-  ( ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. S /\ y e. S ) ) /\ i e. N ) -> ( x e. ( Base ` C ) /\ y e. ( Base ` C ) ) )
14 13 adantr 
 |-  ( ( ( ( ( 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 ) ) ) ) ) )
21 20 adantr 
 |-  ( ( ( ( ( ( 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 )
29 28 adantr 
 |-  ( ( ( 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 )
31 30 adantr 
 |-  ( ( ( 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 )
33 32 adantr 
 |-  ( ( ( 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 )