Metamath Proof Explorer

Theorem 1elcpmat

Description: The identity of the ring of all polynomial matrices over the ring R is a constant polynomial matrix. (Contributed by AV, 16-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s 
|- S = ( N ConstPolyMat R )
cpmatsrngpmat.p 
|- P = ( Poly1 ` R )
cpmatsrngpmat.c 
|- C = ( N Mat P )
Assertion 1elcpmat 
|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) 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 eqid 
 |-  ( Base ` R ) = ( Base ` R )
5 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
6 4 5 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
7 6 ancli 
 |-  ( R e. Ring -> ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) )
8 7 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) )
9 8 ad2antrl 
 |-  ( ( i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) )
10 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
11 eqid 
 |-  ( Base ` P ) = ( Base ` P )
12 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
13 4 10 2 11 12 cply1coe0 
 |-  ( ( R e. Ring /\ ( 1r ` R ) e. ( Base ` R ) ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) = ( 0g ` R ) )
14 9 13 syl 
 |-  ( ( i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) = ( 0g ` R ) )
15 iftrue 
 |-  ( i = j -> if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) = ( ( algSc ` P ) ` ( 1r ` R ) ) )
16 15 fveq2d 
 |-  ( i = j -> ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) = ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) )
17 16 fveq1d 
 |-  ( i = j -> ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) )
18 17 eqeq1d 
 |-  ( i = j -> ( ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) = ( 0g ` R ) ) )
19 18 ralbidv 
 |-  ( i = j -> ( A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) <-> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) = ( 0g ` R ) ) )
20 19 adantr 
 |-  ( ( i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) <-> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 1r ` R ) ) ) ` n ) = ( 0g ` R ) ) )
21 14 20 mpbird 
 |-  ( ( i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) )
22 4 10 ring0cl 
 |-  ( R e. Ring -> ( 0g ` R ) e. ( Base ` R ) )
23 22 ancli 
 |-  ( R e. Ring -> ( R e. Ring /\ ( 0g ` R ) e. ( Base ` R ) ) )
24 23 adantl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( R e. Ring /\ ( 0g ` R ) e. ( Base ` R ) ) )
25 4 10 2 11 12 cply1coe0 
 |-  ( ( R e. Ring /\ ( 0g ` R ) e. ( Base ` R ) ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) = ( 0g ` R ) )
26 24 25 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) = ( 0g ` R ) )
27 26 ad2antrl 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) = ( 0g ` R ) )
28 iffalse 
 |-  ( -. i = j -> if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) = ( ( algSc ` P ) ` ( 0g ` R ) ) )
29 28 adantr 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) = ( ( algSc ` P ) ` ( 0g ` R ) ) )
30 29 fveq2d 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) = ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) )
31 30 fveq1d 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) )
32 31 eqeq1d 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) = ( 0g ` R ) ) )
33 32 ralbidv 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> ( A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) <-> A. n e. NN ( ( coe1 ` ( ( algSc ` P ) ` ( 0g ` R ) ) ) ` n ) = ( 0g ` R ) ) )
34 27 33 mpbird 
 |-  ( ( -. i = j /\ ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) ) -> A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) )
35 21 34 pm2.61ian 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) )
36 35 ralrimivva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) )
37 simpll 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> N e. Fin )
38 simplr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> R e. Ring )
39 simprl 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> i e. N )
40 simprr 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> j e. N )
41 eqid 
 |-  ( 1r ` C ) = ( 1r ` C )
42 2 3 12 10 5 37 38 39 40 41 pmat1ovscd 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( i ( 1r ` C ) j ) = if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) )
43 42 fveq2d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( coe1 ` ( i ( 1r ` C ) j ) ) = ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) )
44 43 fveq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) )
45 44 eqeq1d 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) <-> ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) ) )
46 45 ralbidv 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( i e. N /\ j e. N ) ) -> ( A. n e. NN ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) <-> A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) ) )
47 46 2ralbidva 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) <-> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` if ( i = j , ( ( algSc ` P ) ` ( 1r ` R ) ) , ( ( algSc ` P ) ` ( 0g ` R ) ) ) ) ` n ) = ( 0g ` R ) ) )
48 36 47 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) )
49 2 3 pmatring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
50 eqid 
 |-  ( Base ` C ) = ( Base ` C )
51 50 41 ringidcl 
 |-  ( C e. Ring -> ( 1r ` C ) e. ( Base ` C ) )
52 49 51 syl 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. ( Base ` C ) )
53 1 2 3 50 cpmatel 
 |-  ( ( N e. Fin /\ R e. Ring /\ ( 1r ` C ) e. ( Base ` C ) ) -> ( ( 1r ` C ) e. S <-> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) ) )
54 52 53 mpd3an3 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( ( 1r ` C ) e. S <-> A. i e. N A. j e. N A. n e. NN ( ( coe1 ` ( i ( 1r ` C ) j ) ) ` n ) = ( 0g ` R ) ) )
55 48 54 mpbird 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )