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 ⊢ 𝑄 = ( 𝑆 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 ⊢ ( 𝜑 → ( 𝑄 ‘ 𝑉 ) = ( 𝑂 ‘ 𝑉 ) )