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 ‘ 𝐴 ) )