# Metamath Proof Explorer

## Theorem scmatmats

Description: The set of an N x N scalar matrices over the ring R expressed as a subset of N x N matrices over the ring R with certain properties for their entries. (Contributed by AV, 31-Oct-2019) (Revised by AV, 19-Dec-2019)

Ref Expression
Hypotheses scmatmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
scmatmat.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
scmatmat.s ${⊢}{S}={N}\mathrm{ScMat}{R}$
scmate.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
scmate.0
Assertion scmatmats

### Proof

Step Hyp Ref Expression
1 scmatmat.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 scmatmat.b ${⊢}{B}={\mathrm{Base}}_{{A}}$
3 scmatmat.s ${⊢}{S}={N}\mathrm{ScMat}{R}$
4 scmate.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
5 scmate.0
6 eqid ${⊢}{1}_{{A}}={1}_{{A}}$
7 eqid ${⊢}{\cdot }_{{A}}={\cdot }_{{A}}$
8 4 1 2 6 7 3 scmatval ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {S}=\left\{{m}\in {B}|\exists {c}\in {K}\phantom{\rule{.4em}{0ex}}{m}={c}{\cdot }_{{A}}{1}_{{A}}\right\}$
9 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\to {m}\in {B}$
10 9 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to {m}\in {B}$
11 simpll ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
12 1 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
13 2 6 ringidcl ${⊢}{A}\in \mathrm{Ring}\to {1}_{{A}}\in {B}$
14 12 13 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {1}_{{A}}\in {B}$
15 14 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\to {1}_{{A}}\in {B}$
16 15 anim1ci ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to \left({c}\in {K}\wedge {1}_{{A}}\in {B}\right)$
17 4 1 2 7 matvscl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({c}\in {K}\wedge {1}_{{A}}\in {B}\right)\right)\to {c}{\cdot }_{{A}}{1}_{{A}}\in {B}$
18 11 16 17 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to {c}{\cdot }_{{A}}{1}_{{A}}\in {B}$
19 1 2 eqmat ${⊢}\left({m}\in {B}\wedge {c}{\cdot }_{{A}}{1}_{{A}}\in {B}\right)\to \left({m}={c}{\cdot }_{{A}}{1}_{{A}}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}={i}\left({c}{\cdot }_{{A}}{1}_{{A}}\right){j}\right)$
20 10 18 19 syl2anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to \left({m}={c}{\cdot }_{{A}}{1}_{{A}}↔\forall {i}\in {N}\phantom{\rule{.4em}{0ex}}\forall {j}\in {N}\phantom{\rule{.4em}{0ex}}{i}{m}{j}={i}\left({c}{\cdot }_{{A}}{1}_{{A}}\right){j}\right)$
21 simplll ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to {N}\in \mathrm{Fin}$
22 simpllr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to {R}\in \mathrm{Ring}$
23 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to {c}\in {K}$
24 21 22 23 3jca ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge {m}\in {B}\right)\wedge {c}\in {K}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {c}\in {K}\right)$
25 1 4 5 6 7 scmatscmide
26 24 25 sylan
27 26 eqeq2d
28 27 2ralbidva
29 20 28 bitrd
30 29 rexbidva
31 30 rabbidva
32 8 31 eqtrd