Theorem scmatsrng

Description: The set of scalar matrices is a subring of the matrix ring/algebra. (Contributed by AV, 21-Aug-2019) (Revised by AV, 19-Dec-2019)

	Ref	Expression
Hypotheses	scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	scmatid.0	⊢ 0 = ( 0g ‘ 𝑅 )
	scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
Assertion	scmatsrng	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐴 ) )

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	1 2 3 4 5	scmatsgrp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐴 ) )
7	1 2 3 4 5	scmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )
8	1 2 3 4 5	scmatmulcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
9	8	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
10	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
11		eqid	⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
12		eqid	⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
13	2 11 12	issubrg2	⊢ ( 𝐴 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r ‘ 𝐴 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 ) ) )
14	10 13	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubRing ‘ 𝐴 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐴 ) ∧ ( 1r ‘ 𝐴 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 ) ) )
15	6 7 9 14	mpbir3and	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐴 ) )