Theorem scmatscmid

Description: A scalar matrix can be expressed as a multiplication of a scalar with the identity matrix. (Contributed by AV, 30-Oct-2019) (Revised by AV, 18-Dec-2019)

	Ref	Expression
Hypotheses	scmatval.k	$$⊢K={\mathrm{Base}}_R$$
	scmatval.a	$$⊢A=N\mathrm{Mat}R$$
	scmatval.b	$$⊢B={\mathrm{Base}}_A$$
	scmatval.1	$$⊢\underset{\dot{}}{1}=1_A$$
	scmatval.t	$$⊢\underset{\dot{}}{·}={\cdot }_A$$
	scmatval.s	$$⊢S=N\mathrm{ScMat}R$$
Assertion	scmatscmid	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in S\right)\to \exists c\in KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		scmatval.k	$$⊢K={\mathrm{Base}}_R$$
2		scmatval.a	$$⊢A=N\mathrm{Mat}R$$
3		scmatval.b	$$⊢B={\mathrm{Base}}_A$$
4		scmatval.1	$$⊢\underset{\dot{}}{1}=1_A$$
5		scmatval.t	$$⊢\underset{\dot{}}{·}={\cdot }_A$$
6		scmatval.s	$$⊢S=N\mathrm{ScMat}R$$
7	1 2 3 4 5 6	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 KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right)\right)$$
8	7	simplbda	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in V\right)\wedge M\in S\right)\to \exists c\in KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}$$
9	8	3impa	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\wedge M\in S\right)\to \exists c\in KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}$$