Theorem evls1rhmlem

Description: Lemma for evl1rhm and evls1rhm (formerly part of the proof of evl1rhm ): The first function of the composition forming the univariate polynomial evaluation map function for a (sub)ring is a ring homomorphism. (Contributed by AV, 11-Sep-2019)

	Ref	Expression
Hypotheses	evl1rhmlem.b	$$⊢B={\mathrm{Base}}_R$$
	evl1rhmlem.t	$$⊢T=R{\uparrow }_{𝑠}B$$
	evl1rhmlem.f	$$⊢F=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
Assertion	evls1rhmlem	$$⊢R\in \mathrm{CRing}\to F\in \left(\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\mathrm{RingHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		evl1rhmlem.b	$$⊢B={\mathrm{Base}}_R$$
2		evl1rhmlem.t	$$⊢T=R{\uparrow }_{𝑠}B$$
3		evl1rhmlem.f	$$⊢F=\left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
4		ovex	$$⊢B^{1_{𝑜}}\in \mathrm{V}$$
5		eqid	$$⊢R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)=R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)$$
6	5 1	pwsbas	$$⊢\left(R\in \mathrm{CRing}\wedge B^{1_{𝑜}}\in \mathrm{V}\right)\to B^{\left(B^{1_{𝑜}}\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
7	4 6	mpan2	$$⊢R\in \mathrm{CRing}\to B^{\left(B^{1_{𝑜}}\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
8	7	mpteq1d	$$⊢R\in \mathrm{CRing}\to \left(x\in \left(B^{\left(B^{1_{𝑜}}\right)}\right)⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)=\left(x\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
9	3 8	eqtrid	$$⊢R\in \mathrm{CRing}\to F=\left(x\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)$$
10		eqid	$$⊢{\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}={\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}$$
11		crngring	$$⊢R\in \mathrm{CRing}\to R\in \mathrm{Ring}$$
12	1	fvexi	$$⊢B\in \mathrm{V}$$
13	12	a1i	$$⊢R\in \mathrm{CRing}\to B\in \mathrm{V}$$
14	4	a1i	$$⊢R\in \mathrm{CRing}\to B^{1_{𝑜}}\in \mathrm{V}$$
15		df1o2	$$⊢1_{𝑜}=\left\{\varnothing \right\}$$
16		0ex	$$⊢\varnothing \in \mathrm{V}$$
17		eqid	$$⊢\left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)=\left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)$$
18	15 12 16 17	mapsnf1o3	$$⊢\left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right):B\underset{1-1\; onto}{⟶}{B}^{1_{𝑜}}$$
19		f1of	$$⊢\left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right):B\underset{1-1\; onto}{⟶}{B}^{1_{𝑜}}\to \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right):B⟶B^{1_{𝑜}}$$
20	18 19	mp1i	$$⊢R\in \mathrm{CRing}\to \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right):B⟶B^{1_{𝑜}}$$
21	2 5 10 11 13 14 20	pwsco1rhm	$$⊢R\in \mathrm{CRing}\to \left(x\in {\mathrm{Base}}_{\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)}⟼x\circ \left(y\in B⟼1_{𝑜}\times \left\{y\right\}\right)\right)\in \left(\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\mathrm{RingHom}T\right)$$
22	9 21	eqeltrd	$$⊢R\in \mathrm{CRing}\to F\in \left(\left(R{\uparrow }_{𝑠}\left(B^{1_{𝑜}}\right)\right)\mathrm{RingHom}T\right)$$