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 ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
dmatcrng.c ⊢ 𝐶 = ( 𝐴 ↾s 𝐷 )
Assertion dmatcrng ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐶 ∈ CRing )

Proof

Step Hyp Ref Expression
1 dmatid.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2 dmatid.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
3 dmatid.0 ⊢ 0 = ( 0g ‘ 𝑅 )
4 dmatid.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5 dmatcrng.c ⊢ 𝐶 = ( 𝐴 ↾s 𝐷 )
6 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
7 1 2 3 4 dmatsrng ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
8 6 7 sylan ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
9 5 subrgring ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → 𝐶 ∈ Ring )
10 8 9 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐶 ∈ Ring )
11 simp1lr ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑅 ∈ CRing )
12 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
13 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
14 simp2 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑎 ∈ 𝑁 )
15 simp3 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑏 ∈ 𝑁 )
16 1 13 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑥 ∈ 𝐷 → 𝑥 ∈ ( Base ‘ 𝐴 ) ) )
17 16 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑥 ∈ 𝐷 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
18 17 adantrr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
19 18 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑥 ∈ ( Base ‘ 𝐴 ) )
20 1 12 13 14 15 19 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑥 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
21 1 13 3 4 dmatmat ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑦 ∈ 𝐷 → 𝑦 ∈ ( Base ‘ 𝐴 ) ) )
22 21 imp ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ 𝑦 ∈ 𝐷 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
23 22 adantrl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
24 23 3ad2ant1 ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → 𝑦 ∈ ( Base ‘ 𝐴 ) )
25 1 12 13 14 15 24 matecld ⊢ ( ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) ∧ 𝑎 ∈ 𝑁 ∧ 𝑏 ∈ 𝑁 ) → ( 𝑎 𝑦 𝑏 ) ∈ ( Base ‘ 𝑅 ) )
26 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
27 12 26 crngcom ⊢ ( ( 𝑅 ∈ CRing ∧ ( 𝑎 𝑥 𝑏 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝑎 𝑦 𝑏 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) = ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) )
28 11 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 6 anim2i ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) )
32 1 2 3 4 dmatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) ) )
33 31 32 sylan ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑥 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑦 𝑏 ) ) , 0 ) ) )
34 pm3.22 ⊢ ( ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑦 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) )
35 1 2 3 4 dmatmul ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑦 ∈ 𝐷 ∧ 𝑥 ∈ 𝐷 ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) ) )
36 31 34 35 syl2an ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) = ( 𝑎 ∈ 𝑁 , 𝑏 ∈ 𝑁 ↦ if ( 𝑎 = 𝑏 , ( ( 𝑎 𝑦 𝑏 ) ( .r ‘ 𝑅 ) ( 𝑎 𝑥 𝑏 ) ) , 0 ) ) )
37 30 33 36 3eqtr4d ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
38 37 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
39 38 ancoms ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
40 5 subrgbas ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → 𝐷 = ( Base ‘ 𝐶 ) )
41 40 eqcomd ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( Base ‘ 𝐶 ) = 𝐷 )
42 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
43 5 42 ressmulr ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝐶 ) )
44 43 eqcomd ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐶 ) = ( .r ‘ 𝐴 ) )
45 44 oveqd ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
46 44 oveqd ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) )
47 45 46 eqeq12d ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
48 41 47 raleqbidv ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
49 41 48 raleqbidv ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
50 8 49 syl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ( ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐴 ) 𝑥 ) ) )
51 39 50 mpbird ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) )
52 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
53 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
54 52 53 iscrng2 ⊢ ( 𝐶 ∈ CRing ↔ ( 𝐶 ∈ Ring ∧ ∀ 𝑥 ∈ ( Base ‘ 𝐶 ) ∀ 𝑦 ∈ ( Base ‘ 𝐶 ) ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑦 ( .r ‘ 𝐶 ) 𝑥 ) ) )
55 10 51 54 sylanbrc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑁 ∈ Fin ) → 𝐶 ∈ CRing )