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 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1varsrng.o 𝑂 = ( eval1𝑆 )
evls1varsrng.v 𝑉 = ( var1𝑈 )
evls1varsrng.u 𝑈 = ( 𝑆s 𝑅 )
evls1varsrng.b 𝐵 = ( Base ‘ 𝑆 )
evls1varsrng.s ( 𝜑𝑆 ∈ CRing )
evls1varsrng.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion evls1varsrng ( 𝜑 → ( 𝑄𝑉 ) = ( 𝑂𝑉 ) )

Proof

Step Hyp Ref Expression
1 evls1varsrng.q 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1varsrng.o 𝑂 = ( eval1𝑆 )
3 evls1varsrng.v 𝑉 = ( var1𝑈 )
4 evls1varsrng.u 𝑈 = ( 𝑆s 𝑅 )
5 evls1varsrng.b 𝐵 = ( Base ‘ 𝑆 )
6 evls1varsrng.s ( 𝜑𝑆 ∈ CRing )
7 evls1varsrng.r ( 𝜑𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 1 3 4 5 6 7 evls1var ( 𝜑 → ( 𝑄𝑉 ) = ( I ↾ 𝐵 ) )
9 2 5 evl1fval1 𝑂 = ( 𝑆 evalSub1 𝐵 )
10 9 a1i ( 𝜑𝑂 = ( 𝑆 evalSub1 𝐵 ) )
11 10 fveq1d ( 𝜑 → ( 𝑂𝑉 ) = ( ( 𝑆 evalSub1 𝐵 ) ‘ 𝑉 ) )
12 3 a1i ( 𝜑𝑉 = ( var1𝑈 ) )
13 eqid ( var1𝑆 ) = ( var1𝑆 )
14 13 7 4 subrgvr1 ( 𝜑 → ( var1𝑆 ) = ( var1𝑈 ) )
15 5 ressid ( 𝑆 ∈ CRing → ( 𝑆s 𝐵 ) = 𝑆 )
16 6 15 syl ( 𝜑 → ( 𝑆s 𝐵 ) = 𝑆 )
17 16 eqcomd ( 𝜑𝑆 = ( 𝑆s 𝐵 ) )
18 17 fveq2d ( 𝜑 → ( var1𝑆 ) = ( var1 ‘ ( 𝑆s 𝐵 ) ) )
19 12 14 18 3eqtr2d ( 𝜑𝑉 = ( var1 ‘ ( 𝑆s 𝐵 ) ) )
20 19 fveq2d ( 𝜑 → ( ( 𝑆 evalSub1 𝐵 ) ‘ 𝑉 ) = ( ( 𝑆 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑆s 𝐵 ) ) ) )
21 eqid ( 𝑆 evalSub1 𝐵 ) = ( 𝑆 evalSub1 𝐵 )
22 eqid ( var1 ‘ ( 𝑆s 𝐵 ) ) = ( var1 ‘ ( 𝑆s 𝐵 ) )
23 eqid ( 𝑆s 𝐵 ) = ( 𝑆s 𝐵 )
24 crngring ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
25 5 subrgid ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
26 6 24 25 3syl ( 𝜑𝐵 ∈ ( SubRing ‘ 𝑆 ) )
27 21 22 23 5 6 26 evls1var ( 𝜑 → ( ( 𝑆 evalSub1 𝐵 ) ‘ ( var1 ‘ ( 𝑆s 𝐵 ) ) ) = ( I ↾ 𝐵 ) )
28 11 20 27 3eqtrrd ( 𝜑 → ( I ↾ 𝐵 ) = ( 𝑂𝑉 ) )
29 8 28 eqtrd ( 𝜑 → ( 𝑄𝑉 ) = ( 𝑂𝑉 ) )