Theorem mat1rhmval

Description: The value of the ring homomorphism F . (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	mat1rhmval	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to F\left(X\right)=\left\{⟨O,X⟩\right\}$$

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		opeq2	$$⊢x=X\to ⟨O,x⟩=⟨O,X⟩$$
7	6	sneqd	$$⊢x=X\to \left\{⟨O,x⟩\right\}=\left\{⟨O,X⟩\right\}$$
8		simp3	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to X\in K$$
9		snex	$$⊢\left\{⟨O,X⟩\right\}\in \mathrm{V}$$
10	9	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to \left\{⟨O,X⟩\right\}\in \mathrm{V}$$
11	5 7 8 10	fvmptd3	$$⊢\left(R\in \mathrm{Ring}\wedge E\in V\wedge X\in K\right)\to F\left(X\right)=\left\{⟨O,X⟩\right\}$$