Metamath Proof Explorer

Theorem scmatsrng1

Description: The set of scalar matrices is a subring of the 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 = ( 0g ‘ 𝑅 )
scmatid.s ⊢ 𝑆 = ( 𝑁 ScMat 𝑅 )
scmatsgrp1.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
scmatsgrp1.c ⊢ 𝐶 = ( 𝐴 ↾s 𝐷 )
Assertion scmatsrng1 ( ( 𝑁 ∈ 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 scmatsgrp1.d ⊢ 𝐷 = ( 𝑁 DMat 𝑅 )
7 scmatsgrp1.c ⊢ 𝐶 = ( 𝐴 ↾s 𝐷 )
8 1 2 3 4 5 6 7 scmatsgrp1 ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )
9 1 2 4 6 dmatsrng ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
10 9 ancoms ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐷 ∈ ( SubRing ‘ 𝐴 ) )
11 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
12 7 11 subrg1 ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐶 ) )
13 10 12 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐶 ) )
14 13 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐴 ) )
15 1 2 3 4 5 scmatid ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐴 ) ∈ 𝑆 )
16 14 15 eqeltrd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r ‘ 𝐶 ) ∈ 𝑆 )
17 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
18 7 17 ressmulr ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝐶 ) )
19 10 18 syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( .r ‘ 𝐴 ) = ( .r ‘ 𝐶 ) )
20 19 eqcomd ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( .r ‘ 𝐶 ) = ( .r ‘ 𝐴 ) )
21 20 oveqdr ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) = ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) )
22 1 2 3 4 5 scmatmulcl ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐴 ) 𝑦 ) ∈ 𝑆 )
23 21 22 eqeltrd ⊢ ( ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )
24 23 ralrimivva ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 )
25 7 subrgring ⊢ ( 𝐷 ∈ ( SubRing ‘ 𝐴 ) → 𝐶 ∈ Ring )
26 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
27 eqid ⊢ ( 1r ‘ 𝐶 ) = ( 1r ‘ 𝐶 )
28 eqid ⊢ ( .r ‘ 𝐶 ) = ( .r ‘ 𝐶 )
29 26 27 28 issubrg2 ⊢ ( 𝐶 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 1r ‘ 𝐶 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
30 10 25 29 3syl ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 1r ‘ 𝐶 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( .r ‘ 𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
31 8 16 24 30 mpbir3and ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐶 ) )