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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
scmatcrng.c ⊢ 𝐶 = ( 𝐴 ↾s 𝑆 )
Assertion scmatcrng ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ CRing )

Proof

Step Hyp Ref Expression
1 scmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 scmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 scmatid.e ⊢ 𝐸 = ( Base ‘ 𝑅 )
4 scmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
5 scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6 scmatcrng.c ⊢ 𝐶 = ( 𝐴 ↾s 𝑆 )
7 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8 1 2 3 4 5 scmatsrng ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐴 ) )
9 7 8 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑆 ∈ ( SubRing ‘ 𝐴 ) )
10 6 subrgring ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → 𝐶 ∈ Ring )
11 9 10 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ Ring )
12 simp1lr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ CRing )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
15 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
16 1 13 5 scmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( Base ‘ 𝐴 ) ) )
17 16 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
18 17 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
19 18 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
20 1 3 13 14 15 19 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑥 𝑏 ) ∈ 𝐸 )
21 1 13 5 scmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( Base ‘ 𝐴 ) ) )
22 21 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
23 22 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
24 23 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
25 1 3 13 14 15 24 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑦 𝑏 ) ∈ 𝐸 )
26 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
27 3 26 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑎 𝑥 𝑏 ) ∈ 𝐸 ∧ ( 𝑎 𝑦 𝑏 ) ∈ 𝐸 ) → ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) = ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) )
28 12 20 25 27 syl3anc ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) = ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) )
29 28 ifeq1d ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) = if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) )
30 29 mpoeq3dva ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) ) )
31 7 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
32 eqid ⊢ ( 𝑁 DMat 𝑅 ) = ( 𝑁 DMat 𝑅 )
33 1 2 3 4 5 32 scmatdmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ) )
34 7 33 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ) )
35 1 2 3 4 5 32 scmatdmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ) )
36 7 35 sylan2 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ) )
37 34 36 anim12d ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ∧ 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ) ) )
38 37 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ∧ 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ) )
39 1 2 4 32 dmatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ∧ 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) ) )
40 31 38 39 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) ) )
41 38 ancomd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ∧ 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ) )
42 1 2 4 32 dmatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ ( 𝑁 DMat 𝑅 ) ∧ 𝑥 ∈ ( 𝑁 DMat 𝑅 ) ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) ) )
43 31 41 42 syl2an2r ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) ) )
44 30 40 43 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
45 44 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
46 6 subrgbas ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → 𝑆 = ( Base ‘ 𝐶 ) )
47 46 eqcomd ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( Base ‘ 𝐶 ) = 𝑆 )
48 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
49 6 48 ressmulr ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝐶 ) )
50 49 eqcomd ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐶 ) = ( .r ‘ 𝐴 ) )
51 50 oveqd ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
52 50 oveqd ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
53 51 52 eqeq12d ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
54 47 53 raleqbidv ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
55 47 54 raleqbidv ⊢ ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
56 9 55 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
57 45 56 mpbird ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
58 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
59 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
60 58 59 iscrng2 ⊢ ( 𝐶 ∈ CRing ↔ ( 𝐶 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ) )
61 11 57 60 sylanbrc ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ CRing )