Theorem scmatstrbas

Description: The set of scalar matrices is the base set of the ring of corresponding scalar matrices. (Contributed by AV, 26-Dec-2019)

	Ref	Expression
Hypotheses	scmatstrbas.a	$$⊢A=N\mathrm{Mat}R$$
	scmatstrbas.c	$$⊢C=N\mathrm{ScMat}R$$
	scmatstrbas.s	$$⊢S=A{\upharpoonright }_{𝑠}C$$
Assertion	scmatstrbas	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to {\mathrm{Base}}_S=C$$

Proof

Step	Hyp	Ref	Expression
1		scmatstrbas.a	$$⊢A=N\mathrm{Mat}R$$
2		scmatstrbas.c	$$⊢C=N\mathrm{ScMat}R$$
3		scmatstrbas.s	$$⊢S=A{\upharpoonright }_{𝑠}C$$
4		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_A$$
5		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
6		eqid	$$⊢0_R=0_R$$
7	1 4 5 6 2	scmatsrng	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to C\in \mathrm{SubRing}\left(A\right)$$
8	3	subrgbas	$$⊢C\in \mathrm{SubRing}\left(A\right)\to C={\mathrm{Base}}_S$$
9	8	eqcomd	$$⊢C\in \mathrm{SubRing}\left(A\right)\to {\mathrm{Base}}_S=C$$
10	7 9	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to {\mathrm{Base}}_S=C$$