Theorem evls1scasrng

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, 13-Sep-2019)

	Ref	Expression
Hypotheses	evls1scasrng.q	⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
	evls1scasrng.o	⊢ 𝑂 = ( eval1 ‘ 𝑆 )
	evls1scasrng.w	⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
	evls1scasrng.u	⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
	evls1scasrng.p	⊢ 𝑃 = ( Poly1 ‘ 𝑆 )
	evls1scasrng.b	⊢ 𝐵 = ( Base ‘ 𝑆 )
	evls1scasrng.a	⊢ 𝐴 = ( algSc ‘ 𝑊 )
	evls1scasrng.c	⊢ 𝐶 = ( algSc ‘ 𝑃 )
	evls1scasrng.s	⊢ ( 𝜑 → 𝑆 ∈ CRing )
	evls1scasrng.r	⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
	evls1scasrng.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑅 )
Assertion	evls1scasrng	⊢ ( 𝜑 → ( 𝑄 ‘ ( 𝐴 ‘ 𝑋 ) ) = ( 𝑂 ‘ ( 𝐶 ‘ 𝑋 ) ) )

Proof

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