Theorem evlsvarval

Description: Polynomial evaluation builder for a variable. (Contributed by SN, 27-Jul-2024)

	Ref	Expression
Hypotheses	evlsvarval.q	|- Q = ( ( I evalSub S ) ` R )
	evlsvarval.p	|- P = ( I mPoly U )
	evlsvarval.v	|- V = ( I mVar U )
	evlsvarval.u	|- U = ( S |`s R )
	evlsvarval.k	|- K = ( Base ` S )
	evlsvarval.b	|- B = ( Base ` P )
	evlsvarval.i	|- ( ph -> I e. W )
	evlsvarval.s	|- ( ph -> S e. CRing )
	evlsvarval.r	|- ( ph -> R e. ( SubRing ` S ) )
	evlsvarval.x	|- ( ph -> X e. I )
	evlsvarval.a	|- ( ph -> A e. ( K ^m I ) )
Assertion	evlsvarval	|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvarval.q	|- Q = ( ( I evalSub S ) ` R )
2		evlsvarval.p	|- P = ( I mPoly U )
3		evlsvarval.v	|- V = ( I mVar U )
4		evlsvarval.u	|- U = ( S |`s R )
5		evlsvarval.k	|- K = ( Base ` S )
6		evlsvarval.b	|- B = ( Base ` P )
7		evlsvarval.i	|- ( ph -> I e. W )
8		evlsvarval.s	|- ( ph -> S e. CRing )
9		evlsvarval.r	|- ( ph -> R e. ( SubRing ` S ) )
10		evlsvarval.x	|- ( ph -> X e. I )
11		evlsvarval.a	|- ( ph -> A e. ( K ^m I ) )
12	4	subrgring	|- ( R e. ( SubRing ` S ) -> U e. Ring )
13	9 12	syl	|- ( ph -> U e. Ring )
14	2 3 6 7 13 10	mvrcl	|- ( ph -> ( V ` X ) e. B )
15		fveq1	|- ( g = A -> ( g ` X ) = ( A ` X ) )
16	1 3 4 5 7 8 9 10	evlsvar	|- ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( K ^m I ) |-> ( g ` X ) ) )
17		fvexd	|- ( ph -> ( A ` X ) e. _V )
18	15 16 11 17	fvmptd4	|- ( ph -> ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) )
19	14 18	jca	|- ( ph -> ( ( V ` X ) e. B /\ ( ( Q ` ( V ` X ) ) ` A ) = ( A ` X ) ) )