evls1rhm

Description: Polynomial evaluation is a homomorphism (into the product ring). (Contributed by AV, 11-Sep-2019)

	Ref	Expression
Hypotheses	evls1rhm.q	$⊢ Q = S {evalSub}_{1} R$
	evls1rhm.b	$⊢ B = {Base}_{S}$
	evls1rhm.t	$⊢ T = S ↑_{𝑠} B$
	evls1rhm.u	$⊢ U = S ↾_{𝑠} R$
	evls1rhm.w	$⊢ W = {Poly}_{1} (U)$
Assertion	evls1rhm	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom T)$

Proof

Step	Hyp	Ref	Expression
1		evls1rhm.q	$⊢ Q = S {evalSub}_{1} R$
2		evls1rhm.b	$⊢ B = {Base}_{S}$
3		evls1rhm.t	$⊢ T = S ↑_{𝑠} B$
4		evls1rhm.u	$⊢ U = S ↾_{𝑠} R$
5		evls1rhm.w	$⊢ W = {Poly}_{1} (U)$
6	2	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
7	6	adantl	$⊢ (S \in CRing \land R \in SubRing (S)) \to R \subseteq B$
8		elpwg	$⊢ R \in SubRing (S) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
9	8	adantl	$⊢ (S \in CRing \land R \in SubRing (S)) \to (R \in 𝒫 B \leftrightarrow R \subseteq B)$
10	7 9	mpbird	$⊢ (S \in CRing \land R \in SubRing (S)) \to R \in 𝒫 B$
11		eqid	$⊢ 1_{𝑜} evalSub S = 1_{𝑜} evalSub S$
12	1 11 2	evls1fval	$⊢ (S \in CRing \land R \in 𝒫 B) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)$
13	10 12	syldan	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q = (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R)$
14		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\}))$
15	2 3 14	evls1rhmlem	$⊢ S \in CRing \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in ((S ↑_{𝑠} (B^{1_{𝑜}})) RingHom T)$
16		1on	$⊢ 1_{𝑜} \in On$
17		eqid	$⊢ (1_{𝑜} evalSub S) (R) = (1_{𝑜} evalSub S) (R)$
18		eqid	$⊢ 1_{𝑜} mPoly U = 1_{𝑜} mPoly U$
19		eqid	$⊢ S ↑_{𝑠} (B^{1_{𝑜}}) = S ↑_{𝑠} (B^{1_{𝑜}})$
20	17 18 4 19 2	evlsrhm	$⊢ (1_{𝑜} \in On \land S \in CRing \land R \in SubRing (S)) \to (1_{𝑜} evalSub S) (R) \in ((1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
21	16 20	mp3an1	$⊢ (S \in CRing \land R \in SubRing (S)) \to (1_{𝑜} evalSub S) (R) \in ((1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
22		eqidd	$⊢ (S \in CRing \land R \in SubRing (S)) \to {Base}_{W} = {Base}_{W}$
23		eqidd	$⊢ (S \in CRing \land R \in SubRing (S)) \to {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} = {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))}$
24		eqid	$⊢ {PwSer}_{1} (U) = {PwSer}_{1} (U)$
25		eqid	$⊢ {Base}_{W} = {Base}_{W}$
26	5 24 25	ply1bas	$⊢ {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
27	26	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
28		eqid	$⊢ +_{W} = +_{W}$
29	5 18 28	ply1plusg	$⊢ +_{W} = +_{(1_{𝑜} mPoly U)}$
30	29	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to +_{W} = +_{(1_{𝑜} mPoly U)}$
31	30	oveqdr	$⊢ ((S \in CRing \land R \in SubRing (S)) \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to x +_{W} y = x +_{(1_{𝑜} mPoly U)} y$
32		eqidd	$⊢ ((S \in CRing \land R \in SubRing (S)) \land (x \in {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} \land y \in {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))})) \to x +_{(S ↑_{𝑠} (B^{1_{𝑜}}))} y = x +_{(S ↑_{𝑠} (B^{1_{𝑜}}))} y$
33		eqid	$⊢ \cdot_{W} = \cdot_{W}$
34	5 18 33	ply1mulr	$⊢ \cdot_{W} = \cdot_{(1_{𝑜} mPoly U)}$
35	34	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to \cdot_{W} = \cdot_{(1_{𝑜} mPoly U)}$
36	35	oveqdr	$⊢ ((S \in CRing \land R \in SubRing (S)) \land (x \in {Base}_{W} \land y \in {Base}_{W})) \to x \cdot_{W} y = x \cdot_{(1_{𝑜} mPoly U)} y$
37		eqidd	$⊢ ((S \in CRing \land R \in SubRing (S)) \land (x \in {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))} \land y \in {Base}_{(S ↑_{𝑠} (B^{1_{𝑜}}))})) \to x \cdot_{(S ↑_{𝑠} (B^{1_{𝑜}}))} y = x \cdot_{(S ↑_{𝑠} (B^{1_{𝑜}}))} y$
38	22 23 27 23 31 32 36 37	rhmpropd	$⊢ (S \in CRing \land R \in SubRing (S)) \to W RingHom (S ↑_{𝑠} (B^{1_{𝑜}})) = (1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}}))$
39	21 38	eleqtrrd	$⊢ (S \in CRing \land R \in SubRing (S)) \to (1_{𝑜} evalSub S) (R) \in (W RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
40		rhmco	$⊢ ((x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \in ((S ↑_{𝑠} (B^{1_{𝑜}})) RingHom T) \land (1_{𝑜} evalSub S) (R) \in (W RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R) \in (W RingHom T)$
41	15 39 40	syl2an2r	$⊢ (S \in CRing \land R \in SubRing (S)) \to (x \in (B^{(B^{1_{𝑜}})}) ⟼ x \circ (y \in B ⟼ 1_{𝑜} \times \{y\})) \circ (1_{𝑜} evalSub S) (R) \in (W RingHom T)$
42	13 41	eqeltrd	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom T)$

Metamath Proof Explorer

Theorem evls1rhm

Proof