Metamath Proof Explorer


Theorem dmatsgrp

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

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 dmatmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑧𝐷𝑧𝐵 ) )
6 5 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑧𝐷𝑧𝐵 ) )
7 6 ssrdv ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷𝐵 )
8 1 2 3 4 dmatid ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐴 ) ∈ 𝐷 )
9 8 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 1r𝐴 ) ∈ 𝐷 )
10 9 ne0d ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ≠ ∅ )
11 1 2 3 4 dmatsubcl ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) → ( 𝑥 ( -g𝐴 ) 𝑦 ) ∈ 𝐷 )
12 11 ancom1s ( ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) ∧ ( 𝑥𝐷𝑦𝐷 ) ) → ( 𝑥 ( -g𝐴 ) 𝑦 ) ∈ 𝐷 )
13 12 ralrimivva ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( -g𝐴 ) 𝑦 ) ∈ 𝐷 )
14 1 matring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
15 14 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐴 ∈ Ring )
16 ringgrp ( 𝐴 ∈ Ring → 𝐴 ∈ Grp )
17 eqid ( -g𝐴 ) = ( -g𝐴 )
18 2 17 issubg4 ( 𝐴 ∈ Grp → ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ↔ ( 𝐷𝐵𝐷 ≠ ∅ ∧ ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( -g𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
19 15 16 18 3syl ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝐷 ∈ ( SubGrp ‘ 𝐴 ) ↔ ( 𝐷𝐵𝐷 ≠ ∅ ∧ ∀ 𝑥𝐷𝑦𝐷 ( 𝑥 ( -g𝐴 ) 𝑦 ) ∈ 𝐷 ) ) )
20 7 10 13 19 mpbir3and ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubGrp ‘ 𝐴 ) )