Metamath Proof Explorer

Theorem evlsvar

Description: Polynomial evaluation maps variables to projections. (Contributed by Stefan O'Rear, 12-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlsvar.q 
|- Q = ( ( I evalSub S ) ` R )
evlsvar.v 
|- V = ( I mVar U )
evlsvar.u 
|- U = ( S |`s R )
evlsvar.b 
|- B = ( Base ` S )
evlsvar.i 
|- ( ph -> I e. W )
evlsvar.s 
|- ( ph -> S e. CRing )
evlsvar.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsvar.x 
|- ( ph -> X e. I )
Assertion evlsvar 
|- ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlsvar.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsvar.v 
 |-  V = ( I mVar U )
3 evlsvar.u 
 |-  U = ( S |`s R )
4 evlsvar.b 
 |-  B = ( Base ` S )
5 evlsvar.i 
 |-  ( ph -> I e. W )
6 evlsvar.s 
 |-  ( ph -> S e. CRing )
7 evlsvar.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 evlsvar.x 
 |-  ( ph -> X e. I )
9 eqid 
 |-  ( I mPoly U ) = ( I mPoly U )
10 eqid 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
11 eqid 
 |-  ( algSc ` ( I mPoly U ) ) = ( algSc ` ( I mPoly U ) )
12 eqid 
 |-  ( x e. R |-> ( ( B ^m I ) X. { x } ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
13 eqid 
 |-  ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) )
14 1 9 2 3 10 4 11 12 13 evlsval2 
 |-  ( ( I e. W /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q e. ( ( I mPoly U ) RingHom ( S ^s ( B ^m I ) ) ) /\ ( ( Q o. ( algSc ` ( I mPoly U ) ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) /\ ( Q o. V ) = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) ) ) )
15 5 6 7 14 syl3anc 
 |-  ( ph -> ( Q e. ( ( I mPoly U ) RingHom ( S ^s ( B ^m I ) ) ) /\ ( ( Q o. ( algSc ` ( I mPoly U ) ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) /\ ( Q o. V ) = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) ) ) )
16 15 simprrd 
 |-  ( ph -> ( Q o. V ) = ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) )
17 16 fveq1d 
 |-  ( ph -> ( ( Q o. V ) ` X ) = ( ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) ` X ) )
18 eqid 
 |-  ( Base ` ( I mPoly U ) ) = ( Base ` ( I mPoly U ) )
19 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
20 7 19 syl 
 |-  ( ph -> U e. Ring )
21 9 2 18 5 20 mvrf2 
 |-  ( ph -> V : I --> ( Base ` ( I mPoly U ) ) )
22 21 ffnd 
 |-  ( ph -> V Fn I )
23 fvco2 
 |-  ( ( V Fn I /\ X e. I ) -> ( ( Q o. V ) ` X ) = ( Q ` ( V ` X ) ) )
24 22 8 23 syl2anc 
 |-  ( ph -> ( ( Q o. V ) ` X ) = ( Q ` ( V ` X ) ) )
25 fveq2 
 |-  ( x = X -> ( g ` x ) = ( g ` X ) )
26 25 mpteq2dv 
 |-  ( x = X -> ( g e. ( B ^m I ) |-> ( g ` x ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
27 ovex 
 |-  ( B ^m I ) e. _V
28 27 mptex 
 |-  ( g e. ( B ^m I ) |-> ( g ` X ) ) e. _V
29 26 13 28 fvmpt 
 |-  ( X e. I -> ( ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) ` X ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
30 8 29 syl 
 |-  ( ph -> ( ( x e. I |-> ( g e. ( B ^m I ) |-> ( g ` x ) ) ) ` X ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
31 17 24 30 3eqtr3d 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )