Theorem dmatsrng

Description: The set of diagonal matrices is a subring of the matrix ring/algebra. (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 𝑅 )
Assertion	dmatsrng	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		dmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		dmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		dmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		dmatid.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
5	1 2 3 4	dmatsgrp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )
6	1 2 3 4	dmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝐷 )
7	6	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 1r ‘ 𝐴 ) ∈ 𝐷 )
8	1 2 3 4	dmatmulcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐷 )
9	8	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐷 )
10	9	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐷 )
11	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
12	11	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐴 ∈ Ring )
13		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
14		eqid	⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
15	2 13 14	issubrg2	⊢ ( 𝐴 ∈ Ring → ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r ‘ 𝐴 ) ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
16	12 15	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r ‘ 𝐴 ) ∈ 𝐷 ∧ ∀ 𝑥 ∈ 𝐷 ∀ 𝑦 ∈ 𝐷 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
17	5 7 10 16	mpbir3and	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )