evlvar

Description: Simple polynomial evaluation maps variables to projections. (Contributed by AV, 12-Sep-2019)

Step	Hyp	Ref	Expression
1		evlvar.q	$⊢ Q = I eval S$
2		evlvar.v	$⊢ V = I mVar S$
3		evlvar.b	$⊢ B = {Base}_{S}$
4		evlvar.i	$⊢ φ \to I \in W$
5		evlvar.s	$⊢ φ \to S \in CRing$
6		evlvar.x	$⊢ φ \to X \in I$
7		eqid	$⊢ (I evalSub S) (B) = (I evalSub S) (B)$
8		eqid	$⊢ I mVar (S ↾_{𝑠} B) = I mVar (S ↾_{𝑠} B)$
9		eqid	$⊢ S ↾_{𝑠} B = S ↾_{𝑠} B$
10		crngring	$⊢ S \in CRing \to S \in Ring$
11	3	subrgid	$⊢ S \in Ring \to B \in SubRing (S)$
12	5 10 11	3syl	$⊢ φ \to B \in SubRing (S)$
13	7 1 8 9 3 4 5 12 6	evlsvarsrng	$⊢ φ \to (I evalSub S) (B) ((I mVar (S ↾_{𝑠} B)) (X)) = Q ((I mVar (S ↾_{𝑠} B)) (X))$
14	7 8 9 3 4 5 12 6	evlsvar	$⊢ φ \to (I evalSub S) (B) ((I mVar (S ↾_{𝑠} B)) (X)) = (g \in (B^{I}) ⟼ g (X))$
15	2 4 12 9	subrgmvr	$⊢ φ \to V = I mVar (S ↾_{𝑠} B)$
16	15	fveq1d	$⊢ φ \to V (X) = (I mVar (S ↾_{𝑠} B)) (X)$
17	16	eqcomd	$⊢ φ \to (I mVar (S ↾_{𝑠} B)) (X) = V (X)$
18	17	fveq2d	$⊢ φ \to Q ((I mVar (S ↾_{𝑠} B)) (X)) = Q (V (X))$
19	13 14 18	3eqtr3rd	$⊢ φ \to Q (V (X)) = (g \in (B^{I}) ⟼ g (X))$

Metamath Proof Explorer