evlsval2

Description: Characterizing properties of the polynomial evaluation map function. (Contributed by Stefan O'Rear, 12-Mar-2015) (Revised by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	evlsval.q	$⊢ Q = (I evalSub S) (R)$
	evlsval.w	$⊢ W = I mPoly U$
	evlsval.v	$⊢ V = I mVar U$
	evlsval.u	$⊢ U = S ↾_{𝑠} R$
	evlsval.t	$⊢ T = S ↑_{𝑠} (B^{I})$
	evlsval.b	$⊢ B = {Base}_{S}$
	evlsval.a	$⊢ A = algSc (W)$
	evlsval.x	$⊢ X = (x \in R ⟼ (B^{I}) \times \{x\})$
	evlsval.y	$⊢ Y = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))$
Assertion	evlsval2	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to (Q \in (W RingHom T) \land (Q \circ A = X \land Q \circ V = Y))$

Proof

Step	Hyp	Ref	Expression
1		evlsval.q	$⊢ Q = (I evalSub S) (R)$
2		evlsval.w	$⊢ W = I mPoly U$
3		evlsval.v	$⊢ V = I mVar U$
4		evlsval.u	$⊢ U = S ↾_{𝑠} R$
5		evlsval.t	$⊢ T = S ↑_{𝑠} (B^{I})$
6		evlsval.b	$⊢ B = {Base}_{S}$
7		evlsval.a	$⊢ A = algSc (W)$
8		evlsval.x	$⊢ X = (x \in R ⟼ (B^{I}) \times \{x\})$
9		evlsval.y	$⊢ Y = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))$
10	1 2 3 4 5 6 7 8 9	evlsval	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to Q = (ι m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y))$
11		eqid	$⊢ {Base}_{T} = {Base}_{T}$
12		simp1	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to I \in Z$
13	4	subrgcrng	$⊢ (S \in CRing \land R \in SubRing (S)) \to U \in CRing$
14	13	3adant1	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to U \in CRing$
15		simp2	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to S \in CRing$
16		ovex	$⊢ B^{I} \in V$
17	5	pwscrng	$⊢ (S \in CRing \land B^{I} \in V) \to T \in CRing$
18	15 16 17	sylancl	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to T \in CRing$
19	6	subrgss	$⊢ R \in SubRing (S) \to R \subseteq B$
20	19	3ad2ant3	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to R \subseteq B$
21	20	resmptd	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to {(x \in B ⟼ (B^{I}) \times \{x\}) ↾}_{R} = (x \in R ⟼ (B^{I}) \times \{x\})$
22	21 8	eqtr4di	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to {(x \in B ⟼ (B^{I}) \times \{x\}) ↾}_{R} = X$
23		crngring	$⊢ S \in CRing \to S \in Ring$
24	23	3ad2ant2	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to S \in Ring$
25		eqid	$⊢ (x \in B ⟼ (B^{I}) \times \{x\}) = (x \in B ⟼ (B^{I}) \times \{x\})$
26	5 6 25	pwsdiagrhm	$⊢ (S \in Ring \land B^{I} \in V) \to (x \in B ⟼ (B^{I}) \times \{x\}) \in (S RingHom T)$
27	24 16 26	sylancl	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to (x \in B ⟼ (B^{I}) \times \{x\}) \in (S RingHom T)$
28		simp3	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to R \in SubRing (S)$
29	4	resrhm	$⊢ ((x \in B ⟼ (B^{I}) \times \{x\}) \in (S RingHom T) \land R \in SubRing (S)) \to {(x \in B ⟼ (B^{I}) \times \{x\}) ↾}_{R} \in (U RingHom T)$
30	27 28 29	syl2anc	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to {(x \in B ⟼ (B^{I}) \times \{x\}) ↾}_{R} \in (U RingHom T)$
31	22 30	eqeltrrd	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to X \in (U RingHom T)$
32	6	fvexi	$⊢ B \in V$
33		simpl1	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to I \in Z$
34		elmapg	$⊢ (B \in V \land I \in Z) \to (g \in (B^{I}) \leftrightarrow g : I ⟶ B)$
35	32 33 34	sylancr	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to (g \in (B^{I}) \leftrightarrow g : I ⟶ B)$
36	35	biimpa	$⊢ (((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \land g \in (B^{I})) \to g : I ⟶ B$
37		simplr	$⊢ (((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \land g \in (B^{I})) \to x \in I$
38	36 37	ffvelcdmd	$⊢ (((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \land g \in (B^{I})) \to g (x) \in B$
39	38	fmpttd	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to (g \in (B^{I}) ⟼ g (x)) : B^{I} ⟶ B$
40		simpl2	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to S \in CRing$
41	5 6 11	pwselbasb	$⊢ (S \in CRing \land B^{I} \in V) \to ((g \in (B^{I}) ⟼ g (x)) \in {Base}_{T} \leftrightarrow (g \in (B^{I}) ⟼ g (x)) : B^{I} ⟶ B)$
42	40 16 41	sylancl	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to ((g \in (B^{I}) ⟼ g (x)) \in {Base}_{T} \leftrightarrow (g \in (B^{I}) ⟼ g (x)) : B^{I} ⟶ B)$
43	39 42	mpbird	$⊢ ((I \in Z \land S \in CRing \land R \in SubRing (S)) \land x \in I) \to (g \in (B^{I}) ⟼ g (x)) \in {Base}_{T}$
44	43 9	fmptd	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to Y : I ⟶ {Base}_{T}$
45	2 11 7 3 12 14 18 31 44	evlseu	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to \exists! m \in (W RingHom T) (m \circ A = X \land m \circ V = Y)$
46		riotacl2	$⊢ \exists! m \in (W RingHom T) (m \circ A = X \land m \circ V = Y) \to (ι m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)) \in \{m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)\}$
47	45 46	syl	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to (ι m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)) \in \{m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)\}$
48	10 47	eqeltrd	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to Q \in \{m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)\}$
49		coeq1	$⊢ m = Q \to m \circ A = Q \circ A$
50	49	eqeq1d	$⊢ m = Q \to (m \circ A = X \leftrightarrow Q \circ A = X)$
51		coeq1	$⊢ m = Q \to m \circ V = Q \circ V$
52	51	eqeq1d	$⊢ m = Q \to (m \circ V = Y \leftrightarrow Q \circ V = Y)$
53	50 52	anbi12d	$⊢ m = Q \to ((m \circ A = X \land m \circ V = Y) \leftrightarrow (Q \circ A = X \land Q \circ V = Y))$
54	53	elrab	$⊢ Q \in \{m \in (W RingHom T) \| (m \circ A = X \land m \circ V = Y)\} \leftrightarrow (Q \in (W RingHom T) \land (Q \circ A = X \land Q \circ V = Y))$
55	48 54	sylib	$⊢ (I \in Z \land S \in CRing \land R \in SubRing (S)) \to (Q \in (W RingHom T) \land (Q \circ A = X \land Q \circ V = Y))$

Metamath Proof Explorer

Theorem evlsval2

Proof