Metamath Proof Explorer

Theorem evlsscasrng

Description: The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019)

Ref Expression
Hypotheses evlsscasrng.q 
|- Q = ( ( I evalSub S ) ` R )
evlsscasrng.o 
|- O = ( I eval S )
evlsscasrng.w 
|- W = ( I mPoly U )
evlsscasrng.u 
|- U = ( S |`s R )
evlsscasrng.p 
|- P = ( I mPoly S )
evlsscasrng.b 
|- B = ( Base ` S )
evlsscasrng.a 
|- A = ( algSc ` W )
evlsscasrng.c 
|- C = ( algSc ` P )
evlsscasrng.i 
|- ( ph -> I e. V )
evlsscasrng.s 
|- ( ph -> S e. CRing )
evlsscasrng.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsscasrng.x 
|- ( ph -> X e. R )
Assertion evlsscasrng 
|- ( ph -> ( Q ` ( A ` X ) ) = ( O ` ( C ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlsscasrng.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsscasrng.o 
 |-  O = ( I eval S )
3 evlsscasrng.w 
 |-  W = ( I mPoly U )
4 evlsscasrng.u 
 |-  U = ( S |`s R )
5 evlsscasrng.p 
 |-  P = ( I mPoly S )
6 evlsscasrng.b 
 |-  B = ( Base ` S )
7 evlsscasrng.a 
 |-  A = ( algSc ` W )
8 evlsscasrng.c 
 |-  C = ( algSc ` P )
9 evlsscasrng.i 
 |-  ( ph -> I e. V )
10 evlsscasrng.s 
 |-  ( ph -> S e. CRing )
11 evlsscasrng.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
12 evlsscasrng.x 
 |-  ( ph -> X e. R )
13 6 ressid 
 |-  ( S e. CRing -> ( S |`s B ) = S )
14 13 eqcomd 
 |-  ( S e. CRing -> S = ( S |`s B ) )
15 10 14 syl 
 |-  ( ph -> S = ( S |`s B ) )
16 15 oveq2d 
 |-  ( ph -> ( I mPoly S ) = ( I mPoly ( S |`s B ) ) )
17 5 16 eqtrid 
 |-  ( ph -> P = ( I mPoly ( S |`s B ) ) )
18 17 fveq2d 
 |-  ( ph -> ( algSc ` P ) = ( algSc ` ( I mPoly ( S |`s B ) ) ) )
19 8 18 eqtrid 
 |-  ( ph -> C = ( algSc ` ( I mPoly ( S |`s B ) ) ) )
20 19 fveq1d 
 |-  ( ph -> ( C ` X ) = ( ( algSc ` ( I mPoly ( S |`s B ) ) ) ` X ) )
21 20 fveq2d 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( C ` X ) ) = ( ( ( I evalSub S ) ` B ) ` ( ( algSc ` ( I mPoly ( S |`s B ) ) ) ` X ) ) )
22 eqid 
 |-  ( ( I evalSub S ) ` B ) = ( ( I evalSub S ) ` B )
23 eqid 
 |-  ( I mPoly ( S |`s B ) ) = ( I mPoly ( S |`s B ) )
24 eqid 
 |-  ( S |`s B ) = ( S |`s B )
25 eqid 
 |-  ( algSc ` ( I mPoly ( S |`s B ) ) ) = ( algSc ` ( I mPoly ( S |`s B ) ) )
26 crngring 
 |-  ( S e. CRing -> S e. Ring )
27 6 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
28 10 26 27 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
29 6 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ B )
30 11 29 syl 
 |-  ( ph -> R C_ B )
31 30 12 sseldd 
 |-  ( ph -> X e. B )
32 22 23 24 6 25 9 10 28 31 evlssca 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( algSc ` ( I mPoly ( S |`s B ) ) ) ` X ) ) = ( ( B ^m I ) X. { X } ) )
33 21 32 eqtrd 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( C ` X ) ) = ( ( B ^m I ) X. { X } ) )
34 2 6 evlval 
 |-  O = ( ( I evalSub S ) ` B )
35 34 a1i 
 |-  ( ph -> O = ( ( I evalSub S ) ` B ) )
36 35 fveq1d 
 |-  ( ph -> ( O ` ( C ` X ) ) = ( ( ( I evalSub S ) ` B ) ` ( C ` X ) ) )
37 1 3 4 6 7 9 10 11 12 evlssca 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( ( B ^m I ) X. { X } ) )
38 33 36 37 3eqtr4rd 
 |-  ( ph -> ( Q ` ( A ` X ) ) = ( O ` ( C ` X ) ) )