Theorem scmatsgrp

Description: The set of scalar matrices is a subgroup of the matrix group/algebra. (Contributed by AV, 20-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	scmatsgrp	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐴 ) )

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 5	scmatmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑧 ∈ 𝑆 → 𝑧 ∈ 𝐵 ) )
7	6	ssrdv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ 𝐵 )
8	1 2 3 4 5	scmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )
9	8	ne0d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ≠ ∅ )
10	1 2 3 4 5	scmatsubcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
11	10	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
12	1	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
13		ringgrp	⊢ ( 𝐴 ∈ Ring → 𝐴 ∈ Grp )
14		eqid	⊢ ( -g ‘ 𝐴 ) = ( -g ‘ 𝐴 )
15	2 14	issubg4	⊢ ( 𝐴 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐴 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 ) ) )
16	12 13 15	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐴 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 ) ) )
17	7 9 11 16	mpbir3and	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐴 ) )