Theorem evlvar

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

	Ref	Expression
Hypotheses	evlvar.q	|- Q = ( I eval S )
	evlvar.v	|- V = ( I mVar S )
	evlvar.b	|- B = ( Base ` S )
	evlvar.i	|- ( ph -> I e. W )
	evlvar.s	|- ( ph -> S e. CRing )
	evlvar.x	|- ( ph -> X e. I )
Assertion	evlvar	|- ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )

Proof

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	|- ( ph -> I e. W )
5		evlvar.s	|- ( ph -> S e. CRing )
6		evlvar.x	|- ( ph -> X e. I )
7		eqid	|- ( ( I evalSub S ) ` B ) = ( ( I evalSub S ) ` B )
8		eqid	|- ( I mVar ( S |`s B ) ) = ( I mVar ( S |`s B ) )
9		eqid	|- ( S |`s B ) = ( S |`s B )
10		crngring	|- ( S e. CRing -> S e. Ring )
11	3	subrgid	|- ( S e. Ring -> B e. ( SubRing ` S ) )
12	5 10 11	3syl	|- ( ph -> B e. ( SubRing ` S ) )
13	7 1 8 9 3 4 5 12 6	evlsvarsrng	|- ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( Q ` ( ( I mVar ( S |`s B ) ) ` X ) ) )
14	7 8 9 3 4 5 12 6	evlsvar	|- ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
15	2 4 12 9	subrgmvr	|- ( ph -> V = ( I mVar ( S |`s B ) ) )
16	15	fveq1d	|- ( ph -> ( V ` X ) = ( ( I mVar ( S |`s B ) ) ` X ) )
17	16	eqcomd	|- ( ph -> ( ( I mVar ( S |`s B ) ) ` X ) = ( V ` X ) )
18	17	fveq2d	|- ( ph -> ( Q ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( Q ` ( V ` X ) ) )
19	13 14 18	3eqtr3rd	|- ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )