This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evls1varsrng

Description: The evaluation of the variable of univariate 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 evls1varsrng.q 
|- Q = ( S evalSub1 R )
evls1varsrng.o 
|- O = ( eval1 ` S )
evls1varsrng.v 
|- V = ( var1 ` U )
evls1varsrng.u 
|- U = ( S |`s R )
evls1varsrng.b 
|- B = ( Base ` S )
evls1varsrng.s 
|- ( ph -> S e. CRing )
evls1varsrng.r 
|- ( ph -> R e. ( SubRing ` S ) )
Assertion evls1varsrng 
|- ( ph -> ( Q ` V ) = ( O ` V ) )

Proof

Step Hyp Ref Expression
1 evls1varsrng.q 
 |-  Q = ( S evalSub1 R )
2 evls1varsrng.o 
 |-  O = ( eval1 ` S )
3 evls1varsrng.v 
 |-  V = ( var1 ` U )
4 evls1varsrng.u 
 |-  U = ( S |`s R )
5 evls1varsrng.b 
 |-  B = ( Base ` S )
6 evls1varsrng.s 
 |-  ( ph -> S e. CRing )
7 evls1varsrng.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 1 3 4 5 6 7 evls1var 
 |-  ( ph -> ( Q ` V ) = ( _I |` B ) )
9 2 5 evl1fval1 
 |-  O = ( S evalSub1 B )
10 9 a1i 
 |-  ( ph -> O = ( S evalSub1 B ) )
11 10 fveq1d 
 |-  ( ph -> ( O ` V ) = ( ( S evalSub1 B ) ` V ) )
12 3 a1i 
 |-  ( ph -> V = ( var1 ` U ) )
13 eqid 
 |-  ( var1 ` S ) = ( var1 ` S )
14 13 7 4 subrgvr1 
 |-  ( ph -> ( var1 ` S ) = ( var1 ` U ) )
15 5 ressid 
 |-  ( S e. CRing -> ( S |`s B ) = S )
16 6 15 syl 
 |-  ( ph -> ( S |`s B ) = S )
17 16 eqcomd 
 |-  ( ph -> S = ( S |`s B ) )
18 17 fveq2d 
 |-  ( ph -> ( var1 ` S ) = ( var1 ` ( S |`s B ) ) )
19 12 14 18 3eqtr2d 
 |-  ( ph -> V = ( var1 ` ( S |`s B ) ) )
20 19 fveq2d 
 |-  ( ph -> ( ( S evalSub1 B ) ` V ) = ( ( S evalSub1 B ) ` ( var1 ` ( S |`s B ) ) ) )
21 eqid 
 |-  ( S evalSub1 B ) = ( S evalSub1 B )
22 eqid 
 |-  ( var1 ` ( S |`s B ) ) = ( var1 ` ( S |`s B ) )
23 eqid 
 |-  ( S |`s B ) = ( S |`s B )
24 crngring 
 |-  ( S e. CRing -> S e. Ring )
25 5 subrgid 
 |-  ( S e. Ring -> B e. ( SubRing ` S ) )
26 6 24 25 3syl 
 |-  ( ph -> B e. ( SubRing ` S ) )
27 21 22 23 5 6 26 evls1var 
 |-  ( ph -> ( ( S evalSub1 B ) ` ( var1 ` ( S |`s B ) ) ) = ( _I |` B ) )
28 11 20 27 3eqtrrd 
 |-  ( ph -> ( _I |` B ) = ( O ` V ) )
29 8 28 eqtrd 
 |-  ( ph -> ( Q ` V ) = ( O ` V ) )