Theorem evlscaval

Description: Polynomial evaluation for scalars. See evlsscaval . (Contributed by Thierry Arnoux, 15-Feb-2026)

	Ref	Expression
Hypotheses	evlscafv.1	|- Q = ( I eval R )
	evlscafv.2	|- W = ( I mPoly R )
	evlscafv.3	|- B = ( Base ` R )
	evlscafv.4	|- A = ( algSc ` W )
	evlscafv.5	|- ( ph -> I e. V )
	evlscafv.6	|- ( ph -> R e. CRing )
	evlscafv.7	|- ( ph -> X e. B )
	evlscafv.8	|- ( ph -> L : I --> B )
Assertion	evlscaval	|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = X )

Proof

Step	Hyp	Ref	Expression
1		evlscafv.1	|- Q = ( I eval R )
2		evlscafv.2	|- W = ( I mPoly R )
3		evlscafv.3	|- B = ( Base ` R )
4		evlscafv.4	|- A = ( algSc ` W )
5		evlscafv.5	|- ( ph -> I e. V )
6		evlscafv.6	|- ( ph -> R e. CRing )
7		evlscafv.7	|- ( ph -> X e. B )
8		evlscafv.8	|- ( ph -> L : I --> B )
9	1 2 3 4 5 6 7	evlsca	|- ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) )
10	9	fveq1d	|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = ( ( ( B ^m I ) X. { X } ) ` L ) )
11	3	fvexi	|- B e. _V
12	11	a1i	|- ( ph -> B e. _V )
13	12 5 8	elmapdd	|- ( ph -> L e. ( B ^m I ) )
14		fvconst2g	|- ( ( X e. B /\ L e. ( B ^m I ) ) -> ( ( ( B ^m I ) X. { X } ) ` L ) = X )
15	7 13 14	syl2anc	|- ( ph -> ( ( ( B ^m I ) X. { X } ) ` L ) = X )
16	10 15	eqtrd	|- ( ph -> ( ( Q ` ( A ` X ) ) ` L ) = X )