Theorem mat1rhmcl

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

	Ref	Expression
Hypotheses	mat1rhmval.k	$$⊢K={\mathrm{Base}}_R$$
	mat1rhmval.a	$$⊢A=\left\{E\right\}\mathrm{Mat}R$$
	mat1rhmval.b	$$⊢B={\mathrm{Base}}_A$$
	mat1rhmval.o	$$⊢O=⟨E,E⟩$$
	mat1rhmval.f	$$⊢F=\left(x\in K⟼\left\{⟨O,x⟩\right\}\right)$$
Assertion	mat1rhmcl	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to F\left(X\right)\in B$$

Proof

Step	Hyp	Ref	Expression
1		mat1rhmval.k	$$⊢K={\mathrm{Base}}_R$$
2		mat1rhmval.a	$$⊢A=\left\{E\right\}\mathrm{Mat}R$$
3		mat1rhmval.b	$$⊢B={\mathrm{Base}}_A$$
4		mat1rhmval.o	$$⊢O=⟨E,E⟩$$
5		mat1rhmval.f	$$⊢F=\left(x\in K⟼\left\{⟨O,x⟩\right\}\right)$$
6	2 1 4	mat1dimbas	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to \left\{⟨O,X⟩\right\}\in {\mathrm{Base}}_A$$
7	1 2 3 4 5	mat1rhmval	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to F\left(X\right)=\left\{⟨O,X⟩\right\}$$
8	3	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to B={\mathrm{Base}}_A$$
9	6 7 8	3eltr4d	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to F\left(X\right)\in B$$