Metamath Proof Explorer

Theorem evlsca

Description: Simple polynomial evaluation maps scalars to constant functions. (Contributed by AV, 12-Sep-2019)

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

Proof

Step Hyp Ref Expression
1 evlsca.q 
 |-  Q = ( I eval S )
2 evlsca.w 
 |-  W = ( I mPoly S )
3 evlsca.b 
 |-  B = ( Base ` S )
4 evlsca.a 
 |-  A = ( algSc ` W )
5 evlsca.i 
 |-  ( ph -> I e. V )
6 evlsca.s 
 |-  ( ph -> S e. CRing )
7 evlsca.x 
 |-  ( ph -> X e. B )
8 eqid 
 |-  ( ( I evalSub S ) ` B ) = ( ( I evalSub S ) ` B )
9 eqid 
 |-  ( I mPoly ( S |`s B ) ) = ( I mPoly ( S |`s B ) )
10 eqid 
 |-  ( S |`s B ) = ( S |`s B )
11 eqid 
 |-  ( algSc ` ( I mPoly ( S |`s B ) ) ) = ( algSc ` ( I mPoly ( S |`s B ) ) )
12 crngring 
 |-  ( S e. CRing -> S e. Ring )
13 3 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
14 6 12 13 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
15 8 1 9 10 2 3 11 4 5 6 14 7 evlsscasrng 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( algSc ` ( I mPoly ( S |`s B ) ) ) ` X ) ) = ( Q ` ( A ` X ) ) )
16 8 9 10 3 11 5 6 14 7 evlssca 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( algSc ` ( I mPoly ( S |`s B ) ) ) ` X ) ) = ( ( B ^m I ) X. { X } ) )
17 15 16 eqtr3d 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) )