Metamath Proof Explorer

Theorem dmatcrng

Description: The subring of diagonal matrices (over a commutative ring) is a commutative ring . (Contributed by AV, 20-Aug-2019) (Revised by AV, 18-Dec-2019)

Ref Expression
Hypotheses dmatid.a 
|- A = ( N Mat R )
dmatid.b 
|- B = ( Base ` A )
dmatid.0 
|- .0. = ( 0g ` R )
dmatid.d 
|- D = ( N DMat R )
dmatcrng.c 
|- C = ( A |`s D )
Assertion dmatcrng 
|- ( ( R e. CRing /\ N e. Fin ) -> C e. CRing )

Proof

Step Hyp Ref Expression
1 dmatid.a 
 |-  A = ( N Mat R )
2 dmatid.b 
 |-  B = ( Base ` A )
3 dmatid.0 
 |-  .0. = ( 0g ` R )
4 dmatid.d 
 |-  D = ( N DMat R )
5 dmatcrng.c 
 |-  C = ( A |`s D )
6 crngring 
 |-  ( R e. CRing -> R e. Ring )
7 1 2 3 4 dmatsrng 
 |-  ( ( R e. Ring /\ N e. Fin ) -> D e. ( SubRing ` A ) )
8 6 7 sylan 
 |-  ( ( R e. CRing /\ N e. Fin ) -> D e. ( SubRing ` A ) )
9 5 subrgring 
 |-  ( D e. ( SubRing ` A ) -> C e. Ring )
10 8 9 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> C e. Ring )
11 simp1lr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> R e. CRing )
12 eqid 
 |-  ( Base ` R ) = ( Base ` R )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> a e. N )
15 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> b e. N )
16 1 13 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( x e. D -> x e. ( Base ` A ) ) )
17 16 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ x e. D ) -> x e. ( Base ` A ) )
18 17 adantrr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> x e. ( Base ` A ) )
19 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> x e. ( Base ` A ) )
20 1 12 13 14 15 19 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> ( a x b ) e. ( Base ` R ) )
21 1 13 3 4 dmatmat 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( y e. D -> y e. ( Base ` A ) ) )
22 21 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ y e. D ) -> y e. ( Base ` A ) )
23 22 adantrl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> y e. ( Base ` A ) )
24 23 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> y e. ( Base ` A ) )
25 1 12 13 14 15 24 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> ( a y b ) e. ( Base ` R ) )
26 eqid 
 |-  ( .r ` R ) = ( .r ` R )
27 12 26 crngcom 
 |-  ( ( R e. CRing /\ ( a x b ) e. ( Base ` R ) /\ ( a y b ) e. ( Base ` R ) ) -> ( ( a x b ) ( .r ` R ) ( a y b ) ) = ( ( a y b ) ( .r ` R ) ( a x b ) ) )
28 11 20 25 27 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> ( ( a x b ) ( .r ` R ) ( a y b ) ) = ( ( a y b ) ( .r ` R ) ( a x b ) ) )
29 28 ifeq1d 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) /\ a e. N /\ b e. N ) -> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) = if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) )
30 29 mpoeq3dva 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> ( a e. N , b e. N |-> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) ) = ( a e. N , b e. N |-> if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) ) )
31 6 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
32 1 2 3 4 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` A ) y ) = ( a e. N , b e. N |-> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) ) )
33 31 32 sylan 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` A ) y ) = ( a e. N , b e. N |-> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) ) )
34 pm3.22 
 |-  ( ( x e. D /\ y e. D ) -> ( y e. D /\ x e. D ) )
35 1 2 3 4 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. D /\ x e. D ) ) -> ( y ( .r ` A ) x ) = ( a e. N , b e. N |-> if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) ) )
36 31 34 35 syl2an 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> ( y ( .r ` A ) x ) = ( a e. N , b e. N |-> if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) ) )
37 30 33 36 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. D /\ y e. D ) ) -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
38 37 ralrimivva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
39 38 ancoms 
 |-  ( ( R e. CRing /\ N e. Fin ) -> A. x e. D A. y e. D ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
40 5 subrgbas 
 |-  ( D e. ( SubRing ` A ) -> D = ( Base ` C ) )
41 40 eqcomd 
 |-  ( D e. ( SubRing ` A ) -> ( Base ` C ) = D )
42 eqid 
 |-  ( .r ` A ) = ( .r ` A )
43 5 42 ressmulr 
 |-  ( D e. ( SubRing ` A ) -> ( .r ` A ) = ( .r ` C ) )
44 43 eqcomd 
 |-  ( D e. ( SubRing ` A ) -> ( .r ` C ) = ( .r ` A ) )
45 44 oveqd 
 |-  ( D e. ( SubRing ` A ) -> ( x ( .r ` C ) y ) = ( x ( .r ` A ) y ) )
46 44 oveqd 
 |-  ( D e. ( SubRing ` A ) -> ( y ( .r ` C ) x ) = ( y ( .r ` A ) x ) )
47 45 46 eqeq12d 
 |-  ( D e. ( SubRing ` A ) -> ( ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
48 41 47 raleqbidv 
 |-  ( D e. ( SubRing ` A ) -> ( A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. y e. D ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
49 41 48 raleqbidv 
 |-  ( D e. ( SubRing ` A ) -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. x e. D A. y e. D ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
50 8 49 syl 
 |-  ( ( R e. CRing /\ N e. Fin ) -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. x e. D A. y e. D ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
51 39 50 mpbird 
 |-  ( ( R e. CRing /\ N e. Fin ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
52 eqid 
 |-  ( Base ` C ) = ( Base ` C )
53 eqid 
 |-  ( .r ` C ) = ( .r ` C )
54 52 53 iscrng2 
 |-  ( C e. CRing <-> ( C e. Ring /\ A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) ) )
55 10 51 54 sylanbrc 
 |-  ( ( R e. CRing /\ N e. Fin ) -> C e. CRing )