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