Theorem scmatrhmcl

Description: The value of the ring homomorphism F is a scalar matrix. (Contributed by AV, 22-Dec-2019)

	Ref	Expression
Hypotheses	scmatrhmval.k	$$⊢K={\mathrm{Base}}_R$$
	scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
	scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
	scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
	scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
	scmatrhmval.c	$$⊢C=N\mathrm{ScMat}R$$
Assertion	scmatrhmcl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to F\left(X\right)\in C$$

Proof

Step	Hyp	Ref	Expression
1		scmatrhmval.k	$$⊢K={\mathrm{Base}}_R$$
2		scmatrhmval.a	$$⊢A=N\mathrm{Mat}R$$
3		scmatrhmval.o	$$⊢\underset{\dot{}}{1}=1_A$$
4		scmatrhmval.t	$$⊢\underset{\dot{}}{\ast }={\cdot }_A$$
5		scmatrhmval.f	$$⊢F=\left(x\in K⟼x\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
6		scmatrhmval.c	$$⊢C=N\mathrm{ScMat}R$$
7	1 2 3 4 5	scmatrhmval	$$⊢\left(R\in \mathrm{Ring}\wedge X\in K\right)\to F\left(X\right)=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
8	7	3adant1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to F\left(X\right)=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
9		3simpa	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to \left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)$$
10		simp3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to X\in K$$
11	2	matring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to A\in \mathrm{Ring}$$
12	11	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to A\in \mathrm{Ring}$$
13		eqid	$$⊢{\mathrm{Base}}_A={\mathrm{Base}}_A$$
14	13 3	ringidcl	$$⊢A\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_A$$
15	12 14	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_A$$
16	1 2 13 4	matvscl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge \left(X\in K\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_A\right)\right)\to X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in {\mathrm{Base}}_A$$
17	9 10 15 16	syl12anc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in {\mathrm{Base}}_A$$
18		oveq1	$$⊢c=X\to c\underset{\dot{}}{\ast }\underset{\dot{}}{1}=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
19	18	eqeq2d	$$⊢c=X\to \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}=c\underset{\dot{}}{\ast }\underset{\dot{}}{1}\leftrightarrow X\underset{\dot{}}{\ast }\underset{\dot{}}{1}=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
20	19	adantl	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\wedge c=X\right)\to \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}=c\underset{\dot{}}{\ast }\underset{\dot{}}{1}\leftrightarrow X\underset{\dot{}}{\ast }\underset{\dot{}}{1}=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)$$
21		eqidd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to X\underset{\dot{}}{\ast }\underset{\dot{}}{1}=X\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
22	10 20 21	rspcedvd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to \exists c\in KX\underset{\dot{}}{\ast }\underset{\dot{}}{1}=c\underset{\dot{}}{\ast }\underset{\dot{}}{1}$$
23	1 2 13 3 4 6	scmatel	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in C\leftrightarrow \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in {\mathrm{Base}}_A\wedge \exists c\in KX\underset{\dot{}}{\ast }\underset{\dot{}}{1}=c\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$
24	23	3adant3	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in C\leftrightarrow \left(X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in {\mathrm{Base}}_A\wedge \exists c\in KX\underset{\dot{}}{\ast }\underset{\dot{}}{1}=c\underset{\dot{}}{\ast }\underset{\dot{}}{1}\right)\right)$$
25	17 22 24	mpbir2and	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to X\underset{\dot{}}{\ast }\underset{\dot{}}{1}\in C$$
26	8 25	eqeltrd	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge X\in K\right)\to F\left(X\right)\in C$$