Theorem mat1f

Description: There is a function from a ring to the ring of matrices with dimension 1 over this ring. (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	mat1f	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to F:K⟶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	1 2 3 4 5	mat1f1o	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to F:K\underset{1-1\; onto}{⟶}B$$
7		f1of	$$⊢F:K\underset{1-1\; onto}{⟶}B\to F:K⟶B$$
8	6 7	syl	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\right)\to F:K⟶B$$