evlsval3

Description: Give a formula for the polynomial evaluation homomorphism. (Contributed by SN, 26-Jul-2024)

	Ref	Expression
Hypotheses	evlsval3.q	$⊢ Q = (I evalSub S) (R)$
	evlsval3.p	$⊢ P = I mPoly U$
	evlsval3.b	$⊢ B = {Base}_{P}$
	evlsval3.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
	evlsval3.k	$⊢ K = {Base}_{S}$
	evlsval3.u	$⊢ U = S ↾_{𝑠} R$
	evlsval3.t	$⊢ T = S ↑_{𝑠} (K^{I})$
	evlsval3.m	$⊢ M = {mulGrp}_{T}$
	evlsval3.w	$⊢ \underset{˙}{\times} = \cdot_{M}$
	evlsval3.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
	evlsval3.e	$⊢ E = (p \in B ⟼ \underset{b \in D}{\sum_{T}} (F (p (b)) \underset{˙}{\cdot} (\sum_{M}, (b {\underset{˙}{\times}}_{f} G))))$
	evlsval3.f	$⊢ F = (x \in R ⟼ (K^{I}) \times \{x\})$
	evlsval3.g	$⊢ G = (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))$
	evlsval3.i	$⊢ φ \to I \in V$
	evlsval3.s	$⊢ φ \to S \in CRing$
	evlsval3.r	$⊢ φ \to R \in SubRing (S)$
Assertion	evlsval3	$⊢ φ \to Q = E$

Proof

