Metamath Proof Explorer

Theorem evlsvarsrng

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

Ref Expression
Hypotheses evlsvarsrng.q 
|- Q = ( ( I evalSub S ) ` R )
evlsvarsrng.o 
|- O = ( I eval S )
evlsvarsrng.v 
|- V = ( I mVar U )
evlsvarsrng.u 
|- U = ( S |`s R )
evlsvarsrng.b 
|- B = ( Base ` S )
evlsvarsrng.i 
|- ( ph -> I e. A )
evlsvarsrng.s 
|- ( ph -> S e. CRing )
evlsvarsrng.r 
|- ( ph -> R e. ( SubRing ` S ) )
evlsvarsrng.x 
|- ( ph -> X e. I )
Assertion evlsvarsrng 
|- ( ph -> ( Q ` ( V ` X ) ) = ( O ` ( V ` X ) ) )

Proof

Step Hyp Ref Expression
1 evlsvarsrng.q 
 |-  Q = ( ( I evalSub S ) ` R )
2 evlsvarsrng.o 
 |-  O = ( I eval S )
3 evlsvarsrng.v 
 |-  V = ( I mVar U )
4 evlsvarsrng.u 
 |-  U = ( S |`s R )
5 evlsvarsrng.b 
 |-  B = ( Base ` S )
6 evlsvarsrng.i 
 |-  ( ph -> I e. A )
7 evlsvarsrng.s 
 |-  ( ph -> S e. CRing )
8 evlsvarsrng.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
9 evlsvarsrng.x 
 |-  ( ph -> X e. I )
10 1 3 4 5 6 7 8 9 evlsvar 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
11 2 5 evlval 
 |-  O = ( ( I evalSub S ) ` B )
12 11 a1i 
 |-  ( ph -> O = ( ( I evalSub S ) ` B ) )
13 12 fveq1d 
 |-  ( ph -> ( O ` ( V ` X ) ) = ( ( ( I evalSub S ) ` B ) ` ( V ` X ) ) )
14 3 a1i 
 |-  ( ph -> V = ( I mVar U ) )
15 eqid 
 |-  ( I mVar S ) = ( I mVar S )
16 15 6 8 4 subrgmvr 
 |-  ( ph -> ( I mVar S ) = ( I mVar U ) )
17 5 ressid 
 |-  ( S e. CRing -> ( S |`s B ) = S )
18 7 17 syl 
 |-  ( ph -> ( S |`s B ) = S )
19 18 eqcomd 
 |-  ( ph -> S = ( S |`s B ) )
20 19 oveq2d 
 |-  ( ph -> ( I mVar S ) = ( I mVar ( S |`s B ) ) )
21 14 16 20 3eqtr2d 
 |-  ( ph -> V = ( I mVar ( S |`s B ) ) )
22 21 fveq1d 
 |-  ( ph -> ( V ` X ) = ( ( I mVar ( S |`s B ) ) ` X ) )
23 22 fveq2d 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( V ` X ) ) = ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) )
24 eqid 
 |-  ( ( I evalSub S ) ` B ) = ( ( I evalSub S ) ` B )
25 eqid 
 |-  ( I mVar ( S |`s B ) ) = ( I mVar ( S |`s B ) )
26 eqid 
 |-  ( S |`s B ) = ( S |`s B )
27 crngring 
 |-  ( S e. CRing -> S e. Ring )
28 5 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
29 7 27 28 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
30 24 25 26 5 6 7 29 9 evlsvar 
 |-  ( ph -> ( ( ( I evalSub S ) ` B ) ` ( ( I mVar ( S |`s B ) ) ` X ) ) = ( g e. ( B ^m I ) |-> ( g ` X ) ) )
31 13 23 30 3eqtrrd 
 |-  ( ph -> ( g e. ( B ^m I ) |-> ( g ` X ) ) = ( O ` ( V ` X ) ) )
32 10 31 eqtrd 
 |-  ( ph -> ( Q ` ( V ` X ) ) = ( O ` ( V ` X ) ) )