Theorem evlsscasrng

Description: The evaluation of a scalar of a subring yields the same result as evaluated as a scalar over the ring itself. (Contributed by AV, 12-Sep-2019)

	Ref	Expression
Hypotheses	evlsscasrng.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
	evlsscasrng.o	⊢ 𝑂 = ( 𝐼 eval 𝑆 )
	evlsscasrng.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
	evlsscasrng.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evlsscasrng.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
	evlsscasrng.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evlsscasrng.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evlsscasrng.c	⊢ 𝐶 = ( algSc ‘ 𝑃 )
	evlsscasrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlsscasrng.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evlsscasrng.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evlsscasrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion	evlsscasrng	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlsscasrng.q	⊢ 𝑄 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝑅 )
2		evlsscasrng.o	⊢ 𝑂 = ( 𝐼 eval 𝑆 )
3		evlsscasrng.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑈 )
4		evlsscasrng.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5		evlsscasrng.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑆 )
6		evlsscasrng.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
7		evlsscasrng.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
8		evlsscasrng.c	⊢ 𝐶 = ( algSc ‘ 𝑃 )
9		evlsscasrng.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
10		evlsscasrng.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
11		evlsscasrng.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12		evlsscasrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
13	6	ressid	⊢ ( 𝑆 ∈ CRing → ( 𝑆 ↾s 𝐵 ) = 𝑆 )
14	13	eqcomd	⊢ ( 𝑆 ∈ CRing → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
15	10 14	syl	⊢ ( 𝜑 → 𝑆 = ( 𝑆 ↾s 𝐵 ) )
16	15	oveq2d	⊢ ( 𝜑 → ( 𝐼 mPoly 𝑆 ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
17	5 16	eqtrid	⊢ ( 𝜑 → 𝑃 = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
18	17	fveq2d	⊢ ( 𝜑 → ( algSc ‘ 𝑃 ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) )
19	8 18	eqtrid	⊢ ( 𝜑 → 𝐶 = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) )
20	19	fveq1d	⊢ ( 𝜑 → ( 𝐶 ‘ 𝑋 ) = ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) )
21	20	fveq2d	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) )
22		eqid	⊢ ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
23		eqid	⊢ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) = ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) )
24		eqid	⊢ ( 𝑆 ↾s 𝐵 ) = ( 𝑆 ↾s 𝐵 )
25		eqid	⊢ ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) = ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) )
26		crngring	⊢ ( 𝑆 ∈ CRing → 𝑆 ∈ Ring )
27	6	subrgid	⊢ ( 𝑆 ∈ Ring → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
28	10 26 27	3syl	⊢ ( 𝜑 → 𝐵 ∈ ( SubRing ‘ 𝑆 ) )
29	6	subrgss	⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ 𝐵 )
30	11 29	syl	⊢ ( 𝜑 → 𝑅 ⊆ 𝐵 )
31	30 12	sseldd	⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
32	22 23 24 6 25 9 10 28 31	evlssca	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( ( algSc ‘ ( 𝐼 mPoly ( 𝑆 ↾s 𝐵 ) ) ) ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
33	21 32	eqtrd	⊢ ( 𝜑 → ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
34	2 6	evlval	⊢ 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 )
35	34	a1i	⊢ ( 𝜑 → 𝑂 = ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) )
36	35	fveq1d	⊢ ( 𝜑 → ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) = ( ( ( 𝐼 evalSub 𝑆 ) ‘ 𝐵 ) ‘ ( 𝐶 ‘ 𝑋 ) ) )
37	1 3 4 6 7 9 10 11 12	evlssca	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( ( 𝐵 ↑m 𝐼 ) × { 𝑋 } ) )
38	33 36 37	3eqtr4rd	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )