Theorem evls1scafv

Description: Value of the univariate polynomial evaluation for scalars. (Contributed by Thierry Arnoux, 21-Jan-2025)

	Ref	Expression
Hypotheses	evls1scafv.q	|- Q = ( S evalSub1 R )
	evls1scafv.w	|- W = ( Poly1 ` U )
	evls1scafv.u	|- U = ( S |`s R )
	evls1scafv.b	|- B = ( Base ` S )
	evls1scafv.a	|- A = ( algSc ` W )
	evls1scafv.s	|- ( ph -> S e. CRing )
	evls1scafv.r	|- ( ph -> R e. ( SubRing ` S ) )
	evls1scafv.x	|- ( ph -> X e. R )
	evls1scafv.1	|- ( ph -> C e. B )
Assertion	evls1scafv	|- ( ph -> ( ( Q ` ( A ` X ) ) ` C ) = X )

Proof

Step	Hyp	Ref	Expression
1		evls1scafv.q	|- Q = ( S evalSub1 R )
2		evls1scafv.w	|- W = ( Poly1 ` U )
3		evls1scafv.u	|- U = ( S |`s R )
4		evls1scafv.b	|- B = ( Base ` S )
5		evls1scafv.a	|- A = ( algSc ` W )
6		evls1scafv.s	|- ( ph -> S e. CRing )
7		evls1scafv.r	|- ( ph -> R e. ( SubRing ` S ) )
8		evls1scafv.x	|- ( ph -> X e. R )
9		evls1scafv.1	|- ( ph -> C e. B )
10	1 2 3 4 5 6 7 8	evls1sca	|- ( ph -> ( Q ` ( A ` X ) ) = ( B X. { X } ) )
11	10	fveq1d	|- ( ph -> ( ( Q ` ( A ` X ) ) ` C ) = ( ( B X. { X } ) ` C ) )
12		fvconst2g	|- ( ( X e. R /\ C e. B ) -> ( ( B X. { X } ) ` C ) = X )
13	8 9 12	syl2anc	|- ( ph -> ( ( B X. { X } ) ` C ) = X )
14	11 13	eqtrd	|- ( ph -> ( ( Q ` ( A ` X ) ) ` C ) = X )