evl1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by Mario Carneiro, 12-Jun-2015) (Proof shortened by AV, 13-Sep-2019)

	Ref	Expression
Hypotheses	evl1rhm.q	$⊢ O = {eval}_{1} (R)$
	evl1rhm.w	$⊢ P = {Poly}_{1} (R)$
	evl1rhm.t	$⊢ T = R ↑_{𝑠} B$
	evl1rhm.b	$⊢ B = {Base}_{R}$
Assertion	evl1rhm	$⊢ R \in CRing \to O \in (P RingHom T)$

Proof

Step	Hyp	Ref	Expression
1		evl1rhm.q	$⊢ O = {eval}_{1} (R)$
2		evl1rhm.w	$⊢ P = {Poly}_{1} (R)$
3		evl1rhm.t	$⊢ T = R ↑_{𝑠} B$
4		evl1rhm.b	$⊢ B = {Base}_{R}$
5		eqid	$⊢ 1_{𝑜} eval R = 1_{𝑜} eval R$
6	1 5 4	evl1fval	$⊢ O = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R)$
7		eqid	$⊢ (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\}))$
8	4 3 7	evls1rhmlem	$⊢ R \in CRing \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in ((R ↑_{𝑠} (B^{1_{𝑜}})) RingHom T)$
9		1on	$⊢ 1_{𝑜} \in On$
10		eqid	$⊢ 1_{𝑜} mPoly R = 1_{𝑜} mPoly R$
11		eqid	$⊢ R ↑_{𝑠} (B^{1_{𝑜}}) = R ↑_{𝑠} (B^{1_{𝑜}})$
12	5 4 10 11	evlrhm	$⊢ (1_{𝑜} \in On \land R \in CRing) \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
13	9 12	mpan	$⊢ R \in CRing \to 1_{𝑜} eval R \in ((1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
14		eqidd	$⊢ R \in CRing \to {Base}_{P} = {Base}_{P}$
15		eqidd	$⊢ R \in CRing \to {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))}$
16		eqid	$⊢ {PwSer}_{1} (R) = {PwSer}_{1} (R)$
17		eqid	$⊢ {Base}_{P} = {Base}_{P}$
18	2 16 17	ply1bas	$⊢ {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
19	18	a1i	$⊢ R \in CRing \to {Base}_{P} = {Base}_{(1_{𝑜} mPoly R)}$
20		eqid	$⊢ +_{P} = +_{P}$
21	2 10 20	ply1plusg	$⊢ +_{P} = +_{(1_{𝑜} mPoly R)}$
22	21	a1i	$⊢ R \in CRing \to +_{P} = +_{(1_{𝑜} mPoly R)}$
23	22	oveqdr	$⊢ (R \in CRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x +_{P} y = x +_{(1_{𝑜} mPoly R)} y$
24		eqidd	$⊢ (R \in CRing \land (x \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \land y \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))})) \to x +_{(R ↑_{𝑠} (B^{1_{𝑜}}))} y = x +_{(R ↑_{𝑠} (B^{1_{𝑜}}))} y$
25		eqid	$⊢ \cdot_{P} = \cdot_{P}$
26	2 10 25	ply1mulr	$⊢ \cdot_{P} = \cdot_{(1_{𝑜} mPoly R)}$
27	26	a1i	$⊢ R \in CRing \to \cdot_{P} = \cdot_{(1_{𝑜} mPoly R)}$
28	27	oveqdr	$⊢ (R \in CRing \land (x \in {Base}_{P} \land y \in {Base}_{P})) \to x \cdot_{P} y = x \cdot_{(1_{𝑜} mPoly R)} y$
29		eqidd	$⊢ (R \in CRing \land (x \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))} \land y \in {Base}_{(R ↑_{𝑠} (B^{1_{𝑜}}))})) \to x \cdot_{(R ↑_{𝑠} (B^{1_{𝑜}}))} y = x \cdot_{(R ↑_{𝑠} (B^{1_{𝑜}}))} y$
30	14 15 19 15 23 24 28 29	rhmpropd	$⊢ R \in CRing \to P RingHom (R ↑_{𝑠} (B^{1_{𝑜}})) = (1_{𝑜} mPoly R) RingHom (R ↑_{𝑠} (B^{1_{𝑜}}))$
31	13 30	eleqtrrd	$⊢ R \in CRing \to 1_{𝑜} eval R \in (P RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))$
32		rhmco	$⊢ ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in ((R ↑_{𝑠} (B^{1_{𝑜}})) RingHom T) \land 1_{𝑜} eval R \in (P RingHom (R ↑_{𝑠} (B^{1_{𝑜}})))) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R) \in (P RingHom T)$
33	8 31 32	syl2anc	$⊢ R \in CRing \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} eval R) \in (P RingHom T)$
34	6 33	eqeltrid	$⊢ R \in CRing \to O \in (P RingHom T)$

Metamath Proof Explorer

Theorem evl1rhm

Proof