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	$⊢ {Base}_{W} = {Base}_{W}$
25	5 24	ply1bas	$⊢ {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
26	25	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to {Base}_{W} = {Base}_{(1_{𝑜} mPoly U)}$
27		eqid	$⊢ +_{W} = +_{W}$
28	5 18 27	ply1plusg	$⊢ +_{W} = +_{(1_{𝑜} mPoly U)}$
29	28	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to +_{W} = +_{(1_{𝑜} mPoly U)}$
30	29	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$
31		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$
32		eqid	$⊢ \cdot_{W} = \cdot_{W}$
33	5 18 32	ply1mulr	$⊢ \cdot_{W} = \cdot_{(1_{𝑜} mPoly U)}$
34	33	a1i	$⊢ (S \in CRing \land R \in SubRing (S)) \to \cdot_{W} = \cdot_{(1_{𝑜} mPoly U)}$
35	34	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$
36		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$
37	22 23 26 23 30 31 35 36	rhmpropd	$⊢ (S \in CRing \land R \in SubRing (S)) \to W RingHom (S ↑_{𝑠} (B^{1_{𝑜}})) = (1_{𝑜} mPoly U) RingHom (S ↑_{𝑠} (B^{1_{𝑜}}))$
38	21 37	eleqtrrd	$⊢ (S \in CRing \land R \in SubRing (S)) \to (1_{𝑜} evalSub S) (R) \in (W RingHom (S ↑_{𝑠} (B^{1_{𝑜}})))$
39		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)$
40	15 38 39	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)$
41	13 40	eqeltrd	$⊢ (S \in CRing \land R \in SubRing (S)) \to Q \in (W RingHom T)$

Metamath Proof Explorer

Theorem evls1rhm

Proof