scmatsgrp1

Description: The set of scalar matrices is a subgroup of the group/ring of diagonal matrices. (Contributed by AV, 21-Aug-2019)

	Ref	Expression
Hypotheses	scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
	scmatid.0	⊢ 0 = ( 0_g ‘ 𝑅 )
	scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
	scmatsgrp1.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
	scmatsgrp1.c	⊢ 𝐶 = ( 𝐴 ↾_s 𝐷 )
Assertion	scmatsgrp1	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		scmatid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		scmatid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		scmatid.e	⊢ 𝐸 = ( Base ‘ 𝑅 )
4		scmatid.0	⊢ 0 = ( 0_g ‘ 𝑅 )
5		scmatid.s	⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
6		scmatsgrp1.d	⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
7		scmatsgrp1.c	⊢ 𝐶 = ( 𝐴 ↾_s 𝐷 )
8	1 2 3 4 5 6	scmatdmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → 𝑥 ∈ 𝐷 ) )
9	8	ssrdv	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ 𝐷 )
10	1 2 4 6	dmatsgrp	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )
11	10	ancoms	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )
12	7	subgbas	⊢ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) → 𝐷 = ( Base ‘ 𝐶 ) )
13	12	eqcomd	⊢ ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) → ( Base ‘ 𝐶 ) = 𝐷 )
14	11 13	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( Base ‘ 𝐶 ) = 𝐷 )
15	9 14	sseqtrrd	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
16	1 2 3 4 5	scmatid	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1_r ‘ 𝐴 ) ∈ 𝑆 )
17	16	ne0d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ≠ ∅ )
18	11	adantr	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )
19	8	com12	⊢ ( 𝑥 ∈ 𝑆 → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑥 ∈ 𝐷 ) )
20	19	adantr	⊢ ( ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) → ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑥 ∈ 𝐷 ) )
21	20	impcom	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝐷 )
22	1 2 3 4 5 6	scmatdmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐷 ) )
23	22	a1d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑥 ∈ 𝑆 → ( 𝑦 ∈ 𝑆 → 𝑦 ∈ 𝐷 ) ) )
24	23	imp32	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝐷 )
25		eqid	⊢ ( -_g ‘ 𝐴 ) = ( -_g ‘ 𝐴 )
26		eqid	⊢ ( -_g ‘ 𝐶 ) = ( -_g ‘ 𝐶 )
27	25 7 26	subgsub	⊢ ( ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 ( -_g ‘ 𝐴 ) 𝑦 ) = ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) )
28	27	eqcomd	⊢ ( ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ∧ 𝑥 ∈ 𝐷 ∧ 𝑦 ∈ 𝐷 ) → ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( -_g ‘ 𝐴 ) 𝑦 ) )
29	18 21 24 28	syl3anc	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( -_g ‘ 𝐴 ) 𝑦 ) )
30	1 2 3 4 5	scmatsubcl	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( -_g ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
31	29 30	eqeltrd	⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )
32	31	ralrimivva	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )
33	1 2 4 6	dmatsrng	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
34	33	ancoms	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
35	7	subrgring	⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → 𝐶 ∈ Ring )
36	34 35	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
37		ringgrp	⊢ ( 𝐶 ∈ Ring → 𝐶 ∈ Grp )
38		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
39	38 26	issubg4	⊢ ( 𝐶 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
40	36 37 39	3syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( -_g ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
41	15 17 32 40	mpbir3and	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )

Metamath Proof Explorer

Theorem scmatsgrp1

Proof