Theorem scmatmat

Description: An N x N scalar matrix over (the ring) R is an N x N matrix over (the ring) R . (Contributed by AV, 18-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$$
Assertion	scmatmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in S\to M\in B\right)$$

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		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
5		eqid	$$⊢1_A=1_A$$
6		eqid	$$⊢{\cdot }_A={\cdot }_A$$
7	4 1 2 5 6 3	scmatel	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in S\leftrightarrow \left(M\in B\wedge \exists c\in {\mathrm{Base}}_{R}M=c{\cdot }_A{1}_A\right)\right)$$
8		simpl	$$⊢\left(M\in B\wedge \exists c\in {\mathrm{Base}}_{R}M=c{\cdot }_A{1}_A\right)\to M\in B$$
9	7 8	biimtrdi	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in S\to M\in B\right)$$