Theorem scmatel

Description: An N x N scalar matrix over (a ring) R . (Contributed 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	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)$$

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	scmatval	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to S=\left\{m\in B|\exists c\in Km=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right\}$$
8	7	eleq2d	$$⊢\left(N\in \mathrm{Fin}\wedge R\in V\right)\to \left(M\in S\leftrightarrow M\in \left\{m\in B|\exists c\in Km=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right\}\right)$$
9		eqeq1	$$⊢m=M\to \left(m=c\underset{\dot{}}{·}\underset{\dot{}}{1}\leftrightarrow M=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
10	9	rexbidv	$$⊢m=M\to \left(\exists c\in Km=c\underset{\dot{}}{·}\underset{\dot{}}{1}\leftrightarrow \exists c\in KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
11	10	elrab	$$⊢M\in \left\{m\in B|\exists c\in Km=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right\}\leftrightarrow \left(M\in B\wedge \exists c\in KM=c\underset{\dot{}}{·}\underset{\dot{}}{1}\right)$$
12	8 11	bitrdi	$$⊢\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)$$