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	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsvarsrng.o	⊢ 𝑂 = ( 𝐼 eval 𝑆 )
	evlsvarsrng.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
	evlsvarsrng.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsvarsrng.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlsvarsrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
	evlsvarsrng.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsvarsrng.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsvarsrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
Assertion	evlsvarsrng	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsvarsrng.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsvarsrng.o	⊢ 𝑂 = ( 𝐼 eval 𝑆 )
3		evlsvarsrng.v	⊢ 𝑉 = ( 𝐼 mVar 𝑈 )
4		evlsvarsrng.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		evlsvarsrng.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
6		evlsvarsrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
7		evlsvarsrng.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
8		evlsvarsrng.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
9		evlsvarsrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
10	1 3 4 5 6 7 8 9	evlsvar	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
11	2 5	evlval	⊢ 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
12	11	a1i	⊢ ( 𝜑 → 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) )
13	12	fveq1d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝑉 ‘ 𝑋 ) ) )
14	3	a1i	⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar 𝑈 ) )
15		eqid	⊢ ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar 𝑆 )
16	15 6 8 4	subrgmvr	⊢ ( 𝜑 → ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar 𝑈 ) )
17	5	ressid	⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
18	7 17	syl	⊢ ( 𝜑 → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
19	18	eqcomd	⊢ ( 𝜑 → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
20	19	oveq2d	⊢ ( 𝜑 → ( 𝐼 mVar 𝑆 ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
21	14 16 20	3eqtr2d	⊢ ( 𝜑 → 𝑉 = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) )
22	21	fveq1d	⊢ ( 𝜑 → ( 𝑉 ‘ 𝑋 ) = ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) )
23	22	fveq2d	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝑉 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) )
24		eqid	⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
25		eqid	⊢ ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) )
26		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
27		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
28	5	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
29	7 27 28	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
30	24 25 26 5 6 7 29 9	evlsvar	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( 𝐼 mVar ( 𝑆 ↾s 𝐵 ) ) ‘ 𝑋 ) ) = ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) )
31	13 23 30	3eqtrrd	⊢ ( 𝜑 → ( 𝑔 ∈ ( 𝐵 ↑m 𝐼 ) ↦ ( 𝑔 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )
32	10 31	eqtrd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝑉 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝑉 ‘ 𝑋 ) ) )