Step	Hyp	Ref	Expression
1		evlsval3.q	$⊢ Q = (I evalSub S) (R)$
2		evlsval3.p	$⊢ P = I mPoly U$
3		evlsval3.b	$⊢ B = {Base}_{P}$
4		evlsval3.d	$⊢ D = \{h \in ({ℕ_{0}}^{I}) \| h^{-1} [ℕ] \in Fin\}$
5		evlsval3.k	$⊢ K = {Base}_{S}$
6		evlsval3.u	$⊢ U = S ↾_{𝑠} R$
7		evlsval3.t	$⊢ T = S ↑_{𝑠} (K^{I})$
8		evlsval3.m	$⊢ M = {mulGrp}_{T}$
9		evlsval3.w	$⊢ \underset{˙}{\times} = \cdot_{M}$
10		evlsval3.x	$⊢ \underset{˙}{\cdot} = \cdot_{T}$
11		evlsval3.e	$⊢ E = (p \in B ⟼ \underset{b \in D}{\sum_{T}} (F (p (b)) \underset{˙}{\cdot} (\sum_{M}, (b {\underset{˙}{\times}}_{f} G))))$
12		evlsval3.f	$⊢ F = (x \in R ⟼ (K^{I}) \times \{x\})$
13		evlsval3.g	$⊢ G = (x \in I ⟼ (a \in (K^{I}) ⟼ a (x)))$
14		evlsval3.i	$⊢ φ \to I \in V$
15		evlsval3.s	$⊢ φ \to S \in CRing$
16		evlsval3.r	$⊢ φ \to R \in SubRing (S)$
17		eqid	$⊢ I mVar U = I mVar U$
18		eqid	$⊢ algSc (P) = algSc (P)$
19	1 2 17 6 7 5 18 12 13	evlsval	$⊢ (I \in V \land S \in CRing \land R \in SubRing (S)) \to Q = (ι f \in (P RingHom T) \| (f \circ algSc (P) = F \land f \circ (I mVar U) = G))$
20	14 15 16 19	syl3anc	$⊢ φ \to Q = (ι f \in (P RingHom T) \| (f \circ algSc (P) = F \land f \circ (I mVar U) = G))$
21		eqid	$⊢ {Base}_{T} = {Base}_{T}$
22	6	subrgcrng	$⊢ (S \in CRing \land R \in SubRing (S)) \to U \in CRing$
23	15 16 22	syl2anc	$⊢ φ \to U \in CRing$
24		ovexd	$⊢ φ \to K^{I} \in V$
25	7	pwscrng	$⊢ (S \in CRing \land K^{I} \in V) \to T \in CRing$
26	15 24 25	syl2anc	$⊢ φ \to T \in CRing$
27	5	subrgss	$⊢ R \in SubRing (S) \to R \subseteq K$
28	16 27	syl	$⊢ φ \to R \subseteq K$
29	28	resmptd	$⊢ φ \to {(x \in K ⟼ (K^{I}) \times \{x\}) ↾}_{R} = (x \in R ⟼ (K^{I}) \times \{x\})$
30	12 29	eqtr4id	$⊢ φ \to F = {(x \in K ⟼ (K^{I}) \times \{x\}) ↾}_{R}$
31	15	crngringd	$⊢ φ \to S \in Ring$
32		eqid	$⊢ (x \in K ⟼ (K^{I}) \times \{x\}) = (x \in K ⟼ (K^{I}) \times \{x\})$
33	7 5 32	pwsdiagrhm	$⊢ (S \in Ring \land K^{I} \in V) \to (x \in K ⟼ (K^{I}) \times \{x\}) \in (S RingHom T)$
34	31 24 33	syl2anc	$⊢ φ \to (x \in K ⟼ (K^{I}) \times \{x\}) \in (S RingHom T)$
35	6	resrhm	$⊢ ((x \in K ⟼ (K^{I}) \times \{x\}) \in (S RingHom T) \land R \in SubRing (S)) \to {(x \in K ⟼ (K^{I}) \times \{x\}) ↾}_{R} \in (U RingHom T)$
36	34 16 35	syl2anc	$⊢ φ \to {(x \in K ⟼ (K^{I}) \times \{x\}) ↾}_{R} \in (U RingHom T)$
37	30 36	eqeltrd	$⊢ φ \to F \in (U RingHom T)$
38	5	fvexi	$⊢ K \in V$
39		elmapg	$⊢ (K \in V \land I \in V) \to (a \in (K^{I}) \leftrightarrow a : I ⟶ K)$
40	38 14 39	sylancr	$⊢ φ \to (a \in (K^{I}) \leftrightarrow a : I ⟶ K)$
41	40	biimpa	$⊢ (φ \land a \in (K^{I})) \to a : I ⟶ K$
42	41	adantlr	$⊢ ((φ \land x \in I) \land a \in (K^{I})) \to a : I ⟶ K$
43		simplr	$⊢ ((φ \land x \in I) \land a \in (K^{I})) \to x \in I$
44	42 43	ffvelrnd	$⊢ ((φ \land x \in I) \land a \in (K^{I})) \to a (x) \in K$
45	44	fmpttd	$⊢ (φ \land x \in I) \to (a \in (K^{I}) ⟼ a (x)) : K^{I} ⟶ K$
46		ovexd	$⊢ (φ \land x \in I) \to K^{I} \in V$
47	7 5 21	pwselbasb	$⊢ (S \in CRing \land K^{I} \in V) \to ((a \in (K^{I}) ⟼ a (x)) \in {Base}_{T} \leftrightarrow (a \in (K^{I}) ⟼ a (x)) : K^{I} ⟶ K)$
48	15 46 47	syl2an2r	$⊢ (φ \land x \in I) \to ((a \in (K^{I}) ⟼ a (x)) \in {Base}_{T} \leftrightarrow (a \in (K^{I}) ⟼ a (x)) : K^{I} ⟶ K)$
49	45 48	mpbird	$⊢ (φ \land x \in I) \to (a \in (K^{I}) ⟼ a (x)) \in {Base}_{T}$
50	49 13	fmptd	$⊢ φ \to G : I ⟶ {Base}_{T}$
51	2 3 21 4 8 9 10 17 11 14 23 26 37 50 18	evlslem1	$⊢ φ \to (E \in (P RingHom T) \land E \circ algSc (P) = F \land E \circ (I mVar U) = G)$
52	51	simp2d	$⊢ φ \to E \circ algSc (P) = F$
53	51	simp3d	$⊢ φ \to E \circ (I mVar U) = G$
54	51	simp1d	$⊢ φ \to E \in (P RingHom T)$
55	2 21 18 17 14 23 26 37 50	evlseu	$⊢ φ \to \exists! f \in (P RingHom T) (f \circ algSc (P) = F \land f \circ (I mVar U) = G)$
56		coeq1	$⊢ f = E \to f \circ algSc (P) = E \circ algSc (P)$
57	56	eqeq1d	$⊢ f = E \to (f \circ algSc (P) = F \leftrightarrow E \circ algSc (P) = F)$
58		coeq1	$⊢ f = E \to f \circ (I mVar U) = E \circ (I mVar U)$
59	58	eqeq1d	$⊢ f = E \to (f \circ (I mVar U) = G \leftrightarrow E \circ (I mVar U) = G)$
60	57 59	anbi12d	$⊢ f = E \to ((f \circ algSc (P) = F \land f \circ (I mVar U) = G) \leftrightarrow (E \circ algSc (P) = F \land E \circ (I mVar U) = G))$
61	60	riota2	$⊢ (E \in (P RingHom T) \land \exists! f \in (P RingHom T) (f \circ algSc (P) = F \land f \circ (I mVar U) = G)) \to ((E \circ algSc (P) = F \land E \circ (I mVar U) = G) \leftrightarrow (ι f \in (P RingHom T) \| (f \circ algSc (P) = F \land f \circ (I mVar U) = G)) = E)$
62	54 55 61	syl2anc	$⊢ φ \to ((E \circ algSc (P) = F \land E \circ (I mVar U) = G) \leftrightarrow (ι f \in (P RingHom T) \| (f \circ algSc (P) = F \land f \circ (I mVar U) = G)) = E)$
63	52 53 62	mpbi2and	$⊢ φ \to (ι f \in (P RingHom T) \| (f \circ algSc (P) = F \land f \circ (I mVar U) = G)) = E$
64	20 63	eqtrd	$⊢ φ \to Q = E$

Metamath Proof Explorer

Theorem evlsval3

Proof