Metamath Proof Explorer

Theorem scmatcrng

Description: The subring of scalar matrices (over a commutative ring) is a commutative ring. (Contributed by AV, 21-Aug-2019)

Ref Expression
Hypotheses scmatid.a 
|- A = ( N Mat R )
scmatid.b 
|- B = ( Base ` A )
scmatid.e 
|- E = ( Base ` R )
scmatid.0 
|- .0. = ( 0g ` R )
scmatid.s 
|- S = ( N ScMat R )
scmatcrng.c 
|- C = ( A |`s S )
Assertion scmatcrng 
|- ( ( N e. Fin /\ R e. CRing ) -> C e. CRing )

Proof

Step Hyp Ref Expression
1 scmatid.a 
 |-  A = ( N Mat R )
2 scmatid.b 
 |-  B = ( Base ` A )
3 scmatid.e 
 |-  E = ( Base ` R )
4 scmatid.0 
 |-  .0. = ( 0g ` R )
5 scmatid.s 
 |-  S = ( N ScMat R )
6 scmatcrng.c 
 |-  C = ( A |`s S )
7 crngring 
 |-  ( R e. CRing -> R e. Ring )
8 1 2 3 4 5 scmatsrng 
 |-  ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` A ) )
9 7 8 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> S e. ( SubRing ` A ) )
10 6 subrgring 
 |-  ( S e. ( SubRing ` A ) -> C e. Ring )
11 9 10 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. Ring )
12 simp1lr 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> R e. CRing )
13 eqid 
 |-  ( Base ` A ) = ( Base ` A )
14 simp2 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> a e. N )
15 simp3 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> b e. N )
16 1 13 5 scmatmat 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( x e. S -> x e. ( Base ` A ) ) )
17 16 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ x e. S ) -> x e. ( Base ` A ) )
18 17 adantrr 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> x e. ( Base ` A ) )
19 18 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> x e. ( Base ` A ) )
20 1 3 13 14 15 19 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> ( a x b ) e. E )
21 1 13 5 scmatmat 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( y e. S -> y e. ( Base ` A ) ) )
22 21 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ y e. S ) -> y e. ( Base ` A ) )
23 22 adantrl 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> y e. ( Base ` A ) )
24 23 3ad2ant1 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> y e. ( Base ` A ) )
25 1 3 13 14 15 24 matecld 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ a e. N /\ b e. N ) -> ( a y b ) e. E )
26 eqid 
 |-  ( .r ` R ) = ( .r ` R )
27 3 26 crngcom 
 |-  ( ( R e. CRing /\ ( a x b ) e. E /\ ( a y b ) e. E ) -> ( ( a x b ) ( .r ` R ) ( a y b ) ) = ( ( a y b ) ( .r ` R ) ( a x b ) ) )
28 12 20 25 27 syl3anc 
 |-  ( ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) /\ 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. S /\ y e. S ) ) /\ 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. S /\ y e. S ) ) -> ( 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 7 anim2i 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( N e. Fin /\ R e. Ring ) )
32 eqid 
 |-  ( N DMat R ) = ( N DMat R )
33 1 2 3 4 5 32 scmatdmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( x e. S -> x e. ( N DMat R ) ) )
34 7 33 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( x e. S -> x e. ( N DMat R ) ) )
35 1 2 3 4 5 32 scmatdmat 
 |-  ( ( N e. Fin /\ R e. Ring ) -> ( y e. S -> y e. ( N DMat R ) ) )
36 7 35 sylan2 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( y e. S -> y e. ( N DMat R ) ) )
37 34 36 anim12d 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( ( x e. S /\ y e. S ) -> ( x e. ( N DMat R ) /\ y e. ( N DMat R ) ) ) )
38 37 imp 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> ( x e. ( N DMat R ) /\ y e. ( N DMat R ) ) )
39 1 2 4 32 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( x e. ( N DMat R ) /\ y e. ( N DMat R ) ) ) -> ( x ( .r ` A ) y ) = ( a e. N , b e. N |-> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) ) )
40 31 38 39 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` A ) y ) = ( a e. N , b e. N |-> if ( a = b , ( ( a x b ) ( .r ` R ) ( a y b ) ) , .0. ) ) )
41 38 ancomd 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> ( y e. ( N DMat R ) /\ x e. ( N DMat R ) ) )
42 1 2 4 32 dmatmul 
 |-  ( ( ( N e. Fin /\ R e. Ring ) /\ ( y e. ( N DMat R ) /\ x e. ( N DMat R ) ) ) -> ( y ( .r ` A ) x ) = ( a e. N , b e. N |-> if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) ) )
43 31 41 42 syl2an2r 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> ( y ( .r ` A ) x ) = ( a e. N , b e. N |-> if ( a = b , ( ( a y b ) ( .r ` R ) ( a x b ) ) , .0. ) ) )
44 30 40 43 3eqtr4d 
 |-  ( ( ( N e. Fin /\ R e. CRing ) /\ ( x e. S /\ y e. S ) ) -> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
45 44 ralrimivva 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. x e. S A. y e. S ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) )
46 6 subrgbas 
 |-  ( S e. ( SubRing ` A ) -> S = ( Base ` C ) )
47 46 eqcomd 
 |-  ( S e. ( SubRing ` A ) -> ( Base ` C ) = S )
48 eqid 
 |-  ( .r ` A ) = ( .r ` A )
49 6 48 ressmulr 
 |-  ( S e. ( SubRing ` A ) -> ( .r ` A ) = ( .r ` C ) )
50 49 eqcomd 
 |-  ( S e. ( SubRing ` A ) -> ( .r ` C ) = ( .r ` A ) )
51 50 oveqd 
 |-  ( S e. ( SubRing ` A ) -> ( x ( .r ` C ) y ) = ( x ( .r ` A ) y ) )
52 50 oveqd 
 |-  ( S e. ( SubRing ` A ) -> ( y ( .r ` C ) x ) = ( y ( .r ` A ) x ) )
53 51 52 eqeq12d 
 |-  ( S e. ( SubRing ` A ) -> ( ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
54 47 53 raleqbidv 
 |-  ( S e. ( SubRing ` A ) -> ( A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. y e. S ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
55 47 54 raleqbidv 
 |-  ( S e. ( SubRing ` A ) -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. x e. S A. y e. S ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
56 9 55 syl 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) <-> A. x e. S A. y e. S ( x ( .r ` A ) y ) = ( y ( .r ` A ) x ) ) )
57 45 56 mpbird 
 |-  ( ( N e. Fin /\ R e. CRing ) -> A. x e. ( Base ` C ) A. y e. ( Base ` C ) ( x ( .r ` C ) y ) = ( y ( .r ` C ) x ) )
58 eqid 
 |-  ( Base ` C ) = ( Base ` C )
59 eqid 
 |-  ( .r ` C ) = ( .r ` C )
60 58 59 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 ) ) )
61 11 57 60 sylanbrc 
 |-  ( ( N e. Fin /\ R e. CRing ) -> C e. CRing )