evlsvar

Description: Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

	Ref	Expression
Hypotheses	evlsvar.q	$⊢ Q = (I evalSub S) (R)$
	evlsvar.v	$⊢ V = I mVar U$
	evlsvar.u	$⊢ U = S ↾_{𝑠} R$
	evlsvar.b	$⊢ B = {Base}_{S}$
	evlsvar.i	$⊢ φ \to I \in W$
	evlsvar.s	$⊢ φ \to S \in CRing$
	evlsvar.r	$⊢ φ \to R \in SubRing (S)$
	evlsvar.x	$⊢ φ \to X \in I$
Assertion	evlsvar	$⊢ φ \to Q (V (X)) = (g \in (B^{I}) ⟼ g (X))$

Proof

Step	Hyp	Ref	Expression
1		evlsvar.q	$⊢ Q = (I evalSub S) (R)$
2		evlsvar.v	$⊢ V = I mVar U$
3		evlsvar.u	$⊢ U = S ↾_{𝑠} R$
4		evlsvar.b	$⊢ B = {Base}_{S}$
5		evlsvar.i	$⊢ φ \to I \in W$
6		evlsvar.s	$⊢ φ \to S \in CRing$
7		evlsvar.r	$⊢ φ \to R \in SubRing (S)$
8		evlsvar.x	$⊢ φ \to X \in I$
9		eqid	$⊢ I mPoly U = I mPoly U$
10		eqid	$⊢ S ↑_{𝑠} (B^{I}) = S ↑_{𝑠} (B^{I})$
11		eqid	$⊢ algSc (I mPoly U) = algSc (I mPoly U)$
12		eqid	$⊢ (x \in R ⟼ (B^{I}) \times \{x\}) = (x \in R ⟼ (B^{I}) \times \{x\})$
13		eqid	$⊢ (x \in I ⟼ (g \in (B^{I}) ⟼ g (x))) = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))$
14	1 9 2 3 10 4 11 12 13	evlsval2	$⊢ (I \in W \land S \in CRing \land R \in SubRing (S)) \to (Q \in ((I mPoly U) RingHom (S ↑_{𝑠} (B^{I}))) \land (Q \circ algSc (I mPoly U) = (x \in R ⟼ (B^{I}) \times \{x\}) \land Q \circ V = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))))$
15	5 6 7 14	syl3anc	$⊢ φ \to (Q \in ((I mPoly U) RingHom (S ↑_{𝑠} (B^{I}))) \land (Q \circ algSc (I mPoly U) = (x \in R ⟼ (B^{I}) \times \{x\}) \land Q \circ V = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))))$
16	15	simprrd	$⊢ φ \to Q \circ V = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x)))$
17	16	fveq1d	$⊢ φ \to (Q \circ V) (X) = (x \in I ⟼ (g \in (B^{I}) ⟼ g (x))) (X)$
18		eqid	$⊢ {Base}_{(I mPoly U)} = {Base}_{(I mPoly U)}$
19	3	subrgring	$⊢ R \in SubRing (S) \to U \in Ring$
20	7 19	syl	$⊢ φ \to U \in Ring$
21	9 2 18 5 20	mvrf2	$⊢ φ \to V : I ⟶ {Base}_{(I mPoly U)}$
22	21	ffnd	$⊢ φ \to V Fn I$
23		fvco2	$⊢ (V Fn I \land X \in I) \to (Q \circ V) (X) = Q (V (X))$
24	22 8 23	syl2anc	$⊢ φ \to (Q \circ V) (X) = Q (V (X))$
25		fveq2	$⊢ x = X \to g (x) = g (X)$
26	25	mpteq2dv	$⊢ x = X \to (g \in (B^{I}) ⟼ g (x)) = (g \in (B^{I}) ⟼ g (X))$
27		ovex	$⊢ B^{I} \in V$
28	27	mptex	$⊢ (g \in (B^{I}) ⟼ g (X)) \in V$
29	26 13 28	fvmpt	$⊢ X \in I \to (x \in I ⟼ (g \in (B^{I}) ⟼ g (x))) (X) = (g \in (B^{I}) ⟼ g (X))$
30	8 29	syl	$⊢ φ \to (x \in I ⟼ (g \in (B^{I}) ⟼ g (x))) (X) = (g \in (B^{I}) ⟼ g (X))$
31	17 24 30	3eqtr3d	$⊢ φ \to Q (V (X)) = (g \in (B^{I}) ⟼ g (X))$

Metamath Proof Explorer

Theorem evlsvar

Proof