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 = {Base}_{R}$
	evl1rhmlem.t	$⊢ T = R ↑_{𝑠} B$
	evl1rhmlem.f	$⊢ F = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}))$
Assertion	evls1rhmlem	$⊢ R \in CRing \to F \in ((R ↑_{𝑠} (B^{1_{𝑜}})) RingHom T)$

Proof

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

Metamath Proof Explorer

Theorem evls1rhmlem

Proof