Metamath Proof Explorer

Theorem evlssca

Description: Polynomial evaluation maps scalars to constant functions. (Contributed by Stefan O'Rear, 13-Mar-2015) (Proof shortened by AV, 18-Sep-2021)

Ref Expression
Hypotheses evlssca.q 
|- Q = ( ( I evalSub S ) ` R )
evlssca.w 
|- W = ( I mPoly U )
evlssca.u 
|- U = ( S |`s R )
evlssca.b 
|- B = ( Base ` S )
evlssca.a 
|- A = ( algSc ` W )
evlssca.i 
|- ( ph -> I e. V )
evlssca.s 
|- ( ph -> S e. CRing )
evlssca.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlssca.x 
|- ( ph -> X e. R )
Assertion evlssca 
|- ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) )

Proof

Step Hyp Ref Expression
1 evlssca.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlssca.w 
 |-  W = ( I mPoly U )
3 evlssca.u 
 |-  U = ( S |`s R )
4 evlssca.b 
 |-  B = ( Base ` S )
5 evlssca.a 
 |-  A = ( algSc ` W )
6 evlssca.i 
 |-  ( ph -> I e. V )
7 evlssca.s 
 |-  ( ph -> S e. CRing )
8 evlssca.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
9 evlssca.x 
 |-  ( ph -> X e. R )
10 eqid 
 |-  ( I mVar U ) = ( I mVar U )
11 eqid 
 |-  ( S ^s ( B ^m I ) ) = ( S ^s ( B ^m I ) )
12 eqid 
 |-  ( x e. R |-> ( ( B ^m I ) X. { x } ) ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) )
13 eqid 
 |-  ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) ) = ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) )
14 1 2 10 3 11 4 5 12 13 evlsval2 
 |-  ( ( I e. V /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> ( Q e. ( W RingHom ( S ^s ( B ^m I ) ) ) /\ ( ( Q o. A ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) /\ ( Q o. ( I mVar U ) ) = ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) ) ) ) )
15 6 7 8 14 syl3anc 
 |-  ( ph -> ( Q e. ( W RingHom ( S ^s ( B ^m I ) ) ) /\ ( ( Q o. A ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) /\ ( Q o. ( I mVar U ) ) = ( x e. I |-> ( y e. ( B ^m I ) |-> ( y ` x ) ) ) ) ) )
16 15 simprld 
 |-  ( ph -> ( Q o. A ) = ( x e. R |-> ( ( B ^m I ) X. { x } ) ) )
17 16 fveq1d 
 |-  ( ph -> ( ( Q o. A ) ` X ) = ( ( x e. R |-> ( ( B ^m I ) X. { x } ) ) ` X ) )
18 eqid 
 |-  ( Base ` W ) = ( Base ` W )
19 eqid 
 |-  ( Base ` U ) = ( Base ` U )
20 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
21 8 20 syl 
 |-  ( ph -> U e. Ring )
22 2 18 19 5 6 21 mplasclf 
 |-  ( ph -> A : ( Base ` U ) --> ( Base ` W ) )
23 4 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
24 3 4 ressbas2 
 |-  ( R C_ B -> R = ( Base ` U ) )
25 8 23 24 3syl 
 |-  ( ph -> R = ( Base ` U ) )
26 25 feq2d 
 |-  ( ph -> ( A : R --> ( Base ` W ) <-> A : ( Base ` U ) --> ( Base ` W ) ) )
27 22 26 mpbird 
 |-  ( ph -> A : R --> ( Base ` W ) )
28 fvco3 
 |-  ( ( A : R --> ( Base ` W ) /\ X e. R ) -> ( ( Q o. A ) ` X ) = ( Q ` ( A ` X ) ) )
29 27 9 28 syl2anc 
 |-  ( ph -> ( ( Q o. A ) ` X ) = ( Q ` ( A ` X ) ) )
30 sneq 
 |-  ( x = X -> { x } = { X } )
31 30 xpeq2d 
 |-  ( x = X -> ( ( B ^m I ) X. { x } ) = ( ( B ^m I ) X. { X } ) )
32 ovex 
 |-  ( B ^m I ) e. _V
33 snex 
 |-  { X } e. _V
34 32 33 xpex 
 |-  ( ( B ^m I ) X. { X } ) e. _V
35 31 12 34 fvmpt 
 |-  ( X e. R -> ( ( x e. R |-> ( ( B ^m I ) X. { x } ) ) ` X ) = ( ( B ^m I ) X. { X } ) )
36 9 35 syl 
 |-  ( ph -> ( ( x e. R |-> ( ( B ^m I ) X. { x } ) ) ` X ) = ( ( B ^m I ) X. { X } ) )
37 17 29 36 3eqtr3d 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) )